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 A Tr A E We A

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA class A
1 0 word wff Ord A
2 0 wtr wff Tr A
3 cep class E
4 0 3 wwe wff E We A
5 2 4 wa wff Tr A E We A
6 1 5 wb wff Ord A Tr A E We A