A : Class
hA : powerset A ⊆ A
hnA : ∃ x, ¬A x
⊢ False
A : Class
hA : powerset A ⊆ A
⊢ ∀ (x : ZFSet), A x
by_contra' hnA
no goals
A : Class
hA : powerset A ⊆ A
hnA : ∃ x, ¬A x
⊢ False
exact
  WellFounded.min_mem ZFSet.mem_wf _ hnA
    (hA fun x hx =>
      Classical.not_not.1 fun hB =>
        WellFounded.not_lt_min ZFSet.mem_wf _ hnA hB <| coe_apply.1 hx)