![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > limord | Structured version Visualization version GIF version |
Description: A limit ordinal is ordinal. (Contributed by NM, 4-May-1995.) |
Ref | Expression |
---|---|
limord | ⊢ (Lim 𝐴 → Ord 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-lim 6369 | . 2 ⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴)) | |
2 | 1 | simp1bi 1144 | 1 ⊢ (Lim 𝐴 → Ord 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1540 ≠ wne 2939 ∅c0 4322 ∪ cuni 4908 Ord word 6363 Lim wlim 6365 |
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 206 df-an 396 df-3an 1088 df-lim 6369 |
This theorem is referenced by: 0ellim 6427 limelon 6428 nlimsucg 7835 ordzsl 7838 limsuc 7842 limsssuc 7843 limomss 7864 trom 7868 limom 7875 tfr2b 8402 rdgsucg 8429 rdglimg 8431 rdglim2 8438 1ellim 8504 2ellim 8505 oesuclem 8531 odi 8585 omeulem1 8588 oelim2 8601 oeoalem 8602 oeoelem 8604 limenpsi 9158 limensuci 9159 ordtypelem3 9521 ordtypelem5 9523 ordtypelem6 9524 ordtypelem7 9525 ordtypelem9 9527 r1tr 9777 r1ordg 9779 r1ord3g 9780 r1pwss 9785 r1val1 9787 rankwflemb 9794 r1elwf 9797 rankr1ai 9799 rankr1ag 9803 rankr1bg 9804 unwf 9811 rankr1clem 9821 rankr1c 9822 rankval3b 9827 rankonidlem 9829 onssr1 9832 coflim 10262 cflim3 10263 cflim2 10264 cfss 10266 cfslb 10267 cfslbn 10268 cfslb2n 10269 r1limwun 10737 inar1 10776 oldlim 27727 rdgprc 35237 limsucncmpi 35796 limexissup 42496 limexissupab 42498 oaltublim 42505 omord2lim 42515 dflim5 42544 grur1cld 43456 |
Copyright terms: Public domain | W3C validator |