English
A set x is an ordinal iff x is transitive and the relation ∈ restricted to x is transitive.
Русский
Множество x является ординалом тогда и только тогда, когда x транзитивно и отношение ∈, ограниченное до x, транзитивно.
LaTeX
$$$IsOrdinal(x) \iff (IsTrans(x) \land IsTrans\_{Subrel(\in, \in x)})$$$
Lean4
/-- The simplified form of transitivity used within `IsOrdinal` yields an equivalent definition to
the standard one. -/
theorem _root_.ZFSet.isOrdinal_iff_isTrans : x.IsOrdinal ↔ x.IsTransitive ∧ IsTrans _ (Subrel (· ∈ ·) (· ∈ x))
where
mp h := ⟨h.isTransitive, h.isTrans⟩
mpr := by
rintro ⟨h₁, ⟨h₂⟩⟩
refine ⟨h₁, fun {y z w} hyz hzw hwx ↦ ?_⟩
have hzx := h₁.mem_trans hzw hwx
exact h₂ ⟨y, h₁.mem_trans hyz hzx⟩ ⟨z, hzx⟩ ⟨w, hwx⟩ hyz hzw
