Theorem 0ellim 3047

Description: A limit ordinal contains the empty set.

Assertion

Ref	Expression
0ellim	|- (Lim A -> (/) e. A)

Proof of Theorem 0ellim

Step	Hyp	Ref	Expression
1		nlim0 3043	. . . 4 |- -. Lim (/)
2		limeq 2976	. . . 4 |- (A = (/) -> (Lim A <-> Lim (/)))
3	1, 2	mtbiri 721	. . 3 |- (A = (/) -> -. Lim A)
4	3	necon2ai 1618	. 2 |- (Lim A -> A =/= (/))
5		limord 3044	. . 3 |- (Lim A -> Ord A)
6		ord0eln0 3039	. . 3 |- (Ord A -> ((/) e. A <-> A =/= (/)))
7	5, 6	syl 10	. 2 |- (Lim A -> ((/) e. A <-> A =/= (/)))
8	4, 7	mpbird 196	1 |- (Lim A -> (/) e. A)

Syntax hints:   -> wi 3   <-> wb 146   = wceq 960   e. wcel 962   =/= wne 1592  (/)c0 2291  Ord word 2963  Lim wlim 2965

This theorem is referenced by:  limuni3 3139  peano1 3165  oe1m 4195  oalimcl 4210  oaass 4211  oarec 4212  omlimcl 4225  odi 4226  oen0 4229  oewordri 4235  oelim2 4238  limensuci 4526  rankxplim2 4730  rankxplim3 4731

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 966  ax-gen 967  ax-8 968  ax-10 970  ax-11 971  ax-12 972  ax-13 973  ax-14 974  ax-17 975  ax-4 977  ax-5o 979  ax-6o 982  ax-9o 1127  ax-10o 1144  ax-16 1214  ax-11o 1222  ax-ext 1464  ax-sep 2718  ax-pow 2758  ax-pr 2795

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 780  df-3an 781  df-ex 985  df-sb 1176  df-eu 1386  df-mo 1387  df-clab 1470  df-cleq 1475  df-clel 1478  df-ne 1594  df-ral 1656  df-rex 1657  df-v 1819  df-dif 2060  df-un 2061  df-in 2062  df-ss 2064  df-nul 2292  df-pw 2414  df-sn 2424  df-pr 2425  df-op 2428  df-uni 2518  df-br 2635  df-opab 2682  df-tr 2696  df-eprel 2848  df-po 2856  df-so 2866  df-fr 2933  df-we 2950  df-ord 2967  df-lim 2969

Copyright terms: Public domain