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

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

Metamath Proof Explorer