![]() |
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 5981 | . 2 ⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴)) | |
2 | 1 | simp1bi 1136 | 1 ⊢ (Lim 𝐴 → Ord 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1601 ≠ wne 2968 ∅c0 4140 ∪ cuni 4671 Ord word 5975 Lim wlim 5977 |
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 199 df-an 387 df-3an 1073 df-lim 5981 |
This theorem is referenced by: 0ellim 6038 limelon 6039 nlimsucg 7320 ordzsl 7323 limsuc 7327 limsssuc 7328 limomss 7348 ordom 7352 limom 7358 tfr2b 7775 rdgsucg 7802 rdglimg 7804 rdglim2 7811 oesuclem 7889 odi 7943 omeulem1 7946 oelim2 7959 oeoalem 7960 oeoelem 7962 limenpsi 8423 limensuci 8424 ordtypelem3 8714 ordtypelem5 8716 ordtypelem6 8717 ordtypelem7 8718 ordtypelem9 8720 r1tr 8936 r1ordg 8938 r1ord3g 8939 r1pwss 8944 r1val1 8946 rankwflemb 8953 r1elwf 8956 rankr1ai 8958 rankr1ag 8962 rankr1bg 8963 unwf 8970 rankr1clem 8980 rankr1c 8981 rankval3b 8986 rankonidlem 8988 onssr1 8991 coflim 9418 cflim3 9419 cflim2 9420 cfss 9422 cfslb 9423 cfslbn 9424 cfslb2n 9425 r1limwun 9893 inar1 9932 rdgprc 32302 limsucncmpi 33041 |
Copyright terms: Public domain | W3C validator |