Metamath Proof Explorer


Theorem pinq

Description: The representatives of positive integers as positive fractions. (Contributed by NM, 29-Oct-1995) (Revised by Mario Carneiro, 6-May-2013) (New usage is discouraged.)

Ref Expression
Assertion pinq
|- ( A e. N. -> <. A , 1o >. e. Q. )

Proof

Step Hyp Ref Expression
1 breq1
 |-  ( x = <. A , 1o >. -> ( x ~Q y <-> <. A , 1o >. ~Q y ) )
2 fveq2
 |-  ( x = <. A , 1o >. -> ( 2nd ` x ) = ( 2nd ` <. A , 1o >. ) )
3 2 breq2d
 |-  ( x = <. A , 1o >. -> ( ( 2nd ` y )  ( 2nd ` y ) . ) ) )
4 3 notbid
 |-  ( x = <. A , 1o >. -> ( -. ( 2nd ` y )  -. ( 2nd ` y ) . ) ) )
5 1 4 imbi12d
 |-  ( x = <. A , 1o >. -> ( ( x ~Q y -> -. ( 2nd ` y )  ( <. A , 1o >. ~Q y -> -. ( 2nd ` y ) . ) ) ) )
6 5 ralbidv
 |-  ( x = <. A , 1o >. -> ( A. y e. ( N. X. N. ) ( x ~Q y -> -. ( 2nd ` y )  A. y e. ( N. X. N. ) ( <. A , 1o >. ~Q y -> -. ( 2nd ` y ) . ) ) ) )
7 1pi
 |-  1o e. N.
8 opelxpi
 |-  ( ( A e. N. /\ 1o e. N. ) -> <. A , 1o >. e. ( N. X. N. ) )
9 7 8 mpan2
 |-  ( A e. N. -> <. A , 1o >. e. ( N. X. N. ) )
10 nlt1pi
 |-  -. ( 2nd ` y ) 
11 1oex
 |-  1o e. _V
12 op2ndg
 |-  ( ( A e. N. /\ 1o e. _V ) -> ( 2nd ` <. A , 1o >. ) = 1o )
13 11 12 mpan2
 |-  ( A e. N. -> ( 2nd ` <. A , 1o >. ) = 1o )
14 13 breq2d
 |-  ( A e. N. -> ( ( 2nd ` y ) . ) <-> ( 2nd ` y ) 
15 10 14 mtbiri
 |-  ( A e. N. -> -. ( 2nd ` y ) . ) )
16 15 a1d
 |-  ( A e. N. -> ( <. A , 1o >. ~Q y -> -. ( 2nd ` y ) . ) ) )
17 16 ralrimivw
 |-  ( A e. N. -> A. y e. ( N. X. N. ) ( <. A , 1o >. ~Q y -> -. ( 2nd ` y ) . ) ) )
18 6 9 17 elrabd
 |-  ( A e. N. -> <. A , 1o >. e. { x e. ( N. X. N. ) | A. y e. ( N. X. N. ) ( x ~Q y -> -. ( 2nd ` y ) 
19 df-nq
 |-  Q. = { x e. ( N. X. N. ) | A. y e. ( N. X. N. ) ( x ~Q y -> -. ( 2nd ` y ) 
20 18 19 eleqtrrdi
 |-  ( A e. N. -> <. A , 1o >. e. Q. )