![]() |
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 6087 | . . . 4 ⊢ ¬ Lim ∅ | |
2 | limeq 6041 | . . . 4 ⊢ (𝐴 = ∅ → (Lim 𝐴 ↔ Lim ∅)) | |
3 | 1, 2 | mtbiri 319 | . . 3 ⊢ (𝐴 = ∅ → ¬ Lim 𝐴) |
4 | 3 | necon2ai 2996 | . 2 ⊢ (Lim 𝐴 → 𝐴 ≠ ∅) |
5 | limord 6088 | . . 3 ⊢ (Lim 𝐴 → Ord 𝐴) | |
6 | ord0eln0 6083 | . . 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 1507 ∈ wcel 2050 ≠ wne 2967 ∅c0 4178 Ord word 6028 Lim wlim 6030 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-13 2301 ax-ext 2750 ax-sep 5060 ax-nul 5067 ax-pr 5186 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3or 1069 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-mo 2547 df-eu 2584 df-clab 2759 df-cleq 2771 df-clel 2846 df-nfc 2918 df-ne 2968 df-ral 3093 df-rex 3094 df-rab 3097 df-v 3417 df-sbc 3682 df-dif 3832 df-un 3834 df-in 3836 df-ss 3843 df-pss 3845 df-nul 4179 df-if 4351 df-pw 4424 df-sn 4442 df-pr 4444 df-op 4448 df-uni 4713 df-br 4930 df-opab 4992 df-tr 5031 df-eprel 5317 df-po 5326 df-so 5327 df-fr 5366 df-we 5368 df-ord 6032 df-lim 6034 |
This theorem is referenced by: limuni3 7383 peano1 7416 oe1m 7972 oalimcl 7987 oaass 7988 oarec 7989 omlimcl 8005 odi 8006 oen0 8013 oewordri 8019 oelim2 8022 oeoalem 8023 oeoelem 8025 limensuci 8489 rankxplim2 9103 rankxplim3 9104 r1limwun 9956 |
Copyright terms: Public domain | W3C validator |