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 ) }