ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  omex Unicode version

Theorem omex 4475
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.
StepHypRef Expression
1 zfinf2 4471 . . 3  |-  E. y
( (/)  e.  y  /\  A. x  e.  y  suc  x  e.  y )
2 intexabim 4045 . . 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 )
31, 2ax-mp 5 . 2  |-  |^| { y  |  ( (/)  e.  y  /\  A. x  e.  y  suc  x  e.  y ) }  e.  _V
4 dfom3 4474 . . 3  |-  om  =  |^| { y  |  (
(/)  e.  y  /\  A. x  e.  y  suc  x  e.  y ) }
54eleq1i 2181 . 2  |-  ( om  e.  _V  <->  |^| { y  |  ( (/)  e.  y  /\  A. x  e.  y  suc  x  e.  y ) }  e.  _V )
63, 5mpbir 145 1  |-  om  e.  _V
Colors of variables: wff set class
Syntax hints:    /\ wa 103   E.wex 1451    e. wcel 1463   {cab 2101   A.wral 2391   _Vcvv 2658   (/)c0 3331   |^|cint 3739   suc csuc 4255   omcom 4472
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 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097  ax-sep 4014  ax-iinf 4470
This theorem depends on definitions:  df-bi 116  df-tru 1317  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2245  df-ral 2396  df-v 2660  df-in 3045  df-ss 3052  df-int 3740  df-iom 4473
This theorem is referenced by:  peano5  4480  omelon  4490  frecex  6257  frecabex  6261  fict  6728  infnfi  6755  ominf  6756  inffiexmid  6766  omp1eom  6946  difinfsn  6951  0ct  6958  ctmlemr  6959  ctssdclemn0  6961  ctssdclemr  6963  ctssdc  6964  enumct  6966  omct  6968  ctfoex  6969  exmidlpo  6981  infnninf  6988  nnnninf  6989  niex  7084  enq0ex  7211  nq0ex  7212  uzenom  10138  frecfzennn  10139  nnenom  10147  fxnn0nninf  10151  0tonninf  10152  1tonninf  10153  inftonninf  10154  hashinfuni  10463  hashinfom  10464  xpct  11804  ennnfonelemj0  11809  ennnfonelemg  11811  ennnfonelemen  11829  ctiunct  11848  subctctexmid  13007  0nninf  13008  nnsf  13010  peano4nninf  13011  peano3nninf  13012  nninfex  13016  nninfself  13020  nninfsellemeq  13021  nninfsellemeqinf  13023  sbthom  13032
  Copyright terms: Public domain W3C validator