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. (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