Theorem: SetTheory.mem_prod_iff (SetTheory/OPair.lean)

State before:
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ z ∈ prod x y ↔ ∃ a, a ∈ x ∧ ∃ b, b ∈ y ∧ z = opair a b
Tactic:
unfold prod
State after:
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ z ∈
      sep (BoundedFormula.memProd (Sum.inr 0) (Sum.inl true) (Sum.inl false)) (fun i => if i = true then x else y)
        (power (power (x ∪ y))) ↔
    ∃ a, a ∈ x ∧ ∃ b, b ∈ y ∧ z = opair a b

State before:
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ z ∈
      sep (BoundedFormula.memProd (Sum.inr 0) (Sum.inl true) (Sum.inl false)) (fun i => if i = true then x else y)
        (power (power (x ∪ y))) ↔
    ∃ a, a ∈ x ∧ ∃ b, b ∈ y ∧ z = opair a b
Tactic:
simp only [mem_sep_iff, mem_power_iff, interpret_memProd', interpret_inl, ite_true,
  ite_false, interpret_inr, and_iff_right_iff_imp, forall_exists_index, and_imp]
State after:
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ ∀ (x_1 : V), x_1 ∈ x → ∀ (x_2 : V), x_2 ∈ y → z = opair x_1 x_2 → z ⊆ power (x ∪ y)

State before:
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ ∀ (x_1 : V), x_1 ∈ x → ∀ (x_2 : V), x_2 ∈ y → z = opair x_1 x_2 → z ⊆ power (x ∪ y)
Tactic:
rintro a ha b hb rfl
State after:
V : Type u_1
inst✝ : Zermelo V
x y a : V
ha : a ∈ x
b : V
hb : b ∈ y
⊢ opair a b ⊆ power (x ∪ y)

State before:
V : Type u_1
inst✝ : Zermelo V
x y a : V
ha : a ∈ x
b : V
hb : b ∈ y
⊢ opair a b ⊆ power (x ∪ y)
Tactic:
intro z hz
State after:
V : Type u_1
inst✝ : Zermelo V
x y a : V
ha : a ∈ x
b : V
hb : b ∈ y
z : V
hz : z ∈ opair a b
⊢ z ∈ power (x ∪ y)

State before:
V : Type u_1
inst✝ : Zermelo V
x y a : V
ha : a ∈ x
b : V
hb : b ∈ y
z : V
hz : z ∈ opair a b
⊢ z ∈ power (x ∪ y)
Tactic:
rw [opair, mem_pair_iff] at hz
State after:
V : Type u_1
inst✝ : Zermelo V
x y a : V
ha : a ∈ x
b : V
hb : b ∈ y
z : V
hz : z = {a} ∨ z = pair a b
⊢ z ∈ power (x ∪ y)

State before:
case inr
V : Type u_1
inst✝ : Zermelo V
x y a : V
ha : a ∈ x
b : V
hb : b ∈ y
⊢ pair a b ∈ power (x ∪ y)
Tactic:
rw [mem_power_iff]
State after:
case inr
V : Type u_1
inst✝ : Zermelo V
x y a : V
ha : a ∈ x
b : V
hb : b ∈ y
⊢ pair a b ⊆ x ∪ y

State before:
case inr
V : Type u_1
inst✝ : Zermelo V
x y a : V
ha : a ∈ x
b : V
hb : b ∈ y
⊢ pair a b ⊆ x ∪ y
Tactic:
intro t ht
State after:
case inr
V : Type u_1
inst✝ : Zermelo V
x y a : V
ha : a ∈ x
b : V
hb : b ∈ y
t : V
ht : t ∈ pair a b
⊢ t ∈ x ∪ y

State before:
case inr
V : Type u_1
inst✝ : Zermelo V
x y a : V
ha : a ∈ x
b : V
hb : b ∈ y
t : V
ht : t ∈ pair a b
⊢ t ∈ x ∪ y
Tactic:
aesop
State after:
no goals