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 6190 | . 2 ⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴)) | |
2 | 1 | simp1bi 1137 | 1 ⊢ (Lim 𝐴 → Ord 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1528 ≠ wne 3016 ∅c0 4290 ∪ cuni 4832 Ord word 6184 Lim wlim 6186 |
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 208 df-an 397 df-3an 1081 df-lim 6190 |
This theorem is referenced by: 0ellim 6247 limelon 6248 nlimsucg 7545 ordzsl 7548 limsuc 7552 limsssuc 7553 limomss 7573 ordom 7577 limom 7583 tfr2b 8023 rdgsucg 8050 rdglimg 8052 rdglim2 8059 oesuclem 8141 odi 8195 omeulem1 8198 oelim2 8211 oeoalem 8212 oeoelem 8214 limenpsi 8681 limensuci 8682 ordtypelem3 8973 ordtypelem5 8975 ordtypelem6 8976 ordtypelem7 8977 ordtypelem9 8979 r1tr 9194 r1ordg 9196 r1ord3g 9197 r1pwss 9202 r1val1 9204 rankwflemb 9211 r1elwf 9214 rankr1ai 9216 rankr1ag 9220 rankr1bg 9221 unwf 9228 rankr1clem 9238 rankr1c 9239 rankval3b 9244 rankonidlem 9246 onssr1 9249 coflim 9672 cflim3 9673 cflim2 9674 cfss 9676 cfslb 9677 cfslbn 9678 cfslb2n 9679 r1limwun 10147 inar1 10186 rdgprc 32937 limsucncmpi 33691 grur1cld 40448 |
Copyright terms: Public domain | W3C validator |