Theorem omex 4577

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 4573	. . 3 |- E. y ( (/) e. y /\ A. x e. y suc x e. y )
2		intexabim 4138	. . 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 4576	. . 3 |- om = |^| { y | ( (/) e. y /\ A. x e. y suc x e. y ) }
5	4	eleq1i 2236	. 2 |- ( om e. _V <-> |^| { y | ( (/) e. y /\ A. x e. y suc x e. y ) } e. _V )
6	3, 5	mpbir 145	1 |- om e. _V

Syntax hints:   /\ wa 103   E.wex 1485   e. wcel 2141   {cab 2156   A.wral 2448   _Vcvv 2730   (/)c0 3414   |^|cint 3831   suc csuc 4350   omcom 4574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152  ax-sep 4107  ax-iinf 4572

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ral 2453  df-v 2732  df-in 3127  df-ss 3134  df-int 3832  df-iom 4575

This theorem is referenced by:  peano5  4582  omelon  4593  frecex  6373  frecabex  6377  fict  6846  infnfi  6873  ominf  6874  inffiexmid  6884  omp1eom  7072  difinfsn  7077  0ct  7084  ctmlemr  7085  ctssdclemn0  7087  ctssdclemr  7089  ctssdc  7090  enumct  7092  omct  7094  ctfoex  7095  nninfex  7098  infnninf  7100  infnninfOLD  7101  nnnninf  7102  exmidlpo  7119  nninfdcinf  7147  nninfwlporlem  7149  nninfwlpoimlemg  7151  nninfwlpoim  7154  cc2lem  7228  niex  7274  enq0ex  7401  nq0ex  7402  uzenom  10381  frecfzennn  10382  nnenom  10390  fxnn0nninf  10394  0tonninf  10395  1tonninf  10396  inftonninf  10397  hashinfuni  10711  hashinfom  10712  xpct  12351  ennnfonelemj0  12356  ennnfonelemg  12358  ennnfonelemen  12376  ctiunct  12395  omctfn  12398  ssomct  12400  bj-charfunbi  13846  subctctexmid  14034  0nninf  14037  nnsf  14038  peano4nninf  14039  peano3nninf  14040  nninfself  14046  nninfsellemeq  14047  nninfsellemeqinf  14049  sbthom  14058