feat(SetTheory/ZFC/Basic): order instances (#19946)

Sets form a partial order under the subset relation.

Author: vihdzp

Mathlib/SetTheory/ZFC/Basic.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
 import Mathlib.Data.Fin.VecNotation
+import Mathlib.Data.SetLike.Basic
 import Mathlib.Logic.Small.Basic
 import Mathlib.SetTheory.ZFC.PSet
 
@@ -241,8 +242,25 @@ theorem toSet_injective : Function.Injective toSet := fun _ _ h => ext <| Set.ex
 theorem toSet_inj {x y : ZFSet} : x.toSet = y.toSet ↔ x = y :=
   toSet_injective.eq_iff
 
+instance : SetLike ZFSet ZFSet where
+  coe := toSet
+  coe_injective' := toSet_injective
+
+instance : HasSSubset ZFSet := ⟨(· < ·)⟩
+
+@[simp]
+theorem le_def (x y : ZFSet) : x ≤ y ↔ x ⊆ y :=
+  Iff.rfl
+
+@[simp]
+theorem lt_def (x y : ZFSet) : x < y ↔ x ⊂ y :=
+  Iff.rfl
+
 instance : IsAntisymm ZFSet (· ⊆ ·) :=
-  ⟨fun _ _ hab hba => ext fun c => ⟨@hab c, @hba c⟩⟩
+  ⟨@le_antisymm ZFSet _⟩
+
+instance : IsNonstrictStrictOrder ZFSet (· ⊆ ·) (· ⊂ ·) :=
+  ⟨fun _ _ ↦ Iff.rfl⟩
 
 /-- The empty ZFC set -/
 protected def empty : ZFSet :=

Mathlib/SetTheory/ZFC/Class.lean

@@ -276,7 +276,7 @@ theorem eq_univ_of_powerset_subset {A : Class} (hA : powerset A ⊆ A) : A = uni
 
 /-- The definite description operator, which is `{x}` if `{y | A y} = {x}` and `∅` otherwise. -/
 def iota (A : Class) : Class :=
-  ⋃₀ { x | ∀ y, A y ↔ y = x }
+  ⋃₀ ({ x | ∀ y, A y ↔ y = x } : Class)
 
 theorem iota_val (A : Class) (x : ZFSet) (H : ∀ y, A y ↔ y = x) : iota A = ↑x :=
   ext fun y =>

Mathlib/SetTheory/ZFC/PSet.lean

@@ -158,6 +158,24 @@ theorem Subset.congr_right : ∀ {x y z : PSet}, Equiv x y → (z ⊆ x ↔ z 
       let ⟨a, ab⟩ := βα b
       ⟨a, cb.trans (Equiv.symm ab)⟩⟩
 
+instance : Preorder PSet where
+  le := (· ⊆ ·)
+  le_refl := refl_of (· ⊆ ·)
+  le_trans _ _ _ := trans_of (· ⊆ ·)
+
+instance : HasSSubset PSet := ⟨(· < ·)⟩
+
+@[simp]
+theorem le_def (x y : PSet) : x ≤ y ↔ x ⊆ y :=
+  Iff.rfl
+
+@[simp]
+theorem lt_def (x y : PSet) : x < y ↔ x ⊂ y :=
+  Iff.rfl
+
+instance : IsNonstrictStrictOrder PSet (· ⊆ ·) (· ⊂ ·) :=
+  ⟨fun _ _ ↦ Iff.rfl⟩
+
 /-- `x ∈ y` as pre-sets if `x` is extensionally equivalent to a member of the family `y`. -/
 protected def Mem (y x : PSet.{u}) : Prop :=
   ∃ b, Equiv x (y.Func b)