Theorem 0ellim 6091

Description: A limit ordinal contains the empty set. (Contributed by NM, 15-May-1994.)

Assertion

Ref	Expression
0ellim	⊢ (Lim 𝐴 → ∅ ∈ 𝐴)

Proof of Theorem 0ellim

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 𝐴 → ∅ ∈ 𝐴)

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