Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-ord | Structured version Visualization version Unicode version |
Description: Define the ordinal predicate, which is true for a class that is transitive and is well-ordered by the epsilon relation. Variant of definition of [BellMachover] p. 468. (Contributed by NM, 17-Sep-1993.) |
Ref | Expression |
---|---|
df-ord |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 | |
2 | 1 | word 5722 | . 2 |
3 | 1 | wtr 4752 | . . 3 |
4 | cep 5028 | . . . 4 | |
5 | 1, 4 | wwe 5072 | . . 3 |
6 | 3, 5 | wa 384 | . 2 |
7 | 2, 6 | wb 196 | 1 |
Colors of variables: wff setvar class |
This definition is referenced by: ordeq 5730 ordwe 5736 ordtr 5737 trssord 5740 ordelord 5745 ord0 5777 ordon 6982 dfrecs3 7469 dford2 8517 smobeth 9408 gruina 9640 dford5 31608 dford5reg 31687 dfon2 31697 |
Copyright terms: Public domain | W3C validator |