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

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