case mp
α : Type u
f : α → ZFSet
x : ZFSet
y : PSet
⊢ Quotient.mk setoid y ∈ range f → Quotient.mk setoid y ∈ Set.range f

case mpr
α : Type u
f : α → ZFSet
x : ZFSet
y : PSet
⊢ Quotient.mk setoid y ∈ Set.range f → Quotient.mk setoid y ∈ range f
α : Type u
f : α → ZFSet
x : ZFSet
y : PSet
⊢ Quotient.mk setoid y ∈ range f ↔ Quotient.mk setoid y ∈ Set.range f
constructor
case mp.intro
α : Type u
f : α → ZFSet
x : ZFSet
y : PSet
z : Type (PSet.mk (ULift α) (Quotient.out ∘ f ∘ ULift.down))
hz : PSet.Equiv y (Func (PSet.mk (ULift α) (Quotient.out ∘ f ∘ ULift.down)) z)
⊢ Quotient.mk setoid y ∈ Set.range f
case mp
α : Type u
f : α → ZFSet
x : ZFSet
y : PSet
⊢ Quotient.mk setoid y ∈ range f → Quotient.mk setoid y ∈ Set.range f
rintro ⟨z, hz⟩
no goals
case mp.intro
α : Type u
f : α → ZFSet
x : ZFSet
y : PSet
z : Type (PSet.mk (ULift α) (Quotient.out ∘ f ∘ ULift.down))
hz : PSet.Equiv y (Func (PSet.mk (ULift α) (Quotient.out ∘ f ∘ ULift.down)) z)
⊢ Quotient.mk setoid y ∈ Set.range f
exact ⟨z.down, Quotient.eq_mk_iff_out.2 hz.symm⟩
case mpr.intro
α : Type u
f : α → ZFSet
x : ZFSet
y : PSet
z : α
hz : f z = Quotient.mk setoid y
⊢ Quotient.mk setoid y ∈ range f
case mpr
α : Type u
f : α → ZFSet
x : ZFSet
y : PSet
⊢ Quotient.mk setoid y ∈ Set.range f → Quotient.mk setoid y ∈ range f
rintro ⟨z, hz⟩
case mpr.intro
α : Type u
f : α → ZFSet
x : ZFSet
y : PSet
z : α
hz : f z = Quotient.mk setoid y
⊢ PSet.Equiv y (Func (PSet.mk (ULift α) (Quotient.out ∘ f ∘ ULift.down)) { down := z })
case mpr.intro
α : Type u
f : α → ZFSet
x : ZFSet
y : PSet
z : α
hz : f z = Quotient.mk setoid y
⊢ Quotient.mk setoid y ∈ range f
use ULift.up z
no goals
case mpr.intro
α : Type u
f : α → ZFSet
x : ZFSet
y : PSet
z : α
hz : f z = Quotient.mk setoid y
⊢ PSet.Equiv y (Func (PSet.mk (ULift α) (Quotient.out ∘ f ∘ ULift.down)) { down := z })
simpa [hz] using PSet.Equiv.symm (Quotient.mk_out y)