Metamath Proof Explorer

Theorem rpnnen3lem

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

Ref Expression
Assertion rpnnen3lem 
|- ( ( ( a e. RR /\ b e. RR ) /\ a < b ) -> { c e. QQ | c < a } =/= { c e. QQ | c < b } )

Proof

Step Hyp Ref Expression
1 qbtwnre 
 |-  ( ( a e. RR /\ b e. RR /\ a < b ) -> E. d e. QQ ( a < d /\ d < b ) )
2 simp2 
 |-  ( ( ( a e. RR /\ b e. RR /\ a < b ) /\ d e. QQ /\ ( a < d /\ d < b ) ) -> d e. QQ )
3 simp3r 
 |-  ( ( ( a e. RR /\ b e. RR /\ a < b ) /\ d e. QQ /\ ( a < d /\ d < b ) ) -> d < b )
4 breq1 
 |-  ( c = d -> ( c < b <-> d < b ) )
5 4 elrab 
 |-  ( d e. { c e. QQ | c < b } <-> ( d e. QQ /\ d < b ) )
6 2 3 5 sylanbrc 
 |-  ( ( ( a e. RR /\ b e. RR /\ a < b ) /\ d e. QQ /\ ( a < d /\ d < b ) ) -> d e. { c e. QQ | c < b } )
7 simp11 
 |-  ( ( ( a e. RR /\ b e. RR /\ a < b ) /\ d e. QQ /\ ( a < d /\ d < b ) ) -> a e. RR )
8 qre 
 |-  ( d e. QQ -> d e. RR )
9 8 3ad2ant2 
 |-  ( ( ( a e. RR /\ b e. RR /\ a < b ) /\ d e. QQ /\ ( a < d /\ d < b ) ) -> d e. RR )
10 simp3l 
 |-  ( ( ( a e. RR /\ b e. RR /\ a < b ) /\ d e. QQ /\ ( a < d /\ d < b ) ) -> a < d )
11 7 9 10 ltnsymd 
 |-  ( ( ( a e. RR /\ b e. RR /\ a < b ) /\ d e. QQ /\ ( a < d /\ d < b ) ) -> -. d < a )
12 11 intnand 
 |-  ( ( ( a e. RR /\ b e. RR /\ a < b ) /\ d e. QQ /\ ( a < d /\ d < b ) ) -> -. ( d e. QQ /\ d < a ) )
13 breq1 
 |-  ( c = d -> ( c < a <-> d < a ) )
14 13 elrab 
 |-  ( d e. { c e. QQ | c < a } <-> ( d e. QQ /\ d < a ) )
15 12 14 sylnibr 
 |-  ( ( ( a e. RR /\ b e. RR /\ a < b ) /\ d e. QQ /\ ( a < d /\ d < b ) ) -> -. d e. { c e. QQ | c < a } )
16 nelne1 
 |-  ( ( d e. { c e. QQ | c < b } /\ -. d e. { c e. QQ | c < a } ) -> { c e. QQ | c < b } =/= { c e. QQ | c < a } )
17 6 15 16 syl2anc 
 |-  ( ( ( a e. RR /\ b e. RR /\ a < b ) /\ d e. QQ /\ ( a < d /\ d < b ) ) -> { c e. QQ | c < b } =/= { c e. QQ | c < a } )
18 17 necomd 
 |-  ( ( ( a e. RR /\ b e. RR /\ a < b ) /\ d e. QQ /\ ( a < d /\ d < b ) ) -> { c e. QQ | c < a } =/= { c e. QQ | c < b } )
19 18 rexlimdv3a 
 |-  ( ( a e. RR /\ b e. RR /\ a < b ) -> ( E. d e. QQ ( a < d /\ d < b ) -> { c e. QQ | c < a } =/= { c e. QQ | c < b } ) )
20 1 19 mpd 
 |-  ( ( a e. RR /\ b e. RR /\ a < b ) -> { c e. QQ | c < a } =/= { c e. QQ | c < b } )
21 20 3expa 
 |-  ( ( ( a e. RR /\ b e. RR ) /\ a < b ) -> { c e. QQ | c < a } =/= { c e. QQ | c < b } )