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 imbitrrdi ⊢ 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 ∈ 𝑷