![]() |
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 5445 |
. 2
![]() ![]() ![]() |
3 | 1 | wtr 4513 |
. . 3
![]() ![]() ![]() |
4 | cep 4765 |
. . . 4
![]() ![]() | |
5 | 1, 4 | wwe 4814 |
. . 3
![]() ![]() ![]() ![]() |
6 | 3, 5 | wa 375 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 2, 6 | wb 189 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
This definition is referenced by: ordeq 5453 ordwe 5459 ordtr 5460 trssord 5463 ordelord 5468 ord0 5498 ordon 6641 dfrecs3 7122 dford2 8156 smobeth 9042 gruina 9274 dford5reg 30478 dfon2 30488 |
Copyright terms: Public domain | W3C validator |