![]() |
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 6361 | . 2 wff Ord 𝐴 |
3 | 1 | wtr 5265 | . . 3 wff Tr 𝐴 |
4 | cep 5579 | . . . 4 class E | |
5 | 1, 4 | wwe 5630 | . . 3 wff E We 𝐴 |
6 | 3, 5 | wa 397 | . 2 wff (Tr 𝐴 ∧ E We 𝐴) |
7 | 2, 6 | wb 205 | 1 wff (Ord 𝐴 ↔ (Tr 𝐴 ∧ E We 𝐴)) |
Colors of variables: wff setvar class |
This definition is referenced by: ordeq 6369 ordwe 6375 ordtr 6376 trssord 6379 ordelord 6384 ord0 6415 ordon 7761 dford5 7768 dfrecs3 8369 dfrecs3OLD 8370 dford2 9612 smobeth 10578 gruina 10810 dford5reg 34743 dfon2 34753 oaun3lem1 42110 |
Copyright terms: Public domain | W3C validator |