Metamath Proof Explorer


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 syl6ibr
 |-  ( ( 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