Theorem omex 4642

Description: The existence of omega (the class of natural numbers). Axiom 7 of [TakeutiZaring] p. 43. (Contributed by NM, 6-Aug-1994.)

Assertion

Ref	Expression
omex	|- om e. _V

Proof of Theorem omex

Dummy variables x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		zfinf2 4638	. . 3 |- E. y ( (/) e. y /\ A. x e. y suc x e. y )
2		intexabim 4197	. . 3 |- ( E. y ( (/) e. y /\ A. x e. y suc x e. y ) -> |^| { y | ( (/) e. y /\ A. x e. y suc x e. y ) } e. _V )
3	1, 2	ax-mp 5	. 2 |- |^| { y | ( (/) e. y /\ A. x e. y suc x e. y ) } e. _V
4		dfom3 4641	. . 3 |- om = |^| { y | ( (/) e. y /\ A. x e. y suc x e. y ) }
5	4	eleq1i 2271	. 2 |- ( om e. _V <-> |^| { y | ( (/) e. y /\ A. x e. y suc x e. y ) } e. _V )
6	3, 5	mpbir 146	1 |- om e. _V

Syntax hints:   /\ wa 104   E.wex 1515   e. wcel 2176   {cab 2191   A.wral 2484   _Vcvv 2772   (/)c0 3460   |^|cint 3885   suc csuc 4413   omcom 4639

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187  ax-sep 4163  ax-iinf 4637

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-ral 2489  df-v 2774  df-in 3172  df-ss 3179  df-int 3886  df-iom 4640

This theorem is referenced by:  peano5  4647  omelon  4658  frecex  6482  frecabex  6486  fict  6967  infnfi  6994  ominf  6995  inffiexmid  7005  omp1eom  7199  difinfsn  7204  0ct  7211  ctmlemr  7212  ctssdclemn0  7214  ctssdclemr  7216  ctssdc  7217  enumct  7219  omct  7221  ctfoex  7222  nninfex  7225  infnninf  7228  infnninfOLD  7229  nnnninf  7230  exmidlpo  7247  nninfdcinf  7275  nninfwlporlem  7277  nninfwlpoimlemg  7279  nninfwlpoim  7283  nninfinfwlpo  7284  cc2lem  7380  acnccim  7386  niex  7427  enq0ex  7554  nq0ex  7555  uzenom  10572  frecfzennn  10573  nnenom  10581  fxnn0nninf  10586  0tonninf  10587  1tonninf  10588  inftonninf  10589  nninfinf  10590  hashinfuni  10924  hashinfom  10925  nninfctlemfo  12394  nninfct  12395  xpct  12800  ennnfonelemj0  12805  ennnfonelemg  12807  ennnfonelemen  12825  ctiunct  12844  omctfn  12847  ssomct  12849  bj-charfunbi  15784  subctctexmid  15974  0nninf  15978  nnsf  15979  peano4nninf  15980  peano3nninf  15981  nninfself  15987  nninfsellemeq  15988  nninfsellemeqinf  15990  sbthom  16002