![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > limord | Structured version Visualization version Unicode version |
Description: A limit ordinal is ordinal. (Contributed by NM, 4-May-1995.) |
Ref | Expression |
---|---|
limord |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-lim 5431 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | simp1bi 1024 |
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 |
This theorem depends on definitions: df-bi 189 df-an 373 df-3an 988 df-lim 5431 |
This theorem is referenced by: 0ellim 5488 limelon 5489 nlimsucg 6674 ordzsl 6677 limsuc 6681 limsssuc 6682 limomss 6702 ordom 6706 limom 6712 tfr2b 7119 rdgsucg 7146 rdglimg 7148 rdglim2 7155 oesuclem 7232 odi 7285 omeulem1 7288 oelim2 7301 oeoalem 7302 oeoelem 7304 limenpsi 7752 limensuci 7753 ordtypelem3 8040 ordtypelem5 8042 ordtypelem6 8043 ordtypelem7 8044 ordtypelem9 8046 r1tr 8252 r1ordg 8254 r1ord3g 8255 r1pwss 8260 r1val1 8262 rankwflemb 8269 r1elwf 8272 rankr1ai 8274 rankr1ag 8278 rankr1bg 8279 unwf 8286 rankr1clem 8296 rankr1c 8297 rankval3b 8302 rankonidlem 8304 onssr1 8307 coflim 8696 cflim3 8697 cflim2 8698 cfss 8700 cfslb 8701 cfslbn 8702 cfslb2n 8703 r1limwun 9166 inar1 9205 rdgprc 30453 limsucncmpi 31117 |
Copyright terms: Public domain | W3C validator |