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 5728 | . 2 | |
2 | 1 | simp1bi 1076 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wceq 1483 wne 2794 c0 3915 cuni 4436 word 5722 wlim 5724 |
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 197 df-an 386 df-3an 1039 df-lim 5728 |
This theorem is referenced by: 0ellim 5787 limelon 5788 nlimsucg 7042 ordzsl 7045 limsuc 7049 limsssuc 7050 limomss 7070 ordom 7074 limom 7080 tfr2b 7492 rdgsucg 7519 rdglimg 7521 rdglim2 7528 oesuclem 7605 odi 7659 omeulem1 7662 oelim2 7675 oeoalem 7676 oeoelem 7678 limenpsi 8135 limensuci 8136 ordtypelem3 8425 ordtypelem5 8427 ordtypelem6 8428 ordtypelem7 8429 ordtypelem9 8431 r1tr 8639 r1ordg 8641 r1ord3g 8642 r1pwss 8647 r1val1 8649 rankwflemb 8656 r1elwf 8659 rankr1ai 8661 rankr1ag 8665 rankr1bg 8666 unwf 8673 rankr1clem 8683 rankr1c 8684 rankval3b 8689 rankonidlem 8691 onssr1 8694 coflim 9083 cflim3 9084 cflim2 9085 cfss 9087 cfslb 9088 cfslbn 9089 cfslb2n 9090 r1limwun 9558 inar1 9597 rdgprc 31700 limsucncmpi 32444 |
Copyright terms: Public domain | W3C validator |