Metamath Proof Explorer

Theorem ioonct

Description: A nonempty open interval is uncountable. (Contributed by Glauco Siliprandi, 3-Jan-2021)

Ref Expression
Hypotheses ioonct.b 
|- ( ph -> A e. RR* )
ioonct.c 
|- ( ph -> B e. RR* )
ioonct.l 
|- ( ph -> A < B )
ioonct.a 
|- C = ( A (,) B )
Assertion ioonct 
|- ( ph -> -. C ~<_ _om )

Proof

Step Hyp Ref Expression
1 ioonct.b 
 |-  ( ph -> A e. RR* )
2 ioonct.c 
 |-  ( ph -> B e. RR* )
3 ioonct.l 
 |-  ( ph -> A < B )
4 ioonct.a 
 |-  C = ( A (,) B )
5 ioontr 
 |-  ( ( int ` ( topGen ` ran (,) ) ) ` ( A (,) B ) ) = ( A (,) B )
6 5 a1i 
 |-  ( ( ph /\ C ~<_ _om ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A (,) B ) ) = ( A (,) B ) )
7 ioossre 
 |-  ( A (,) B ) C_ RR
8 7 a1i 
 |-  ( ( ph /\ C ~<_ _om ) -> ( A (,) B ) C_ RR )
9 4 breq1i 
 |-  ( C ~<_ _om <-> ( A (,) B ) ~<_ _om )
10 9 biimpi 
 |-  ( C ~<_ _om -> ( A (,) B ) ~<_ _om )
11 nnenom 
 |-  NN ~~ _om
12 11 ensymi 
 |-  _om ~~ NN
13 12 a1i 
 |-  ( C ~<_ _om -> _om ~~ NN )
14 domentr 
 |-  ( ( ( A (,) B ) ~<_ _om /\ _om ~~ NN ) -> ( A (,) B ) ~<_ NN )
15 10 13 14 syl2anc 
 |-  ( C ~<_ _om -> ( A (,) B ) ~<_ NN )
16 15 adantl 
 |-  ( ( ph /\ C ~<_ _om ) -> ( A (,) B ) ~<_ NN )
17 rectbntr0 
 |-  ( ( ( A (,) B ) C_ RR /\ ( A (,) B ) ~<_ NN ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A (,) B ) ) = (/) )
18 8 16 17 syl2anc 
 |-  ( ( ph /\ C ~<_ _om ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A (,) B ) ) = (/) )
19 6 18 eqtr3d 
 |-  ( ( ph /\ C ~<_ _om ) -> ( A (,) B ) = (/) )
20 ioon0 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( A (,) B ) =/= (/) <-> A < B ) )
21 1 2 20 syl2anc 
 |-  ( ph -> ( ( A (,) B ) =/= (/) <-> A < B ) )
22 3 21 mpbird 
 |-  ( ph -> ( A (,) B ) =/= (/) )
23 22 neneqd 
 |-  ( ph -> -. ( A (,) B ) = (/) )
24 23 adantr 
 |-  ( ( ph /\ C ~<_ _om ) -> -. ( A (,) B ) = (/) )
25 19 24 pm2.65da 
 |-  ( ph -> -. C ~<_ _om )