feat(set_theory/zfc/basic): pSet with empty type is equivalent to `…

…Ø` (#15550)

We also add `Set.equiv_iff`, which unfolds the definition of `equiv` in terms of `Set.func` and `Set.type`.

src/set_theory/zfc/basic.lean

@@ -109,13 +109,15 @@ equivalent to some element of the second family and vice-versa. -/
 def equiv (x y : pSet) : Prop :=
 pSet.rec (λ α z m ⟨β, B⟩, (∀ a, ∃ b, m a (B b)) ∧ (∀ b, ∃ a, m a (B b))) x y
 
-theorem exists_equiv_left : Π {x y : pSet} (h : equiv x y) (i : x.type),
-  ∃ j, equiv (x.func i) (y.func j)
-| ⟨α, A⟩ ⟨β, B⟩ h := h.1
+theorem equiv_iff : Π {x y : pSet}, equiv x y ↔
+  (∀ i, ∃ j, equiv (x.func i) (y.func j)) ∧ (∀ j, ∃ i, equiv (x.func i) (y.func j))
+| ⟨α, A⟩ ⟨β, B⟩ := iff.rfl
 
-theorem exists_equiv_right : Π {x y : pSet} (h : equiv x y) (j : y.type),
-  ∃ i, equiv (x.func i) (y.func j)
-| ⟨α, A⟩ ⟨β, B⟩ h := h.2
+theorem equiv.exists_left {x y : pSet} (h : equiv x y) : ∀ i, ∃ j, equiv (x.func i) (y.func j) :=
+(equiv_iff.1 h).1
+
+theorem equiv.exists_right {x y : pSet} (h : equiv x y) : ∀ j, ∃ i, equiv (x.func i) (y.func j) :=
+(equiv_iff.1 h).2
 
 @[refl] protected theorem equiv.refl (x) : equiv x x :=
 pSet.rec_on x $ λ α A IH, ⟨λ a, ⟨a, IH a⟩, λ a, ⟨a, IH a⟩⟩
@@ -133,6 +135,9 @@ pSet.rec_on x $ λ α A IH y, pSet.cases_on y $ λ β B ⟨γ, Γ⟩ ⟨αβ, β
 @[trans] protected theorem equiv.trans {x y z} (h1 : equiv x y) (h2 : equiv y z) : equiv x z :=
 h1.euc h2.symm
 
+protected theorem equiv_of_is_empty (x y : pSet) [is_empty x.type] [is_empty y.type] : equiv x y :=
+equiv_iff.2 $ by simp
+
 instance setoid : setoid pSet :=
 ⟨pSet.equiv, equiv.refl, λ x y, equiv.symm, λ x y z, equiv.trans⟩
 
@@ -198,7 +203,7 @@ theorem mem.congr_left : Π {x y : pSet.{u}}, equiv x y → (∀ {w : pSet.{u}},
 private theorem mem_wf_aux : Π {x y : pSet.{u}}, equiv x y → acc (∈) y
 | ⟨α, A⟩ ⟨β, B⟩ H := ⟨_, begin
   rintros ⟨γ, C⟩ ⟨b, hc⟩,
-  cases exists_equiv_right H b with a ha,
+  cases H.exists_right b with a ha,
   have H := ha.trans hc.symm,
   rw mk_func at H,
   exact mem_wf_aux H
@@ -234,6 +239,9 @@ instance : is_empty (type (∅)) := pempty.is_empty
 
 @[simp] theorem empty_subset (x : pSet.{u}) : (∅ : pSet) ⊆ x := λ x, x.elim
 
+protected theorem equiv_empty (x : pSet) [is_empty x.type] : equiv x ∅ :=
+pSet.equiv_of_is_empty x _
+
 /-- Insert an element into a pre-set -/
 protected def insert (x y : pSet) : pSet := ⟨option y.type, λ o, option.rec x y.func o⟩