feat(set_theory/zfc/ordinal): more lemmas on transitive sets (#18307)

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

src/set_theory/zfc/basic.lean

@@ -720,6 +720,19 @@ by { rw ←mem_to_set, simp }
 @[simp] theorem mem_diff {x y z : Set.{u}} : z ∈ x \ y ↔ z ∈ x ∧ z ∉ y :=
 @@mem_sep (λ z : Set.{u}, z ∉ y)
 
+@[simp] theorem sUnion_pair {x y : Set.{u}} : ⋃₀ ({x, y} : Set.{u}) = x ∪ y :=
+begin
+  ext,
+  simp_rw [mem_union, mem_sUnion, mem_pair],
+  split,
+  { rintro ⟨w, (rfl | rfl), hw⟩,
+    { exact or.inl hw },
+    { exact or.inr hw } },
+  { rintro (hz | hz),
+    { exact ⟨x, or.inl rfl, hz⟩ },
+    { exact ⟨y, or.inr rfl, hz⟩ } }
+end
+
 theorem mem_wf : @well_founded Set (∈) :=
 well_founded_lift₂_iff.mpr pSet.mem_wf
 

src/set_theory/zfc/ordinal.lean

@@ -60,6 +60,19 @@ theorem is_transitive.sUnion' (H : ∀ y ∈ x, is_transitive y) : (⋃₀ x).is
   exact mem_sUnion_of_mem ((H w hw).mem_trans hz hw') hw
 end
 
+protected theorem is_transitive.union (hx : x.is_transitive) (hy : y.is_transitive) :
+  (x ∪ y).is_transitive :=
+begin
+  rw ←sUnion_pair,
+  apply is_transitive.sUnion' (λ z, _),
+  rw mem_pair,
+  rintro (rfl | rfl),
+  assumption'
+end
+
+protected theorem is_transitive.powerset (h : x.is_transitive) : (powerset x).is_transitive :=
+λ y hy z hz, by { rw mem_powerset at ⊢ hy, exact h.subset_of_mem (hy hz) }
+
 theorem is_transitive_iff_sUnion_subset : x.is_transitive ↔ ⋃₀ x ⊆ x :=
 ⟨λ h y hy, by { rcases mem_sUnion.1 hy with ⟨z, hz, hz'⟩, exact h.mem_trans hz' hz },
   λ H y hy z hz, H $ mem_sUnion_of_mem hz hy⟩