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 )