Theorem dfnn2 10655

Description: Alternate definition of the set of positive integers. This was our original definition, before the current df-nn 10643 replaced it. This definition requires the axiom of infinity to ensure it has the properties we expect. (Contributed by Jeff Hankins, 12-Sep-2013.) (Revised by Mario Carneiro, 3-May-2014.)

Assertion

Ref	Expression
dfnn2	|- NN = |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }

Distinct variable group:   x, y

Proof of Theorem dfnn2

Dummy variable z is distinct from all other variables.

Step	Hyp	Ref	Expression
1		1ex 9669	. . . . 5 |- 1 e. _V
2	1	elintab 4259	. . . 4 |- ( 1 e. |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } <-> A. x ( ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) -> 1 e. x ) )
3		simpl 463	. . . 4 |- ( ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) -> 1 e. x )
4	2, 3	mpgbir 1684	. . 3 |- 1 e. |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }
5		oveq1 6327	. . . . . . . . . 10 |- ( y = z -> ( y + 1 ) = ( z + 1 ) )
6	5	eleq1d 2524	. . . . . . . . 9 |- ( y = z -> ( ( y + 1 ) e. x <-> ( z + 1 ) e. x ) )
7	6	rspccv 3159	. . . . . . . 8 |- ( A. y e. x ( y + 1 ) e. x -> ( z e. x -> ( z + 1 ) e. x ) )
8	7	adantl 472	. . . . . . 7 |- ( ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) -> ( z e. x -> ( z + 1 ) e. x ) )
9	8	a2i 14	. . . . . 6 |- ( ( ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) -> z e. x ) -> ( ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) -> ( z + 1 ) e. x ) )
10	9	alimi 1695	. . . . 5 |- ( A. x ( ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) -> z e. x ) -> A. x ( ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) -> ( z + 1 ) e. x ) )
11		vex 3060	. . . . . 6 |- z e. _V
12	11	elintab 4259	. . . . 5 |- ( z e. |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } <-> A. x ( ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) -> z e. x ) )
13		ovex 6348	. . . . . 6 |- ( z + 1 ) e. _V
14	13	elintab 4259	. . . . 5 |- ( ( z + 1 ) e. |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } <-> A. x ( ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) -> ( z + 1 ) e. x ) )
15	10, 12, 14	3imtr4i 274	. . . 4 |- ( z e. |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } -> ( z + 1 ) e. |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } )
16	15	rgen 2759	. . 3 |- A. z e. |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } ( z + 1 ) e. |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }
17		peano5nni 10645	. . 3 |- ( ( 1 e. |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } /\ A. z e. |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } ( z + 1 ) e. |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } ) -> NN C_ |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } )
18	4, 16, 17	mp2an 683	. 2 |- NN C_ |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }
19		1nn 10653	. . . 4 |- 1 e. NN
20		peano2nn 10654	. . . . 5 |- ( y e. NN -> ( y + 1 ) e. NN )
21	20	rgen 2759	. . . 4 |- A. y e. NN ( y + 1 ) e. NN
22		nnex 10648	. . . . 5 |- NN e. _V
23		eleq2 2529	. . . . . 6 |- ( x = NN -> ( 1 e. x <-> 1 e. NN ) )
24		eleq2 2529	. . . . . . 7 |- ( x = NN -> ( ( y + 1 ) e. x <-> ( y + 1 ) e. NN ) )
25	24	raleqbi1dv 3007	. . . . . 6 |- ( x = NN -> ( A. y e. x ( y + 1 ) e. x <-> A. y e. NN ( y + 1 ) e. NN ) )
26	23, 25	anbi12d 722	. . . . 5 |- ( x = NN -> ( ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) <-> ( 1 e. NN /\ A. y e. NN ( y + 1 ) e. NN ) ) )
27	22, 26	elab 3197	. . . 4 |- ( NN e. { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } <-> ( 1 e. NN /\ A. y e. NN ( y + 1 ) e. NN ) )
28	19, 21, 27	mpbir2an 936	. . 3 |- NN e. { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }
29		intss1 4263	. . 3 |- ( NN e. { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } -> |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } C_ NN )
30	28, 29	ax-mp 5	. 2 |- |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } C_ NN
31	18, 30	eqssi 3460	1 |- NN = |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }

Syntax hints:   -> wi 4   /\ wa 375   A.wal 1453   = wceq 1455   e. wcel 1898   {cab 2448   A.wral 2749   C_ wss 3416   |^|cint 4248  (class class class)co 6320   1c1 9571   + caddc 9573   NNcn 10642

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4541  ax-nul 4550  ax-pow 4598  ax-pr 4656  ax-un 6615  ax-cnex 9626  ax-resscn 9627  ax-1cn 9628  ax-icn 9629  ax-addcl 9630  ax-addrcl 9631  ax-mulcl 9632  ax-mulrcl 9633  ax-i2m1 9638  ax-1ne0 9639  ax-rrecex 9642  ax-cnre 9643

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rex 2755  df-reu 2756  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-tp 3985  df-op 3987  df-uni 4213  df-int 4249  df-iun 4294  df-br 4419  df-opab 4478  df-mpt 4479  df-tr 4514  df-eprel 4767  df-id 4771  df-po 4777  df-so 4778  df-fr 4815  df-we 4817  df-xp 4862  df-rel 4863  df-cnv 4864  df-co 4865  df-dm 4866  df-rn 4867  df-res 4868  df-ima 4869  df-pred 5403  df-ord 5449  df-on 5450  df-lim 5451  df-suc 5452  df-iota 5569  df-fun 5607  df-fn 5608  df-f 5609  df-f1 5610  df-fo 5611  df-f1o 5612  df-fv 5613  df-ov 6323  df-om 6725  df-wrecs 7059  df-recs 7121  df-rdg 7159  df-nn 10643

This theorem is referenced by:  dfnn3  10656