![]() |
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 6374 | . 2 wff Ord 𝐴 |
3 | 1 | wtr 5263 | . . 3 wff Tr 𝐴 |
4 | cep 5577 | . . . 4 class E | |
5 | 1, 4 | wwe 5629 | . . 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 6382 ordwe 6388 ordtr 6389 trssord 6392 ordelord 6397 ord0 6428 ordon 7783 dford5 7790 dfrecs3 8398 dfrecs3OLD 8399 dford2 9644 smobeth 10610 gruina 10842 dford5reg 35719 dfon2 35729 oaun3lem1 43323 |
Copyright terms: Public domain | W3C validator |