Metamath Proof Explorer


Definition df-ord

Description: Define the ordinal predicate, which is true for a class that is transitive and is well-ordered by the membership relation. Variant of definition of BellMachover p. 468.

Some sources will define a notation for ordinal order corresponding to < and <_ but we just use e. and C_ respectively.

(Contributed by NM, 17-Sep-1993)

Ref Expression
Assertion df-ord ( Ord 𝐴 ↔ ( Tr 𝐴 ∧ E We 𝐴 ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA 𝐴
1 0 word Ord 𝐴
2 0 wtr Tr 𝐴
3 cep E
4 0 3 wwe E We 𝐴
5 2 4 wa ( Tr 𝐴 ∧ E We 𝐴 )
6 1 5 wb ( Ord 𝐴 ↔ ( Tr 𝐴 ∧ E We 𝐴 ) )