Theorem rpnnen3lem

Description: Lemma for rpnnen3 . (Contributed by Stefan O'Rear, 18-Jan-2015)

	Ref	Expression
Assertion	rpnnen3lem	⊢ ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ 𝑎 < 𝑏 ) → { 𝑐 ∈ ℚ ∣ 𝑐 < 𝑎 } ≠ { 𝑐 ∈ ℚ ∣ 𝑐 < 𝑏 } )

Proof

Step	Hyp	Ref	Expression
1		qbtwnre	⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑎 < 𝑏 ) → ∃ 𝑑 ∈ ℚ ( 𝑎 < 𝑑 ∧ 𝑑 < 𝑏 ) )
2		simp2	⊢ ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑎 < 𝑏 ) ∧ 𝑑 ∈ ℚ ∧ ( 𝑎 < 𝑑 ∧ 𝑑 < 𝑏 ) ) → 𝑑 ∈ ℚ )
3		simp3r	⊢ ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑎 < 𝑏 ) ∧ 𝑑 ∈ ℚ ∧ ( 𝑎 < 𝑑 ∧ 𝑑 < 𝑏 ) ) → 𝑑 < 𝑏 )
4		breq1	⊢ ( 𝑐 = 𝑑 → ( 𝑐 < 𝑏 ↔ 𝑑 < 𝑏 ) )
5	4	elrab	⊢ ( 𝑑 ∈ { 𝑐 ∈ ℚ ∣ 𝑐 < 𝑏 } ↔ ( 𝑑 ∈ ℚ ∧ 𝑑 < 𝑏 ) )
6	2 3 5	sylanbrc	⊢ ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑎 < 𝑏 ) ∧ 𝑑 ∈ ℚ ∧ ( 𝑎 < 𝑑 ∧ 𝑑 < 𝑏 ) ) → 𝑑 ∈ { 𝑐 ∈ ℚ ∣ 𝑐 < 𝑏 } )
7		simp11	⊢ ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑎 < 𝑏 ) ∧ 𝑑 ∈ ℚ ∧ ( 𝑎 < 𝑑 ∧ 𝑑 < 𝑏 ) ) → 𝑎 ∈ ℝ )
8		qre	⊢ ( 𝑑 ∈ ℚ → 𝑑 ∈ ℝ )
9	8	3ad2ant2	⊢ ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑎 < 𝑏 ) ∧ 𝑑 ∈ ℚ ∧ ( 𝑎 < 𝑑 ∧ 𝑑 < 𝑏 ) ) → 𝑑 ∈ ℝ )
10		simp3l	⊢ ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑎 < 𝑏 ) ∧ 𝑑 ∈ ℚ ∧ ( 𝑎 < 𝑑 ∧ 𝑑 < 𝑏 ) ) → 𝑎 < 𝑑 )
11	7 9 10	ltnsymd	⊢ ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑎 < 𝑏 ) ∧ 𝑑 ∈ ℚ ∧ ( 𝑎 < 𝑑 ∧ 𝑑 < 𝑏 ) ) → ¬ 𝑑 < 𝑎 )
12	11	intnand	⊢ ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑎 < 𝑏 ) ∧ 𝑑 ∈ ℚ ∧ ( 𝑎 < 𝑑 ∧ 𝑑 < 𝑏 ) ) → ¬ ( 𝑑 ∈ ℚ ∧ 𝑑 < 𝑎 ) )
13		breq1	⊢ ( 𝑐 = 𝑑 → ( 𝑐 < 𝑎 ↔ 𝑑 < 𝑎 ) )
14	13	elrab	⊢ ( 𝑑 ∈ { 𝑐 ∈ ℚ ∣ 𝑐 < 𝑎 } ↔ ( 𝑑 ∈ ℚ ∧ 𝑑 < 𝑎 ) )
15	12 14	sylnibr	⊢ ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑎 < 𝑏 ) ∧ 𝑑 ∈ ℚ ∧ ( 𝑎 < 𝑑 ∧ 𝑑 < 𝑏 ) ) → ¬ 𝑑 ∈ { 𝑐 ∈ ℚ ∣ 𝑐 < 𝑎 } )
16		nelne1	⊢ ( ( 𝑑 ∈ { 𝑐 ∈ ℚ ∣ 𝑐 < 𝑏 } ∧ ¬ 𝑑 ∈ { 𝑐 ∈ ℚ ∣ 𝑐 < 𝑎 } ) → { 𝑐 ∈ ℚ ∣ 𝑐 < 𝑏 } ≠ { 𝑐 ∈ ℚ ∣ 𝑐 < 𝑎 } )
17	6 15 16	syl2anc	⊢ ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑎 < 𝑏 ) ∧ 𝑑 ∈ ℚ ∧ ( 𝑎 < 𝑑 ∧ 𝑑 < 𝑏 ) ) → { 𝑐 ∈ ℚ ∣ 𝑐 < 𝑏 } ≠ { 𝑐 ∈ ℚ ∣ 𝑐 < 𝑎 } )
18	17	necomd	⊢ ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑎 < 𝑏 ) ∧ 𝑑 ∈ ℚ ∧ ( 𝑎 < 𝑑 ∧ 𝑑 < 𝑏 ) ) → { 𝑐 ∈ ℚ ∣ 𝑐 < 𝑎 } ≠ { 𝑐 ∈ ℚ ∣ 𝑐 < 𝑏 } )
19	18	rexlimdv3a	⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑎 < 𝑏 ) → ( ∃ 𝑑 ∈ ℚ ( 𝑎 < 𝑑 ∧ 𝑑 < 𝑏 ) → { 𝑐 ∈ ℚ ∣ 𝑐 < 𝑎 } ≠ { 𝑐 ∈ ℚ ∣ 𝑐 < 𝑏 } ) )
20	1 19	mpd	⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑎 < 𝑏 ) → { 𝑐 ∈ ℚ ∣ 𝑐 < 𝑎 } ≠ { 𝑐 ∈ ℚ ∣ 𝑐 < 𝑏 } )
21	20	3expa	⊢ ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ 𝑎 < 𝑏 ) → { 𝑐 ∈ ℚ ∣ 𝑐 < 𝑎 } ≠ { 𝑐 ∈ ℚ ∣ 𝑐 < 𝑏 } )