Theorem 0ellim 6439

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 6435	. . . 4 ⊢ ¬ Lim ∅
2		limeq 6388	. . . 4 ⊢ (𝐴 = ∅ → (Lim 𝐴 ↔ Lim ∅))
3	1, 2	mtbiri 326	. . 3 ⊢ (𝐴 = ∅ → ¬ Lim 𝐴)
4	3	necon2ai 2960	. 2 ⊢ (Lim 𝐴 → 𝐴 ≠ ∅)
5		limord 6436	. . 3 ⊢ (Lim 𝐴 → Ord 𝐴)
6		ord0eln0 6431	. . 3 ⊢ (Ord 𝐴 → (∅ ∈ 𝐴 ↔ 𝐴 ≠ ∅))
7	5, 6	syl 17	. 2 ⊢ (Lim 𝐴 → (∅ ∈ 𝐴 ↔ 𝐴 ≠ ∅))
8	4, 7	mpbird 256	1 ⊢ (Lim 𝐴 → ∅ ∈ 𝐴)

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1534   ∈ wcel 2099   ≠ wne 2930  ∅c0 4325  Ord word 6375  Lim wlim 6377

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697  ax-sep 5304  ax-nul 5311  ax-pr 5433

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-ne 2931  df-ral 3052  df-rex 3061  df-rab 3420  df-v 3464  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3967  df-nul 4326  df-if 4534  df-pw 4609  df-sn 4634  df-pr 4636  df-op 4640  df-uni 4914  df-br 5154  df-opab 5216  df-tr 5271  df-eprel 5586  df-po 5594  df-so 5595  df-fr 5637  df-we 5639  df-ord 6379  df-lim 6381

This theorem is referenced by:  limuni3  7862  peano1  7900  peano1OLD  7901  oe1m  8575  oalimcl  8590  oaass  8591  oarec  8592  omlimcl  8608  odi  8609  oen0  8616  oewordri  8622  oelim2  8625  oeoalem  8626  oeoelem  8628  limensuci  9191  rankxplim2  9923  rankxplim3  9924  r1limwun  10779  constr01  33600  omlimcl2  42907  oe0suclim  42943