Metamath Proof Explorer


Theorem dfnn3

Description: Alternate definition of the set of positive integers. Definition of positive integers in Apostol p. 22. (Contributed by NM, 3-Jul-2005)

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

Proof

Step Hyp Ref Expression
1 eleq2
 |-  ( x = z -> ( 1 e. x <-> 1 e. z ) )
2 eleq2
 |-  ( x = z -> ( ( y + 1 ) e. x <-> ( y + 1 ) e. z ) )
3 2 raleqbi1dv
 |-  ( x = z -> ( A. y e. x ( y + 1 ) e. x <-> A. y e. z ( y + 1 ) e. z ) )
4 1 3 anbi12d
 |-  ( x = z -> ( ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) <-> ( 1 e. z /\ A. y e. z ( y + 1 ) e. z ) ) )
5 dfnn2
 |-  NN = |^| { z | ( 1 e. z /\ A. y e. z ( y + 1 ) e. z ) }
6 5 eqeq2i
 |-  ( x = NN <-> x = |^| { z | ( 1 e. z /\ A. y e. z ( y + 1 ) e. z ) } )
7 eleq2
 |-  ( x = NN -> ( 1 e. x <-> 1 e. NN ) )
8 eleq2
 |-  ( x = NN -> ( ( y + 1 ) e. x <-> ( y + 1 ) e. NN ) )
9 8 raleqbi1dv
 |-  ( x = NN -> ( A. y e. x ( y + 1 ) e. x <-> A. y e. NN ( y + 1 ) e. NN ) )
10 7 9 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 ) ) )
11 6 10 sylbir
 |-  ( x = |^| { z | ( 1 e. z /\ A. y e. z ( y + 1 ) e. z ) } -> ( ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) <-> ( 1 e. NN /\ A. y e. NN ( y + 1 ) e. NN ) ) )
12 nnssre
 |-  NN C_ RR
13 5 12 eqsstrri
 |-  |^| { z | ( 1 e. z /\ A. y e. z ( y + 1 ) e. z ) } C_ RR
14 1nn
 |-  1 e. NN
15 peano2nn
 |-  ( y e. NN -> ( y + 1 ) e. NN )
16 15 rgen
 |-  A. y e. NN ( y + 1 ) e. NN
17 14 16 pm3.2i
 |-  ( 1 e. NN /\ A. y e. NN ( y + 1 ) e. NN )
18 13 17 pm3.2i
 |-  ( |^| { z | ( 1 e. z /\ A. y e. z ( y + 1 ) e. z ) } C_ RR /\ ( 1 e. NN /\ A. y e. NN ( y + 1 ) e. NN ) )
19 4 11 18 intabs
 |-  |^| { x | ( x C_ RR /\ ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) ) } = |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }
20 3anass
 |-  ( ( x C_ RR /\ 1 e. x /\ A. y e. x ( y + 1 ) e. x ) <-> ( x C_ RR /\ ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) ) )
21 20 abbii
 |-  { x | ( x C_ RR /\ 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } = { x | ( x C_ RR /\ ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) ) }
22 21 inteqi
 |-  |^| { x | ( x C_ RR /\ 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } = |^| { x | ( x C_ RR /\ ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) ) }
23 dfnn2
 |-  NN = |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }
24 19 22 23 3eqtr4ri
 |-  NN = |^| { x | ( x C_ RR /\ 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }