Theorem omex 4259

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 4255	. . 3 |- E.y( (/) e. y /\ A.x e. y suc x e. y)
2		intexabim 3897	. . 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 7	. 2 |- |^| {y | ( (/) e. y /\ A.x e. y suc x e. y) } e. _V
4		dfom3 4258	. . 3 |- om = |^| {y | ( (/) e. y /\ A.x e. y suc x e. y) }
5	4	eleq1i 2100	. 2 |- ( om e. _V <-> |^| {y | ( (/) e. y /\ A.x e. y suc x e. y) } e. _V)
6	3, 5	mpbir 134	1 |- om e. _V

Syntax hints:   /\ wa 97  E.wex 1378   e. wcel 1390   {cab 2023  A.wral 2300   _Vcvv 2551   (/)c0 3218   |^|cint 3606   suc csuc 4068   omcom 4256

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bndl 1396  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-iinf 4254

This theorem depends on definitions:  df-bi 110  df-tru 1245  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-v 2553  df-in 2918  df-ss 2925  df-int 3607  df-iom 4257

This theorem is referenced by:  peano5  4264  omelon  4274  frecabex  5923  niex  6296  enq0ex  6422  nq0ex  6423  uzenom  8883  frecfzennn  8884  nnenom  8891