Theorems · Theorem · logic and foundations

ZFSet.isOrdinal_iff_isTrans

∀ {x : ZFSet.{u}}, x.IsOrdinal ↔ x.IsTransitive ∧ IsTrans (↥x) (Subrel (fun x1 x2 => x1 ∈ x2) fun x_1 => x_1 ∈ x)

The simplified form of transitivity used within IsOrdinal yields an equivalent definition to the standard one.

Defined in

Mathlib.SetTheory.ZFC.Ordinal

Cited by

3 results in Mathlib

Foundations

Depth 28 from the axioms · uses propext, Quot.sound