![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ordtr1 | Structured version Visualization version Unicode version |
Description: Transitive law for ordinal classes. (Contributed by NM, 12-Dec-2004.) |
Ref | Expression |
---|---|
ordtr1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ordtr 5437 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | trel 4504 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl 17 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-10 1915 ax-11 1920 ax-12 1933 ax-13 2091 ax-ext 2431 |
This theorem depends on definitions: df-bi 189 df-an 373 df-tru 1447 df-ex 1664 df-nf 1668 df-sb 1798 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2581 df-v 3047 df-in 3411 df-ss 3418 df-uni 4199 df-tr 4498 df-ord 5426 |
This theorem is referenced by: ontr1 5469 dfsmo2 7066 smores2 7073 smoel 7079 smogt 7086 ordiso2 8030 r1ordg 8249 r1pwss 8255 r1val1 8257 rankr1ai 8269 rankval3b 8297 rankonidlem 8299 onssr1 8302 cofsmo 8699 fpwwe2lem9 9063 bnj1098 29595 bnj594 29723 |
Copyright terms: Public domain | W3C validator |