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 6171 | . 2 ⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴)) | |
2 | 1 | simp1bi 1146 | 1 ⊢ (Lim 𝐴 → Ord 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1542 ≠ wne 2934 ∅c0 4209 ∪ cuni 4793 Ord word 6165 Lim wlim 6167 |
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 210 df-an 400 df-3an 1090 df-lim 6171 |
This theorem is referenced by: 0ellim 6228 limelon 6229 nlimsucg 7570 ordzsl 7573 limsuc 7577 limsssuc 7578 limomss 7598 ordom 7602 limom 7608 tfr2b 8054 rdgsucg 8081 rdglimg 8083 rdglim2 8090 oesuclem 8174 odi 8229 omeulem1 8232 oelim2 8245 oeoalem 8246 oeoelem 8248 limenpsi 8735 limensuci 8736 ordtypelem3 9050 ordtypelem5 9052 ordtypelem6 9053 ordtypelem7 9054 ordtypelem9 9056 r1tr 9271 r1ordg 9273 r1ord3g 9274 r1pwss 9279 r1val1 9281 rankwflemb 9288 r1elwf 9291 rankr1ai 9293 rankr1ag 9297 rankr1bg 9298 unwf 9305 rankr1clem 9315 rankr1c 9316 rankval3b 9321 rankonidlem 9323 onssr1 9326 coflim 9754 cflim3 9755 cflim2 9756 cfss 9758 cfslb 9759 cfslbn 9760 cfslb2n 9761 r1limwun 10229 inar1 10268 rdgprc 33334 oldlim 33699 limsucncmpi 34264 grur1cld 41376 |
Copyright terms: Public domain | W3C validator |