Theorem nqpr

Description: The canonical embedding of the rationals into the reals. (Contributed by Mario Carneiro, 12-Jun-2013) (New usage is discouraged.)

	Ref	Expression
Assertion	nqpr	|- ( A e. Q. -> { x | x

Proof

Step	Hyp	Ref	Expression
1		nsmallnq	|- ( A e. Q. -> E. x x
2		abn0	|- ( { x | x E. x x
3	1 2	sylibr	|- ( A e. Q. -> { x | x
4		0pss	|- ( (/) C. { x | x { x | x
5	3 4	sylibr	|- ( A e. Q. -> (/) C. { x | x
6		ltrelnq	|-
7	6	brel	|- ( x ( x e. Q. /\ A e. Q. ) )
8	7	simpld	|- ( x x e. Q. )
9	8	abssi	|- { x | x
10		ltsonq	|-
11	10 6	soirri	|- -. A
12		breq1	|- ( x = A -> ( x A
13	12	elabg	|- ( A e. Q. -> ( A e. { x | x A
14	11 13	mtbiri	|- ( A e. Q. -> -. A e. { x | x
15	14	ancli	|- ( A e. Q. -> ( A e. Q. /\ -. A e. { x | x
16		ssnelpss	|- ( { x | x ( ( A e. Q. /\ -. A e. { x | x { x | x
17	9 15 16	mpsyl	|- ( A e. Q. -> { x | x
18		vex	|- y e. _V
19		breq1	|- ( x = y -> ( x y
20	18 19	elab	|- ( y e. { x | x y
21	10 6	sotri	|- ( ( z z
22	21	expcom	|- ( y ( z z
23	22	adantl	|- ( ( A e. Q. /\ y ( z z
24		vex	|- z e. _V
25		breq1	|- ( x = z -> ( x z
26	24 25	elab	|- ( z e. { x | x z
27	23 26	imbitrrdi	|- ( ( A e. Q. /\ y ( z z e. { x | x
28	27	alrimiv	|- ( ( A e. Q. /\ y A. z ( z z e. { x | x
29		ltbtwnnq	|- ( y E. z ( y
30	26	anbi2i	|- ( ( y ( y
31	30	biimpri	|- ( ( y ( y
32	31	ancomd	|- ( ( y ( z e. { x | x
33	32	eximi	|- ( E. z ( y E. z ( z e. { x | x
34	29 33	sylbi	|- ( y E. z ( z e. { x | x
35	34	adantl	|- ( ( A e. Q. /\ y E. z ( z e. { x | x
36		df-rex	|- ( E. z e. { x | x E. z ( z e. { x | x
37	35 36	sylibr	|- ( ( A e. Q. /\ y E. z e. { x | x
38	28 37	jca	|- ( ( A e. Q. /\ y ( A. z ( z z e. { x | x
39	20 38	sylan2b	|- ( ( A e. Q. /\ y e. { x | x ( A. z ( z z e. { x | x
40	39	ralrimiva	|- ( A e. Q. -> A. y e. { x | x z e. { x | x
41		elnp	|- ( { x | x ( ( (/) C. { x | x z e. { x | x
42	5 17 40 41	syl21anbrc	|- ( A e. Q. -> { x | x