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