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 5645 | . 2 ⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴)) | |
2 | 1 | simp1bi 1069 | 1 ⊢ (Lim 𝐴 → Ord 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1475 ≠ wne 2780 ∅c0 3874 ∪ cuni 4372 Ord word 5639 Lim wlim 5641 |
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 196 df-an 385 df-3an 1033 df-lim 5645 |
This theorem is referenced by: 0ellim 5704 limelon 5705 nlimsucg 6934 ordzsl 6937 limsuc 6941 limsssuc 6942 limomss 6962 ordom 6966 limom 6972 tfr2b 7379 rdgsucg 7406 rdglimg 7408 rdglim2 7415 oesuclem 7492 odi 7546 omeulem1 7549 oelim2 7562 oeoalem 7563 oeoelem 7565 limenpsi 8020 limensuci 8021 ordtypelem3 8308 ordtypelem5 8310 ordtypelem6 8311 ordtypelem7 8312 ordtypelem9 8314 r1tr 8522 r1ordg 8524 r1ord3g 8525 r1pwss 8530 r1val1 8532 rankwflemb 8539 r1elwf 8542 rankr1ai 8544 rankr1ag 8548 rankr1bg 8549 unwf 8556 rankr1clem 8566 rankr1c 8567 rankval3b 8572 rankonidlem 8574 onssr1 8577 coflim 8966 cflim3 8967 cflim2 8968 cfss 8970 cfslb 8971 cfslbn 8972 cfslb2n 8973 r1limwun 9437 inar1 9476 rdgprc 30944 limsucncmpi 31614 |
Copyright terms: Public domain | W3C validator |