p : ZFSet → ZFSet → Prop
x y z : ZFSet
e : ∃ a, a ∈ x ∧ ∃ b, b ∈ y ∧ z = pair a b ∧ p a b
⊢ z ∈ powerset (powerset (x ∪ y))
p : ZFSet → ZFSet → Prop
x y z : ZFSet
⊢ z ∈ pairSep p x y ↔ ∃ a, a ∈ x ∧ ∃ b, b ∈ y ∧ z = pair a b ∧ p a b
refine' mem_sep.trans ⟨And.right, fun e => ⟨_, e⟩⟩
case intro.intro.intro.intro.intro
p : ZFSet → ZFSet → Prop
x y a : ZFSet
ax : a ∈ x
b : ZFSet
bY : b ∈ y
pab : p a b
⊢ pair a b ∈ powerset (powerset (x ∪ y))
p : ZFSet → ZFSet → Prop
x y z : ZFSet
e : ∃ a, a ∈ x ∧ ∃ b, b ∈ y ∧ z = pair a b ∧ p a b
⊢ z ∈ powerset (powerset (x ∪ y))
rcases e with ⟨a, ax, b, bY, rfl, pab⟩
case intro.intro.intro.intro.intro
p : ZFSet → ZFSet → Prop
x y a : ZFSet
ax : a ∈ x
b : ZFSet
bY : b ∈ y
pab : p a b
⊢ ∀ ⦃z : ZFSet⦄, z = {a} ∨ z = {a, b} → ∀ ⦃z_1 : ZFSet⦄, z_1 ∈ z → z_1 ∈ x ∨ z_1 ∈ y
case intro.intro.intro.intro.intro
p : ZFSet → ZFSet → Prop
x y a : ZFSet
ax : a ∈ x
b : ZFSet
bY : b ∈ y
pab : p a b
⊢ pair a b ∈ powerset (powerset (x ∪ y))
simp only [mem_powerset, subset_def, mem_union, pair, mem_pair]
case intro.intro.intro.intro.intro.inl
p : ZFSet → ZFSet → Prop
x y a : ZFSet
ax : a ∈ x
b : ZFSet
bY : b ∈ y
pab : p a b
v : ZFSet
⊢ v = a → v ∈ x ∨ v ∈ y

case intro.intro.intro.intro.intro.inr
p : ZFSet → ZFSet → Prop
x y a : ZFSet
ax : a ∈ x
b : ZFSet
bY : b ∈ y
pab : p a b
v : ZFSet
⊢ v = a ∨ v = b → v ∈ x ∨ v ∈ y
case intro.intro.intro.intro.intro
p : ZFSet → ZFSet → Prop
x y a : ZFSet
ax : a ∈ x
b : ZFSet
bY : b ∈ y
pab : p a b
⊢ ∀ ⦃z : ZFSet⦄, z = {a} ∨ z = {a, b} → ∀ ⦃z_1 : ZFSet⦄, z_1 ∈ z → z_1 ∈ x ∨ z_1 ∈ y
rintro u (rfl | rfl) v <;> simp only [mem_singleton, mem_pair]
case intro.intro.intro.intro.intro.inl
p : ZFSet → ZFSet → Prop
x y b : ZFSet
bY : b ∈ y
v : ZFSet
ax : v ∈ x
pab : p v b
⊢ v ∈ x ∨ v ∈ y
case intro.intro.intro.intro.intro.inl
p : ZFSet → ZFSet → Prop
x y a : ZFSet
ax : a ∈ x
b : ZFSet
bY : b ∈ y
pab : p a b
v : ZFSet
⊢ v = a → v ∈ x ∨ v ∈ y
rintro rfl
no goals
case intro.intro.intro.intro.intro.inl
p : ZFSet → ZFSet → Prop
x y b : ZFSet
bY : b ∈ y
v : ZFSet
ax : v ∈ x
pab : p v b
⊢ v ∈ x ∨ v ∈ y
exact Or.inl ax
no goals
case intro.intro.intro.intro.intro.inr
p : ZFSet → ZFSet → Prop
x y a : ZFSet
ax : a ∈ x
b : ZFSet
bY : b ∈ y
pab : p a b
v : ZFSet
⊢ v = a ∨ v = b → v ∈ x ∨ v ∈ y
rintro (rfl | rfl) <;> [left; right] <;> assumption