![]() |
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 6375 | . 2 wff Ord 𝐴 |
3 | 1 | wtr 5270 | . . 3 wff Tr 𝐴 |
4 | cep 5585 | . . . 4 class E | |
5 | 1, 4 | wwe 5636 | . . 3 wff E We 𝐴 |
6 | 3, 5 | wa 394 | . 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 6383 ordwe 6389 ordtr 6390 trssord 6393 ordelord 6398 ord0 6429 ordon 7785 dford5 7792 dfrecs3 8402 dfrecs3OLD 8403 dford2 9663 smobeth 10629 gruina 10861 dford5reg 35606 dfon2 35616 oaun3lem1 43040 |
Copyright terms: Public domain | W3C validator |