p : ZFSet → Prop
x y : ZFSet
⊢ ∀ (x : ZFSet), (∀ (y : ZFSet), y ∈ x → Hereditarily p y → p ∅) → Hereditarily p x → p ∅
p : ZFSet → Prop
x y : ZFSet
⊢ Hereditarily p x → p ∅
apply @ZFSet.inductionOn _ x
p : ZFSet → Prop
x y✝ y : ZFSet
IH : ∀ (y_1 : ZFSet), y_1 ∈ y → Hereditarily p y_1 → p ∅
h : Hereditarily p y
⊢ p ∅
p : ZFSet → Prop
x y : ZFSet
⊢ ∀ (x : ZFSet), (∀ (y : ZFSet), y ∈ x → Hereditarily p y → p ∅) → Hereditarily p x → p ∅
intro y IH h
case inl
p : ZFSet → Prop
x y : ZFSet
IH : ∀ (y : ZFSet), y ∈ ∅ → Hereditarily p y → p ∅
h : Hereditarily p ∅
⊢ p ∅

case inr.intro
p : ZFSet → Prop
x y✝ y : ZFSet
IH : ∀ (y_1 : ZFSet), y_1 ∈ y → Hereditarily p y_1 → p ∅
h : Hereditarily p y
a : ZFSet
ha : a ∈ toSet y
⊢ p ∅
p : ZFSet → Prop
x y✝ y : ZFSet
IH : ∀ (y_1 : ZFSet), y_1 ∈ y → Hereditarily p y_1 → p ∅
h : Hereditarily p y
⊢ p ∅
rcases ZFSet.eq_empty_or_nonempty y with (rfl | ⟨a, ha⟩)
no goals
case inl
p : ZFSet → Prop
x y : ZFSet
IH : ∀ (y : ZFSet), y ∈ ∅ → Hereditarily p y → p ∅
h : Hereditarily p ∅
⊢ p ∅
exact h.self
no goals
case inr.intro
p : ZFSet → Prop
x y✝ y : ZFSet
IH : ∀ (y_1 : ZFSet), y_1 ∈ y → Hereditarily p y_1 → p ∅
h : Hereditarily p y
a : ZFSet
ha : a ∈ toSet y
⊢ p ∅
exact IH a ha (h.mem ha)