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 𝑸 x | x < 𝑸 A 𝑷

Proof

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