Theorem: SetTheory.π₂_opair (SetTheory/OPair.lean)

State before:
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ π₂ (opair x y) = y
Tactic:
unfold opair
State after:
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ π₂ (pair {x} (pair x y)) = y

State before:
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ π₂ (pair {x} (pair x y)) = y
Tactic:
ext z
State after:
case h
V : Type u_1
inst✝ : Zermelo V
x y z✝ z : V
⊢ z ∈ π₂ (pair {x} (pair x y)) ↔ z ∈ y

State before:
case h
V : Type u_1
inst✝ : Zermelo V
x y z✝ z : V
⊢ z ∈ π₂ (pair {x} (pair x y)) ↔ z ∈ y
Tactic:
rw [mem_π₂_iff]
State after:
case h
V : Type u_1
inst✝ : Zermelo V
x y z✝ z : V
⊢ (∃ z_1,
      z ∈ z_1 ∧
        z_1 ∈ ⋃ pair {x} (pair x y) ∧ (⋃ pair {x} (pair x y) ≠ ⋂ pair {x} (pair x y) → ¬z_1 ∈ ⋂ pair {x} (pair x y))) ↔
    z ∈ y

State before:
case h
V : Type u_1
inst✝ : Zermelo V
x y z✝ z : V
⊢ (∃ z_1,
      z ∈ z_1 ∧
        z_1 ∈ ⋃ pair {x} (pair x y) ∧ (⋃ pair {x} (pair x y) ≠ ⋂ pair {x} (pair x y) → ¬z_1 ∈ ⋂ pair {x} (pair x y))) ↔
    z ∈ y
Tactic:
simp only [sUnion_pair, sInter_pair, ne_eq, union_pair_eq_inter_pair]
State after:
case h
V : Type u_1
inst✝ : Zermelo V
x y z✝ z : V
⊢ (∃ z_1, z ∈ z_1 ∧ z_1 ∈ {x} ∪ pair x y ∧ (¬x = y → ¬z_1 ∈ {x} ∩ pair x y)) ↔ z ∈ y

State before:
case h
V : Type u_1
inst✝ : Zermelo V
x y z✝ z : V
⊢ (∃ z_1, z ∈ z_1 ∧ z_1 ∈ {x} ∪ pair x y ∧ (¬x = y → ¬z_1 ∈ {x} ∩ pair x y)) ↔ z ∈ y
Tactic:
constructor
State after:
case h.mp
V : Type u_1
inst✝ : Zermelo V
x y z✝ z : V
⊢ (∃ z_1, z ∈ z_1 ∧ z_1 ∈ {x} ∪ pair x y ∧ (¬x = y → ¬z_1 ∈ {x} ∩ pair x y)) → z ∈ y

case h.mpr
V : Type u_1
inst✝ : Zermelo V
x y z✝ z : V
⊢ z ∈ y → ∃ z_1, z ∈ z_1 ∧ z_1 ∈ {x} ∪ pair x y ∧ (¬x = y → ¬z_1 ∈ {x} ∩ pair x y)

State before:
case h.mp
V : Type u_1
inst✝ : Zermelo V
x y z✝ z : V
⊢ (∃ z_1, z ∈ z_1 ∧ z_1 ∈ {x} ∪ pair x y ∧ (¬x = y → ¬z_1 ∈ {x} ∩ pair x y)) → z ∈ y
Tactic:
rintro ⟨s, hzs, hsx, hs⟩
State after:
case h.mp.intro.intro.intro
V : Type u_1
inst✝ : Zermelo V
x y z✝ z s : V
hzs : z ∈ s
hsx : s ∈ {x} ∪ pair x y
hs : ¬x = y → ¬s ∈ {x} ∩ pair x y
⊢ z ∈ y

State before:
case h.mp.intro.intro.intro
V : Type u_1
inst✝ : Zermelo V
x y z✝ z s : V
hzs : z ∈ s
hsx : s ∈ {x} ∪ pair x y
hs : ¬x = y → ¬s ∈ {x} ∩ pair x y
⊢ z ∈ y
Tactic:
by_cases h : s = y
State after:
case pos
V : Type u_1
inst✝ : Zermelo V
x y z✝ z s : V
hzs : z ∈ s
hsx : s ∈ {x} ∪ pair x y
hs : ¬x = y → ¬s ∈ {x} ∩ pair x y
h : s = y
⊢ z ∈ y

case neg
V : Type u_1
inst✝ : Zermelo V
x y z✝ z s : V
hzs : z ∈ s
hsx : s ∈ {x} ∪ pair x y
hs : ¬x = y → ¬s ∈ {x} ∩ pair x y
h : ¬s = y
⊢ z ∈ y

State before:
case pos
V : Type u_1
inst✝ : Zermelo V
x y z✝ z s : V
hzs : z ∈ s
hsx : s ∈ {x} ∪ pair x y
hs : ¬x = y → ¬s ∈ {x} ∩ pair x y
h : s = y
⊢ z ∈ y
Tactic:
subst h
State after:
case pos
V : Type u_1
inst✝ : Zermelo V
x z✝ z s : V
hzs : z ∈ s
hsx : s ∈ {x} ∪ pair x s
hs : ¬x = s → ¬s ∈ {x} ∩ pair x s
⊢ z ∈ s

State before:
case pos
V : Type u_1
inst✝ : Zermelo V
x z✝ z s : V
hzs : z ∈ s
hsx : s ∈ {x} ∪ pair x s
hs : ¬x = s → ¬s ∈ {x} ∩ pair x s
⊢ z ∈ s
Tactic:
exact hzs
State after:
no goals

State before:
case neg
V : Type u_1
inst✝ : Zermelo V
x y z✝ z s : V
hzs : z ∈ s
hsx : s ∈ {x} ∪ pair x y
hs : ¬x = y → ¬s ∈ {x} ∩ pair x y
h : ¬s = y
⊢ z ∈ y
Tactic:
aesop
State after:
no goals

State before:
case h.mpr
V : Type u_1
inst✝ : Zermelo V
x y z✝ z : V
⊢ z ∈ y → ∃ z_1, z ∈ z_1 ∧ z_1 ∈ {x} ∪ pair x y ∧ (¬x = y → ¬z_1 ∈ {x} ∩ pair x y)
Tactic:
aesop
State after:
no goals