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
 |-  A
1 0 word
 |-  Ord A
2 0 wtr
 |-  Tr A
3 cep
 |-  _E
4 0 3 wwe
 |-  _E We A
5 2 4 wa
 |-  ( Tr A /\ _E We A )
6 1 5 wb
 |-  ( Ord A <-> ( Tr A /\ _E We A ) )