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

We add `empty_is_transitive`, `is_transitive.inter`, and `is_transitive.sUnion'`. We also add a `variables` block.

Author: vihdzp

src/set_theory/zfc/ordinal.lean

@@ -26,32 +26,47 @@ Further development can be found on the branch `von_neumann_v2`.
   `set_theory/ordinal/arithmetic.lean`.
 -/
 
+universe u
+
+variables {x y z : Set.{u}}
+
 namespace Set
 
 /-- A transitive set is one where every element is a subset. -/
 def is_transitive (x : Set) : Prop := ∀ y ∈ x, y ⊆ x
 
-theorem is_transitive.subset_of_mem {x y : Set} (h : x.is_transitive) : y ∈ x → y ⊆ x := h y
+@[simp] theorem empty_is_transitive : is_transitive ∅ := λ y hy, (mem_empty y hy).elim
 
-theorem is_transitive_iff_mem_trans {z : Set} :
-  z.is_transitive ↔ ∀ {x y : Set}, x ∈ y → y ∈ z → x ∈ z :=
+theorem is_transitive.subset_of_mem (h : x.is_transitive) : y ∈ x → y ⊆ x := h y
+
+theorem is_transitive_iff_mem_trans : z.is_transitive ↔ ∀ {x y : Set}, x ∈ y → y ∈ z → x ∈ z :=
 ⟨λ h x y hx hy, h.subset_of_mem hy hx, λ H x hx y hy, H hy hx⟩
 
 alias is_transitive_iff_mem_trans ↔ is_transitive.mem_trans _
 
-theorem is_transitive.sUnion {x : Set} (h : x.is_transitive) : (⋃₀ x).is_transitive :=
+protected theorem is_transitive.inter (hx : x.is_transitive) (hy : y.is_transitive) :
+  (x ∩ y).is_transitive :=
+λ z hz w hw, by { rw mem_inter at hz ⊢, exact ⟨hx.mem_trans hw hz.1, hy.mem_trans hw hz.2⟩ }
+
+protected theorem is_transitive.sUnion (h : x.is_transitive) : (⋃₀ x).is_transitive :=
 λ y hy z hz, begin
   rcases mem_sUnion.1 hy with ⟨w, hw, hw'⟩,
   exact mem_sUnion_of_mem hz (h.mem_trans hw' hw)
 end
 
-theorem is_transitive_iff_sUnion_subset {x : Set} : x.is_transitive ↔ ⋃₀ x ⊆ x :=
+theorem is_transitive.sUnion' (H : ∀ y ∈ x, is_transitive y) : (⋃₀ x).is_transitive :=
+λ y hy z hz, begin
+  rcases mem_sUnion.1 hy with ⟨w, hw, hw'⟩,
+  exact mem_sUnion_of_mem ((H w hw).mem_trans hz hw') hw
+end
+
+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⟩
 
 alias is_transitive_iff_sUnion_subset ↔ is_transitive.sUnion_subset _
 
-theorem is_transitive_iff_subset_powerset {x : Set} : x.is_transitive ↔ x ⊆ powerset x :=
+theorem is_transitive_iff_subset_powerset : x.is_transitive ↔ x ⊆ powerset x :=
 ⟨λ h y hy, mem_powerset.2 $ h.subset_of_mem hy, λ H y hy z hz, mem_powerset.1 (H hy) hz⟩
 
 alias is_transitive_iff_subset_powerset ↔ is_transitive.subset_powerset _