![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 0ellim | Structured version Visualization version GIF version |
Description: A limit ordinal contains the empty set. (Contributed by NM, 15-May-1994.) |
Ref | Expression |
---|---|
0ellim | ⊢ (Lim 𝐴 → ∅ ∈ 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nlim0 6036 | . . . 4 ⊢ ¬ Lim ∅ | |
2 | limeq 5990 | . . . 4 ⊢ (𝐴 = ∅ → (Lim 𝐴 ↔ Lim ∅)) | |
3 | 1, 2 | mtbiri 319 | . . 3 ⊢ (𝐴 = ∅ → ¬ Lim 𝐴) |
4 | 3 | necon2ai 2998 | . 2 ⊢ (Lim 𝐴 → 𝐴 ≠ ∅) |
5 | limord 6037 | . . 3 ⊢ (Lim 𝐴 → Ord 𝐴) | |
6 | ord0eln0 6032 | . . 3 ⊢ (Ord 𝐴 → (∅ ∈ 𝐴 ↔ 𝐴 ≠ ∅)) | |
7 | 5, 6 | syl 17 | . 2 ⊢ (Lim 𝐴 → (∅ ∈ 𝐴 ↔ 𝐴 ≠ ∅)) |
8 | 4, 7 | mpbird 249 | 1 ⊢ (Lim 𝐴 → ∅ ∈ 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 = wceq 1601 ∈ wcel 2107 ≠ wne 2969 ∅c0 4141 Ord word 5977 Lim wlim 5979 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-13 2334 ax-ext 2754 ax-sep 5019 ax-nul 5027 ax-pr 5140 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-3or 1072 df-3an 1073 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-mo 2551 df-eu 2587 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-ne 2970 df-ral 3095 df-rex 3096 df-rab 3099 df-v 3400 df-sbc 3653 df-dif 3795 df-un 3797 df-in 3799 df-ss 3806 df-pss 3808 df-nul 4142 df-if 4308 df-pw 4381 df-sn 4399 df-pr 4401 df-op 4405 df-uni 4674 df-br 4889 df-opab 4951 df-tr 4990 df-eprel 5268 df-po 5276 df-so 5277 df-fr 5316 df-we 5318 df-ord 5981 df-lim 5983 |
This theorem is referenced by: limuni3 7332 peano1 7365 oe1m 7911 oalimcl 7926 oaass 7927 oarec 7928 omlimcl 7944 odi 7945 oen0 7952 oewordri 7958 oelim2 7961 oeoalem 7962 oeoelem 7964 limensuci 8426 rankxplim2 9042 rankxplim3 9043 r1limwun 9895 |
Copyright terms: Public domain | W3C validator |