This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dfnn2

Description: Alternate definition of the set of positive integers. This was our original definition, before the current df-nn 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)

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

Proof

Step Hyp Ref Expression
1 1ex 
 |-  1 e. _V
2 1 elintab 
 |-  ( 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 
 |-  ( ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) -> 1 e. x )
4 2 3 mpgbir 
 |-  1 e. |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }
5 oveq1 
 |-  ( y = z -> ( y + 1 ) = ( z + 1 ) )
6 5 eleq1d 
 |-  ( y = z -> ( ( y + 1 ) e. x <-> ( z + 1 ) e. x ) )
7 6 rspccv 
 |-  ( A. y e. x ( y + 1 ) e. x -> ( z e. x -> ( z + 1 ) e. x ) )
8 7 adantl 
 |-  ( ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) -> ( z e. x -> ( z + 1 ) e. x ) )
9 8 a2i 
 |-  ( ( ( 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 
 |-  ( 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 
 |-  z e. _V
12 11 elintab 
 |-  ( 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 
 |-  ( z + 1 ) e. _V
14 13 elintab 
 |-  ( ( 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 
 |-  ( 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 
 |-  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 
 |-  ( ( 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 
 |-  NN C_ |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }
19 1nn 
 |-  1 e. NN
20 peano2nn 
 |-  ( y e. NN -> ( y + 1 ) e. NN )
21 20 rgen 
 |-  A. y e. NN ( y + 1 ) e. NN
22 nnex 
 |-  NN e. _V
23 eleq2 
 |-  ( x = NN -> ( 1 e. x <-> 1 e. NN ) )
24 eleq2 
 |-  ( x = NN -> ( ( y + 1 ) e. x <-> ( y + 1 ) e. NN ) )
25 24 raleqbi1dv 
 |-  ( x = NN -> ( A. y e. x ( y + 1 ) e. x <-> A. y e. NN ( y + 1 ) e. NN ) )
26 23 25 anbi12d 
 |-  ( 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 
 |-  ( 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 
 |-  NN e. { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }
29 intss1 
 |-  ( 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 
 |-  |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } C_ NN
31 18 30 eqssi 
 |-  NN = |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }