ZFSet.IsTransitive.mem_trans
theorem ZFSet.IsTransitive.mem_trans : ∀ {z : ZFSet}, z.IsTransitive → ∀ {x y : ZFSet}, x ∈ y → y ∈ z → x ∈ z := by
sorry
This theorem states that for any given ZFSet `z`, if `z` is a transitive set (in the sense that every element is a subset of `z`), then for any two other ZFSets `x` and `y`, if `x` is an element of `y` and `y` is an element of `z`, it follows that `x` is also an element of `z`. This theorem is an alias of the forward direction of `ZFSet.isTransitive_iff_mem_trans`.
More concisely: If `z` is a transitive ZFSet, then for all `x` and `y`, if `x` is an element of `y` and `y` is an element of `z`, then `x` is an element of `z`.
|
ZFSet.IsTransitive.subset_powerset
theorem ZFSet.IsTransitive.subset_powerset : ∀ {x : ZFSet}, x.IsTransitive → x ⊆ x.powerset
The theorem `ZFSet.IsTransitive.subset_powerset` states that for any set `x` in the ZFSet universe (which is the universe of sets in Zermelo-Fraenkel set theory), if `x` is transitive, then `x` is a subset of its powerset. In other words, every element of `x` is also an element of the powerset of `x` when `x` is a transitive set.
More concisely: If `x` is a transitive set in the ZFSet universe, then `x` is a subset of its powerset.
|
ZFSet.IsTransitive.subset_of_mem
theorem ZFSet.IsTransitive.subset_of_mem : ∀ {x y : ZFSet}, x.IsTransitive → y ∈ x → y ⊆ x
This theorem states that for any two sets `x` and `y` in the Zermelo-Fraenkel universe, if `x` is a transitive set (meaning every element of `x` is a subset of `x`) and `y` is an element of `x`, then `y` is a subset of `x`. In other words, if a set belongs to a transitive set, it is also a subset of that transitive set.
More concisely: If `x` is a transitive set and `y` is an element of `x`, then `y` is a subset of `x`.
|
ZFSet.IsTransitive.sUnion_subset
theorem ZFSet.IsTransitive.sUnion_subset : ∀ {x : ZFSet}, x.IsTransitive → x.sUnion ⊆ x
This theorem, referred to as an alias of the forward direction of `ZFSet.isTransitive_iff_sUnion_subset`, establishes that for any set `x` in the ZFSet universe, if `x` is a transitive set, then the union of the elements of `x` (denoted by `x.sUnion`) is a subset of `x`. In other words, every element of the union of the elements of a transitive set is itself a member of the set.
More concisely: If `x` is a transitive set, then `x.sUnion ⊆ x`.
|