|   | 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 6388 | . 2 ⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴)) | |
| 2 | 1 | simp1bi 1145 | 1 ⊢ (Lim 𝐴 → Ord 𝐴) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 = wceq 1539 ≠ wne 2939 ∅c0 4332 ∪ cuni 4906 Ord word 6382 Lim wlim 6384 | 
| 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 207 df-an 396 df-3an 1088 df-lim 6388 | 
| This theorem is referenced by: 0ellim 6446 limelon 6447 nlimsucg 7864 ordzsl 7867 limsuc 7871 limsssuc 7872 limomss 7893 trom 7897 limom 7904 tfr2b 8437 rdgsucg 8464 rdglimg 8466 rdglim2 8473 1ellim 8537 2ellim 8538 oesuclem 8564 odi 8618 omeulem1 8621 oelim2 8634 oeoalem 8635 oeoelem 8637 limenpsi 9193 limensuci 9194 ordtypelem3 9561 ordtypelem5 9563 ordtypelem6 9564 ordtypelem7 9565 ordtypelem9 9567 r1tr 9817 r1ordg 9819 r1ord3g 9820 r1pwss 9825 r1val1 9827 rankwflemb 9834 r1elwf 9837 rankr1ai 9839 rankr1ag 9843 rankr1bg 9844 unwf 9851 rankr1clem 9861 rankr1c 9862 rankval3b 9867 rankonidlem 9869 onssr1 9872 coflim 10302 cflim3 10303 cflim2 10304 cfss 10306 cfslb 10307 cfslbn 10308 cfslb2n 10309 r1limwun 10777 inar1 10816 oldlim 27926 rdgprc 35796 limsucncmpi 36447 limexissup 43299 limexissupab 43301 oaltublim 43308 omord2lim 43318 dflim5 43347 grur1cld 44256 | 
| Copyright terms: Public domain | W3C validator |