Theorems · Inductive type · logic and foundations

ZFSet.IsOrdinal

ZFSet.{u_1} → Prop

A set x is a von Neumann ordinal when it's a transitive set, that's transitive under ∈. We prove that this further implies that x is well-ordered under ∈ in isOrdinal_iff_isWellOrder. The transitivity condition a ∈ b → b ∈ c → a ∈ c can be written without assuming a ∈ x and b ∈ x. The lemma isOrdinal_iff_isTrans shows this condition is equivalent to the usual one.

Defined in

Mathlib.SetTheory.ZFC.Ordinal

Cited by

34 results in Mathlib

Foundations

Depth 15 from the axioms · uses no axioms