![]() |
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 6391 | . 2 ⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴)) | |
2 | 1 | simp1bi 1144 | 1 ⊢ (Lim 𝐴 → Ord 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1537 ≠ wne 2938 ∅c0 4339 ∪ cuni 4912 Ord word 6385 Lim wlim 6387 |
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 207 df-an 396 df-3an 1088 df-lim 6391 |
This theorem is referenced by: 0ellim 6449 limelon 6450 nlimsucg 7863 ordzsl 7866 limsuc 7870 limsssuc 7871 limomss 7892 trom 7896 limom 7903 tfr2b 8435 rdgsucg 8462 rdglimg 8464 rdglim2 8471 1ellim 8535 2ellim 8536 oesuclem 8562 odi 8616 omeulem1 8619 oelim2 8632 oeoalem 8633 oeoelem 8635 limenpsi 9191 limensuci 9192 ordtypelem3 9558 ordtypelem5 9560 ordtypelem6 9561 ordtypelem7 9562 ordtypelem9 9564 r1tr 9814 r1ordg 9816 r1ord3g 9817 r1pwss 9822 r1val1 9824 rankwflemb 9831 r1elwf 9834 rankr1ai 9836 rankr1ag 9840 rankr1bg 9841 unwf 9848 rankr1clem 9858 rankr1c 9859 rankval3b 9864 rankonidlem 9866 onssr1 9869 coflim 10299 cflim3 10300 cflim2 10301 cfss 10303 cfslb 10304 cfslbn 10305 cfslb2n 10306 r1limwun 10774 inar1 10813 oldlim 27940 rdgprc 35776 limsucncmpi 36428 limexissup 43271 limexissupab 43273 oaltublim 43280 omord2lim 43290 dflim5 43319 grur1cld 44228 |
Copyright terms: Public domain | W3C validator |