x : PSet
⊢ ZFSet.Nonempty (mk x) → PSet.Nonempty x
x : PSet
⊢ ZFSet.Nonempty (mk x) ↔ PSet.Nonempty x
refine' ⟨_, fun ⟨a, h⟩ => ⟨mk a, h⟩⟩
case intro
x : PSet
a : ZFSet
h : a ∈ toSet (mk x)
⊢ PSet.Nonempty x
x : PSet
⊢ ZFSet.Nonempty (mk x) → PSet.Nonempty x
rintro ⟨a, h⟩
case intro.h
x a✝ : PSet
h : Quotient.mk setoid a✝ ∈ toSet (mk x)
⊢ PSet.Nonempty x
case intro
x : PSet
a : ZFSet
h : a ∈ toSet (mk x)
⊢ PSet.Nonempty x
induction a using Quotient.inductionOn
no goals
case intro.h
x a✝ : PSet
h : Quotient.mk setoid a✝ ∈ toSet (mk x)
⊢ PSet.Nonempty x
exact ⟨_, h⟩