Theorem omex 4659

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 4655	. . 3 |- E. y ( (/) e. y /\ A. x e. y suc x e. y )
2		intexabim 4212	. . 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 4658	. . 3 |- om = |^| { y | ( (/) e. y /\ A. x e. y suc x e. y ) }
5	4	eleq1i 2273	. 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 1516   e. wcel 2178   {cab 2193   A.wral 2486   _Vcvv 2776   (/)c0 3468   |^|cint 3899   suc csuc 4430   omcom 4656

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189  ax-sep 4178  ax-iinf 4654

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-ral 2491  df-v 2778  df-in 3180  df-ss 3187  df-int 3900  df-iom 4657

This theorem is referenced by:  peano5  4664  omelon  4675  frecex  6503  frecabex  6507  fict  6991  infnfi  7018  ominf  7019  inffiexmid  7029  omp1eom  7223  difinfsn  7228  0ct  7235  ctmlemr  7236  ctssdclemn0  7238  ctssdclemr  7240  ctssdc  7241  enumct  7243  omct  7245  ctfoex  7246  nninfex  7249  infnninf  7252  infnninfOLD  7253  nnnninf  7254  exmidlpo  7271  nninfdcinf  7299  nninfwlporlem  7301  nninfwlpoimlemg  7303  nninfwlpoim  7307  nninfinfwlpo  7308  cc2lem  7413  acnccim  7419  niex  7460  enq0ex  7587  nq0ex  7588  uzenom  10607  frecfzennn  10608  nnenom  10616  fxnn0nninf  10621  0tonninf  10622  1tonninf  10623  inftonninf  10624  nninfinf  10625  hashinfuni  10959  hashinfom  10960  nninfctlemfo  12476  nninfct  12477  xpct  12882  ennnfonelemj0  12887  ennnfonelemg  12889  ennnfonelemen  12907  ctiunct  12926  omctfn  12929  ssomct  12931  bj-charfunbi  15946  subctctexmid  16139  0nninf  16143  nnsf  16144  peano4nninf  16145  peano3nninf  16146  nninfself  16152  nninfsellemeq  16153  nninfsellemeqinf  16155  sbthom  16167