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

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