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 ) ) |
| 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 ) ) |