a x : ZFSet
IH : ∀ (y : ZFSet), y ∈ x → Acc (fun x x_1 => x ∈ x_1) ↑y
⊢ ∀ (y : Class), y ∈ ↑x → Acc (fun x x_1 => x ∈ x_1) y
⊢ ∀ (x : ZFSet), Acc (fun x x_1 => x ∈ x_1) ↑x
refine' fun a => ZFSet.inductionOn a fun x IH => ⟨_, _⟩
case intro.intro
a x : ZFSet
IH : ∀ (y : ZFSet), y ∈ x → Acc (fun x x_1 => x ∈ x_1) ↑y
z : ZFSet
hz : ↑x z
⊢ Acc (fun x x_1 => x ∈ x_1) ↑z
a x : ZFSet
IH : ∀ (y : ZFSet), y ∈ x → Acc (fun x x_1 => x ∈ x_1) ↑y
⊢ ∀ (y : Class), y ∈ ↑x → Acc (fun x x_1 => x ∈ x_1) y
rintro A ⟨z, rfl, hz⟩
no goals
case intro.intro
a x : ZFSet
IH : ∀ (y : ZFSet), y ∈ x → Acc (fun x x_1 => x ∈ x_1) ↑y
z : ZFSet
hz : ↑x z
⊢ Acc (fun x x_1 => x ∈ x_1) ↑z
exact IH z hz
H : ∀ (x : ZFSet), Acc (fun x x_1 => x ∈ x_1) ↑x
A : Class
⊢ ∀ (y : Class), y ∈ A → Acc (fun x x_1 => x ∈ x_1) y
H : ∀ (x : ZFSet), Acc (fun x x_1 => x ∈ x_1) ↑x
⊢ ∀ (a : Class), Acc (fun x x_1 => x ∈ x_1) a
refine' fun A => ⟨A, _⟩
case intro.intro
H : ∀ (x : ZFSet), Acc (fun x x_1 => x ∈ x_1) ↑x
A : Class
x : ZFSet
right✝ : A x
⊢ Acc (fun x x_1 => x ∈ x_1) ↑x
H : ∀ (x : ZFSet), Acc (fun x x_1 => x ∈ x_1) ↑x
A : Class
⊢ ∀ (y : Class), y ∈ A → Acc (fun x x_1 => x ∈ x_1) y
rintro B ⟨x, rfl, _⟩
no goals
case intro.intro
H : ∀ (x : ZFSet), Acc (fun x x_1 => x ∈ x_1) ↑x
A : Class
x : ZFSet
right✝ : A x
⊢ Acc (fun x x_1 => x ∈ x_1) ↑x
exact H x