| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > df-ord | Structured version Visualization version GIF version | ||
| 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 ∈ and ⊆ respectively. (Contributed by NM, 17-Sep-1993.) |
| Ref | Expression |
|---|---|
| df-ord | ⊢ (Ord 𝐴 ↔ (Tr 𝐴 ∧ E We 𝐴)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cA | . . 3 class 𝐴 | |
| 2 | 1 | word 6381 | . 2 wff Ord 𝐴 |
| 3 | 1 | wtr 5257 | . . 3 wff Tr 𝐴 |
| 4 | cep 5581 | . . . 4 class E | |
| 5 | 1, 4 | wwe 5634 | . . 3 wff E We 𝐴 |
| 6 | 3, 5 | wa 395 | . 2 wff (Tr 𝐴 ∧ E We 𝐴) |
| 7 | 2, 6 | wb 206 | 1 wff (Ord 𝐴 ↔ (Tr 𝐴 ∧ E We 𝐴)) |
| Colors of variables: wff setvar class |
| This definition is referenced by: ordeq 6389 ordwe 6395 ordtr 6396 trssord 6399 ordelord 6404 ord0 6435 ordon 7793 dford5 7800 dfrecs3 8408 dfrecs3OLD 8409 dford2 9656 smobeth 10622 gruina 10854 dford5reg 35761 dfon2 35771 oaun3lem1 43365 |
| Copyright terms: Public domain | W3C validator |