Theorem dfnn2 10629

Description: Alternate definition of the set of positive integers. This was our original definition, before the current df-nn 10617 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 9645	. . . . 5 |- 1 e. _V
2	1	elintab 4266	. . . 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 458	. . . 4 |- ( ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) -> 1 e. x )
4	2, 3	mpgbir 1667	. . 3 |- 1 e. |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }
5		oveq1 6312	. . . . . . . . . 10 |- ( y = z -> ( y + 1 ) = ( z + 1 ) )
6	5	eleq1d 2491	. . . . . . . . 9 |- ( y = z -> ( ( y + 1 ) e. x <-> ( z + 1 ) e. x ) )
7	6	rspccv 3179	. . . . . . . 8 |- ( A. y e. x ( y + 1 ) e. x -> ( z e. x -> ( z + 1 ) e. x ) )
8	7	adantl 467	. . . . . . 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 1678	. . . . 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 3083	. . . . . 6 |- z e. _V
12	11	elintab 4266	. . . . 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 6333	. . . . . 6 |- ( z + 1 ) e. _V
14	13	elintab 4266	. . . . 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 269	. . . 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 2781	. . 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 10619	. . 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 676	. 2 |- NN C_ |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }
19		1nn 10627	. . . 4 |- 1 e. NN
20		peano2nn 10628	. . . . 5 |- ( y e. NN -> ( y + 1 ) e. NN )
21	20	rgen 2781	. . . 4 |- A. y e. NN ( y + 1 ) e. NN
22		nnex 10622	. . . . 5 |- NN e. _V
23		eleq2 2496	. . . . . 6 |- ( x = NN -> ( 1 e. x <-> 1 e. NN ) )
24		eleq2 2496	. . . . . . 7 |- ( x = NN -> ( ( y + 1 ) e. x <-> ( y + 1 ) e. NN ) )
25	24	raleqbi1dv 3030	. . . . . 6 |- ( x = NN -> ( A. y e. x ( y + 1 ) e. x <-> A. y e. NN ( y + 1 ) e. NN ) )
26	23, 25	anbi12d 715	. . . . 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 3217	. . . 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 928	. . 3 |- NN e. { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }
29		intss1 4270	. . 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 3480	1 |- NN = |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }

Syntax hints:   -> wi 4   /\ wa 370   A.wal 1435   = wceq 1437   e. wcel 1872   {cab 2407   A.wral 2771   C_ wss 3436   |^|cint 4255  (class class class)co 6305   1c1 9547   + caddc 9549   NNcn 10616

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-sep 4546  ax-nul 4555  ax-pow 4602  ax-pr 4660  ax-un 6597  ax-cnex 9602  ax-resscn 9603  ax-1cn 9604  ax-icn 9605  ax-addcl 9606  ax-addrcl 9607  ax-mulcl 9608  ax-mulrcl 9609  ax-i2m1 9614  ax-1ne0 9615  ax-rrecex 9618  ax-cnre 9619

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-ral 2776  df-rex 2777  df-reu 2778  df-rab 2780  df-v 3082  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3912  df-pw 3983  df-sn 3999  df-pr 4001  df-tp 4003  df-op 4005  df-uni 4220  df-int 4256  df-iun 4301  df-br 4424  df-opab 4483  df-mpt 4484  df-tr 4519  df-eprel 4764  df-id 4768  df-po 4774  df-so 4775  df-fr 4812  df-we 4814  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-ov 6308  df-om 6707  df-wrecs 7039  df-recs 7101  df-rdg 7139  df-nn 10617

This theorem is referenced by:  dfnn3  10630