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	syl6ibr	⊢ ( ( 𝐴 ∈ 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 )