Theorem 0ellim 6404

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 6400	. . . 4 ⊢ ¬ Lim ∅
2		limeq 6352	. . . 4 ⊢ (𝐴 = ∅ → (Lim 𝐴 ↔ Lim ∅))
3	1, 2	mtbiri 327	. . 3 ⊢ (𝐴 = ∅ → ¬ Lim 𝐴)
4	3	necon2ai 2956	. 2 ⊢ (Lim 𝐴 → 𝐴 ≠ ∅)
5		limord 6401	. . 3 ⊢ (Lim 𝐴 → Ord 𝐴)
6		ord0eln0 6396	. . 3 ⊢ (Ord 𝐴 → (∅ ∈ 𝐴 ↔ 𝐴 ≠ ∅))
7	5, 6	syl 17	. 2 ⊢ (Lim 𝐴 → (∅ ∈ 𝐴 ↔ 𝐴 ≠ ∅))
8	4, 7	mpbird 257	1 ⊢ (Lim 𝐴 → ∅ ∈ 𝐴)

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2109   ≠ wne 2927  ∅c0 4304  Ord word 6339  Lim wlim 6341

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-sep 5259  ax-nul 5269  ax-pr 5395

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ne 2928  df-ral 3047  df-rex 3056  df-rab 3412  df-v 3457  df-dif 3925  df-un 3927  df-in 3929  df-ss 3939  df-pss 3942  df-nul 4305  df-if 4497  df-pw 4573  df-sn 4598  df-pr 4600  df-op 4604  df-uni 4880  df-br 5116  df-opab 5178  df-tr 5223  df-eprel 5546  df-po 5554  df-so 5555  df-fr 5599  df-we 5601  df-ord 6343  df-lim 6345

This theorem is referenced by:  limuni3  7836  peano1  7873  peano1OLD  7874  oe1m  8520  oalimcl  8535  oaass  8536  oarec  8537  omlimcl  8553  odi  8554  oen0  8561  oewordri  8567  oelim2  8570  oeoalem  8571  oeoelem  8573  limensuci  9130  rankxplim2  9851  rankxplim3  9852  r1limwun  10707  constr01  33740  omlimcl2  43203  oe0suclim  43238