This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝐴 ∈ Q → { 𝑥 ∣ 𝑥 <Q 𝐴 } ∈ P )

Proof

Step Hyp Ref Expression
1 nsmallnq ⊢ ( 𝐴 ∈ Q → ∃ 𝑥 𝑥 <Q 𝐴 )
2 abn0 ⊢ ( { 𝑥 ∣ 𝑥 <Q 𝐴 } ≠ ∅ ↔ ∃ 𝑥 𝑥 <Q 𝐴 )
3 1 2 sylibr ⊢ ( 𝐴 ∈ Q → { 𝑥 ∣ 𝑥 <Q 𝐴 } ≠ ∅ )
4 0pss ⊢ ( ∅ ⊊ { 𝑥 ∣ 𝑥 <Q 𝐴 } ↔ { 𝑥 ∣ 𝑥 <Q 𝐴 } ≠ ∅ )
5 3 4 sylibr ⊢ ( 𝐴 ∈ Q → ∅ ⊊ { 𝑥 ∣ 𝑥 <Q 𝐴 } )
6 ltrelnq ⊢ <Q ⊆ ( Q × Q )
7 6 brel ⊢ ( 𝑥 <Q 𝐴 → ( 𝑥 ∈ Q ∧ 𝐴 ∈ Q ) )
8 7 simpld ⊢ ( 𝑥 <Q 𝐴 → 𝑥 ∈ Q )
9 8 abssi ⊢ { 𝑥 ∣ 𝑥 <Q 𝐴 } ⊆ Q
10 ltsonq ⊢ <Q Or Q
11 10 6 soirri ⊢ ¬ 𝐴 <Q 𝐴
12 breq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 <Q 𝐴 ↔ 𝐴 <Q 𝐴 ) )
13 12 elabg ⊢ ( 𝐴 ∈ Q → ( 𝐴 ∈ { 𝑥 ∣ 𝑥 <Q 𝐴 } ↔ 𝐴 <Q 𝐴 ) )
14 11 13 mtbiri ⊢ ( 𝐴 ∈ Q → ¬ 𝐴 ∈ { 𝑥 ∣ 𝑥 <Q 𝐴 } )
15 14 ancli ⊢ ( 𝐴 ∈ Q → ( 𝐴 ∈ Q ∧ ¬ 𝐴 ∈ { 𝑥 ∣ 𝑥 <Q 𝐴 } ) )
16 ssnelpss ⊢ ( { 𝑥 ∣ 𝑥 <Q 𝐴 } ⊆ Q → ( ( 𝐴 ∈ Q ∧ ¬ 𝐴 ∈ { 𝑥 ∣ 𝑥 <Q 𝐴 } ) → { 𝑥 ∣ 𝑥 <Q 𝐴 } ⊊ Q ) )
17 9 15 16 mpsyl ⊢ ( 𝐴 ∈ Q → { 𝑥 ∣ 𝑥 <Q 𝐴 } ⊊ Q )
18 vex ⊢ 𝑦 ∈ V
19 breq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 <Q 𝐴 ↔ 𝑦 <Q 𝐴 ) )
20 18 19 elab ⊢ ( 𝑦 ∈ { 𝑥 ∣ 𝑥 <Q 𝐴 } ↔ 𝑦 <Q 𝐴 )
21 10 6 sotri ⊢ ( ( 𝑧 <Q 𝑦 ∧ 𝑦 <Q 𝐴 ) → 𝑧 <Q 𝐴 )
22 21 expcom ⊢ ( 𝑦 <Q 𝐴 → ( 𝑧 <Q 𝑦 → 𝑧 <Q 𝐴 ) )
23 22 adantl ⊢ ( ( 𝐴 ∈ Q ∧ 𝑦 <Q 𝐴 ) → ( 𝑧 <Q 𝑦 → 𝑧 <Q 𝐴 ) )
24 vex ⊢ 𝑧 ∈ V
25 breq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 <Q 𝐴 ↔ 𝑧 <Q 𝐴 ) )
26 24 25 elab ⊢ ( 𝑧 ∈ { 𝑥 ∣ 𝑥 <Q 𝐴 } ↔ 𝑧 <Q 𝐴 )
27 23 26 imbitrrdi ⊢ ( ( 𝐴 ∈ Q ∧ 𝑦 <Q 𝐴 ) → ( 𝑧 <Q 𝑦 → 𝑧 ∈ { 𝑥 ∣ 𝑥 <Q 𝐴 } ) )
28 27 alrimiv ⊢ ( ( 𝐴 ∈ Q ∧ 𝑦 <Q 𝐴 ) → ∀ 𝑧 ( 𝑧 <Q 𝑦 → 𝑧 ∈ { 𝑥 ∣ 𝑥 <Q 𝐴 } ) )
29 ltbtwnnq ⊢ ( 𝑦 <Q 𝐴 ↔ ∃ 𝑧 ( 𝑦 <Q 𝑧 ∧ 𝑧 <Q 𝐴 ) )
30 26 anbi2i ⊢ ( ( 𝑦 <Q 𝑧 ∧ 𝑧 ∈ { 𝑥 ∣ 𝑥 <Q 𝐴 } ) ↔ ( 𝑦 <Q 𝑧 ∧ 𝑧 <Q 𝐴 ) )
31 30 biimpri ⊢ ( ( 𝑦 <Q 𝑧 ∧ 𝑧 <Q 𝐴 ) → ( 𝑦 <Q 𝑧 ∧ 𝑧 ∈ { 𝑥 ∣ 𝑥 <Q 𝐴 } ) )
32 31 ancomd ⊢ ( ( 𝑦 <Q 𝑧 ∧ 𝑧 <Q 𝐴 ) → ( 𝑧 ∈ { 𝑥 ∣ 𝑥 <Q 𝐴 } ∧ 𝑦 <Q 𝑧 ) )
33 32 eximi ⊢ ( ∃ 𝑧 ( 𝑦 <Q 𝑧 ∧ 𝑧 <Q 𝐴 ) → ∃ 𝑧 ( 𝑧 ∈ { 𝑥 ∣ 𝑥 <Q 𝐴 } ∧ 𝑦 <Q 𝑧 ) )
34 29 33 sylbi ⊢ ( 𝑦 <Q 𝐴 → ∃ 𝑧 ( 𝑧 ∈ { 𝑥 ∣ 𝑥 <Q 𝐴 } ∧ 𝑦 <Q 𝑧 ) )
35 34 adantl ⊢ ( ( 𝐴 ∈ Q ∧ 𝑦 <Q 𝐴 ) → ∃ 𝑧 ( 𝑧 ∈ { 𝑥 ∣ 𝑥 <Q 𝐴 } ∧ 𝑦 <Q 𝑧 ) )
36 df-rex ⊢ ( ∃ 𝑧 ∈ { 𝑥 ∣ 𝑥 <Q 𝐴 } 𝑦 <Q 𝑧 ↔ ∃ 𝑧 ( 𝑧 ∈ { 𝑥 ∣ 𝑥 <Q 𝐴 } ∧ 𝑦 <Q 𝑧 ) )
37 35 36 sylibr ⊢ ( ( 𝐴 ∈ Q ∧ 𝑦 <Q 𝐴 ) → ∃ 𝑧 ∈ { 𝑥 ∣ 𝑥 <Q 𝐴 } 𝑦 <Q 𝑧 )
38 28 37 jca ⊢ ( ( 𝐴 ∈ Q ∧ 𝑦 <Q 𝐴 ) → ( ∀ 𝑧 ( 𝑧 <Q 𝑦 → 𝑧 ∈ { 𝑥 ∣ 𝑥 <Q 𝐴 } ) ∧ ∃ 𝑧 ∈ { 𝑥 ∣ 𝑥 <Q 𝐴 } 𝑦 <Q 𝑧 ) )
39 20 38 sylan2b ⊢ ( ( 𝐴 ∈ Q ∧ 𝑦 ∈ { 𝑥 ∣ 𝑥 <Q 𝐴 } ) → ( ∀ 𝑧 ( 𝑧 <Q 𝑦 → 𝑧 ∈ { 𝑥 ∣ 𝑥 <Q 𝐴 } ) ∧ ∃ 𝑧 ∈ { 𝑥 ∣ 𝑥 <Q 𝐴 } 𝑦 <Q 𝑧 ) )
40 39 ralrimiva ⊢ ( 𝐴 ∈ Q → ∀ 𝑦 ∈ { 𝑥 ∣ 𝑥 <Q 𝐴 } ( ∀ 𝑧 ( 𝑧 <Q 𝑦 → 𝑧 ∈ { 𝑥 ∣ 𝑥 <Q 𝐴 } ) ∧ ∃ 𝑧 ∈ { 𝑥 ∣ 𝑥 <Q 𝐴 } 𝑦 <Q 𝑧 ) )
41 elnp ⊢ ( { 𝑥 ∣ 𝑥 <Q 𝐴 } ∈ P ↔ ( ( ∅ ⊊ { 𝑥 ∣ 𝑥 <Q 𝐴 } ∧ { 𝑥 ∣ 𝑥 <Q 𝐴 } ⊊ Q ) ∧ ∀ 𝑦 ∈ { 𝑥 ∣ 𝑥 <Q 𝐴 } ( ∀ 𝑧 ( 𝑧 <Q 𝑦 → 𝑧 ∈ { 𝑥 ∣ 𝑥 <Q 𝐴 } ) ∧ ∃ 𝑧 ∈ { 𝑥 ∣ 𝑥 <Q 𝐴 } 𝑦 <Q 𝑧 ) ) )
42 5 17 40 41 syl21anbrc ⊢ ( 𝐴 ∈ Q → { 𝑥 ∣ 𝑥 <Q 𝐴 } ∈ P )