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 6271 | . 2 ⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴)) | |
2 | 1 | simp1bi 1144 | 1 ⊢ (Lim 𝐴 → Ord 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1539 ≠ wne 2943 ∅c0 4256 ∪ cuni 4839 Ord word 6265 Lim wlim 6267 |
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 397 df-3an 1088 df-lim 6271 |
This theorem is referenced by: 0ellim 6328 limelon 6329 nlimsucg 7689 ordzsl 7692 limsuc 7696 limsssuc 7697 limomss 7717 trom 7721 limom 7728 tfr2b 8227 rdgsucg 8254 rdglimg 8256 rdglim2 8263 1ellim 8328 2ellim 8329 oesuclem 8355 odi 8410 omeulem1 8413 oelim2 8426 oeoalem 8427 oeoelem 8429 limenpsi 8939 limensuci 8940 ordtypelem3 9279 ordtypelem5 9281 ordtypelem6 9282 ordtypelem7 9283 ordtypelem9 9285 r1tr 9534 r1ordg 9536 r1ord3g 9537 r1pwss 9542 r1val1 9544 rankwflemb 9551 r1elwf 9554 rankr1ai 9556 rankr1ag 9560 rankr1bg 9561 unwf 9568 rankr1clem 9578 rankr1c 9579 rankval3b 9584 rankonidlem 9586 onssr1 9589 coflim 10017 cflim3 10018 cflim2 10019 cfss 10021 cfslb 10022 cfslbn 10023 cfslb2n 10024 r1limwun 10492 inar1 10531 rdgprc 33770 oldlim 34069 limsucncmpi 34634 grur1cld 41850 |
Copyright terms: Public domain | W3C validator |