Theorem 0ellim 6427

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		dflim2 6421	. 2 ⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ ∅ ∈ 𝐴 ∧ 𝐴 = ∪ 𝐴))
2	1	simp2bi 1164	1 ⊢ (Lim 𝐴 → ∅ ∈ 𝐴)

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144  ∅c0 4278  ∪ cuni 4866  Ord word 6361  Lim wlim 6363

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-tr 5212  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-ord 6365  df-lim 6367

This theorem is used by:  limuni3  7864  peano1  7901  oe1m  8557  oalimcl  8572  oaass  8573  oarec  8574  omlimcl  8590  odi  8591  oen0  8599  oewordri  8605  oelim2  8608  oeoalem  8609  oeoelem  8611  limensuci  9176  rankxplim2  9901  rankxplim3  9902  rankfilimbi  9906  r1limwun  10825  constr01  34421  r11  35778  omlimcl2  44338  oe0suclim  44373