Metamath Proof Explorer

Theorem opnreen

Description: Every nonempty open set is uncountable. (Contributed by Mario Carneiro, 26-Jul-2014) (Revised by Mario Carneiro, 20-Feb-2015)

Ref Expression
Assertion opnreen 
|- ( ( A e. ( topGen ` ran (,) ) /\ A =/= (/) ) -> A ~~ ~P NN )

Proof

Step Hyp Ref Expression
1 reex 
 |-  RR e. _V
2 elssuni 
 |-  ( A e. ( topGen ` ran (,) ) -> A C_ U. ( topGen ` ran (,) ) )
3 uniretop 
 |-  RR = U. ( topGen ` ran (,) )
4 2 3 sseqtrrdi 
 |-  ( A e. ( topGen ` ran (,) ) -> A C_ RR )
5 ssdomg 
 |-  ( RR e. _V -> ( A C_ RR -> A ~<_ RR ) )
6 1 4 5 mpsyl 
 |-  ( A e. ( topGen ` ran (,) ) -> A ~<_ RR )
7 rpnnen 
 |-  RR ~~ ~P NN
8 domentr 
 |-  ( ( A ~<_ RR /\ RR ~~ ~P NN ) -> A ~<_ ~P NN )
9 6 7 8 sylancl 
 |-  ( A e. ( topGen ` ran (,) ) -> A ~<_ ~P NN )
10 n0 
 |-  ( A =/= (/) <-> E. x x e. A )
11 4 sselda 
 |-  ( ( A e. ( topGen ` ran (,) ) /\ x e. A ) -> x e. RR )
12 rpnnen2 
 |-  ~P NN ~<_ ( 0 [,] 1 )
13 rphalfcl 
 |-  ( y e. RR+ -> ( y / 2 ) e. RR+ )
14 13 rpred 
 |-  ( y e. RR+ -> ( y / 2 ) e. RR )
15 resubcl 
 |-  ( ( x e. RR /\ ( y / 2 ) e. RR ) -> ( x - ( y / 2 ) ) e. RR )
16 14 15 sylan2 
 |-  ( ( x e. RR /\ y e. RR+ ) -> ( x - ( y / 2 ) ) e. RR )
17 readdcl 
 |-  ( ( x e. RR /\ ( y / 2 ) e. RR ) -> ( x + ( y / 2 ) ) e. RR )
18 14 17 sylan2 
 |-  ( ( x e. RR /\ y e. RR+ ) -> ( x + ( y / 2 ) ) e. RR )
19 simpl 
 |-  ( ( x e. RR /\ y e. RR+ ) -> x e. RR )
20 ltsubrp 
 |-  ( ( x e. RR /\ ( y / 2 ) e. RR+ ) -> ( x - ( y / 2 ) ) < x )
21 13 20 sylan2 
 |-  ( ( x e. RR /\ y e. RR+ ) -> ( x - ( y / 2 ) ) < x )
22 ltaddrp 
 |-  ( ( x e. RR /\ ( y / 2 ) e. RR+ ) -> x < ( x + ( y / 2 ) ) )
23 13 22 sylan2 
 |-  ( ( x e. RR /\ y e. RR+ ) -> x < ( x + ( y / 2 ) ) )
24 16 19 18 21 23 lttrd 
 |-  ( ( x e. RR /\ y e. RR+ ) -> ( x - ( y / 2 ) ) < ( x + ( y / 2 ) ) )
25 iccen 
 |-  ( ( ( x - ( y / 2 ) ) e. RR /\ ( x + ( y / 2 ) ) e. RR /\ ( x - ( y / 2 ) ) < ( x + ( y / 2 ) ) ) -> ( 0 [,] 1 ) ~~ ( ( x - ( y / 2 ) ) [,] ( x + ( y / 2 ) ) ) )
26 16 18 24 25 syl3anc 
 |-  ( ( x e. RR /\ y e. RR+ ) -> ( 0 [,] 1 ) ~~ ( ( x - ( y / 2 ) ) [,] ( x + ( y / 2 ) ) ) )
27 domentr 
 |-  ( ( ~P NN ~<_ ( 0 [,] 1 ) /\ ( 0 [,] 1 ) ~~ ( ( x - ( y / 2 ) ) [,] ( x + ( y / 2 ) ) ) ) -> ~P NN ~<_ ( ( x - ( y / 2 ) ) [,] ( x + ( y / 2 ) ) ) )
28 12 26 27 sylancr 
 |-  ( ( x e. RR /\ y e. RR+ ) -> ~P NN ~<_ ( ( x - ( y / 2 ) ) [,] ( x + ( y / 2 ) ) ) )
29 ovex 
 |-  ( ( x - y ) (,) ( x + y ) ) e. _V
30 rpre 
 |-  ( y e. RR+ -> y e. RR )
31 resubcl 
 |-  ( ( x e. RR /\ y e. RR ) -> ( x - y ) e. RR )
32 30 31 sylan2 
 |-  ( ( x e. RR /\ y e. RR+ ) -> ( x - y ) e. RR )
33 32 rexrd 
 |-  ( ( x e. RR /\ y e. RR+ ) -> ( x - y ) e. RR* )
34 readdcl 
 |-  ( ( x e. RR /\ y e. RR ) -> ( x + y ) e. RR )
35 30 34 sylan2 
 |-  ( ( x e. RR /\ y e. RR+ ) -> ( x + y ) e. RR )
36 35 rexrd 
 |-  ( ( x e. RR /\ y e. RR+ ) -> ( x + y ) e. RR* )
37 19 recnd 
 |-  ( ( x e. RR /\ y e. RR+ ) -> x e. CC )
38 14 adantl 
 |-  ( ( x e. RR /\ y e. RR+ ) -> ( y / 2 ) e. RR )
39 38 recnd 
 |-  ( ( x e. RR /\ y e. RR+ ) -> ( y / 2 ) e. CC )
40 37 39 39 subsub4d 
 |-  ( ( x e. RR /\ y e. RR+ ) -> ( ( x - ( y / 2 ) ) - ( y / 2 ) ) = ( x - ( ( y / 2 ) + ( y / 2 ) ) ) )
41 30 adantl 
 |-  ( ( x e. RR /\ y e. RR+ ) -> y e. RR )
42 41 recnd 
 |-  ( ( x e. RR /\ y e. RR+ ) -> y e. CC )
43 42 2halvesd 
 |-  ( ( x e. RR /\ y e. RR+ ) -> ( ( y / 2 ) + ( y / 2 ) ) = y )
44 43 oveq2d 
 |-  ( ( x e. RR /\ y e. RR+ ) -> ( x - ( ( y / 2 ) + ( y / 2 ) ) ) = ( x - y ) )
45 40 44 eqtrd 
 |-  ( ( x e. RR /\ y e. RR+ ) -> ( ( x - ( y / 2 ) ) - ( y / 2 ) ) = ( x - y ) )
46 13 adantl 
 |-  ( ( x e. RR /\ y e. RR+ ) -> ( y / 2 ) e. RR+ )
47 16 46 ltsubrpd 
 |-  ( ( x e. RR /\ y e. RR+ ) -> ( ( x - ( y / 2 ) ) - ( y / 2 ) ) < ( x - ( y / 2 ) ) )
48 45 47 eqbrtrrd 
 |-  ( ( x e. RR /\ y e. RR+ ) -> ( x - y ) < ( x - ( y / 2 ) ) )
49 18 46 ltaddrpd 
 |-  ( ( x e. RR /\ y e. RR+ ) -> ( x + ( y / 2 ) ) < ( ( x + ( y / 2 ) ) + ( y / 2 ) ) )
50 37 39 39 addassd 
 |-  ( ( x e. RR /\ y e. RR+ ) -> ( ( x + ( y / 2 ) ) + ( y / 2 ) ) = ( x + ( ( y / 2 ) + ( y / 2 ) ) ) )
51 43 oveq2d 
 |-  ( ( x e. RR /\ y e. RR+ ) -> ( x + ( ( y / 2 ) + ( y / 2 ) ) ) = ( x + y ) )
52 50 51 eqtrd 
 |-  ( ( x e. RR /\ y e. RR+ ) -> ( ( x + ( y / 2 ) ) + ( y / 2 ) ) = ( x + y ) )
53 49 52 breqtrd 
 |-  ( ( x e. RR /\ y e. RR+ ) -> ( x + ( y / 2 ) ) < ( x + y ) )
54 iccssioo 
 |-  ( ( ( ( x - y ) e. RR* /\ ( x + y ) e. RR* ) /\ ( ( x - y ) < ( x - ( y / 2 ) ) /\ ( x + ( y / 2 ) ) < ( x + y ) ) ) -> ( ( x - ( y / 2 ) ) [,] ( x + ( y / 2 ) ) ) C_ ( ( x - y ) (,) ( x + y ) ) )
55 33 36 48 53 54 syl22anc 
 |-  ( ( x e. RR /\ y e. RR+ ) -> ( ( x - ( y / 2 ) ) [,] ( x + ( y / 2 ) ) ) C_ ( ( x - y ) (,) ( x + y ) ) )
56 ssdomg 
 |-  ( ( ( x - y ) (,) ( x + y ) ) e. _V -> ( ( ( x - ( y / 2 ) ) [,] ( x + ( y / 2 ) ) ) C_ ( ( x - y ) (,) ( x + y ) ) -> ( ( x - ( y / 2 ) ) [,] ( x + ( y / 2 ) ) ) ~<_ ( ( x - y ) (,) ( x + y ) ) ) )
57 29 55 56 mpsyl 
 |-  ( ( x e. RR /\ y e. RR+ ) -> ( ( x - ( y / 2 ) ) [,] ( x + ( y / 2 ) ) ) ~<_ ( ( x - y ) (,) ( x + y ) ) )
58 domtr 
 |-  ( ( ~P NN ~<_ ( ( x - ( y / 2 ) ) [,] ( x + ( y / 2 ) ) ) /\ ( ( x - ( y / 2 ) ) [,] ( x + ( y / 2 ) ) ) ~<_ ( ( x - y ) (,) ( x + y ) ) ) -> ~P NN ~<_ ( ( x - y ) (,) ( x + y ) ) )
59 28 57 58 syl2anc 
 |-  ( ( x e. RR /\ y e. RR+ ) -> ~P NN ~<_ ( ( x - y ) (,) ( x + y ) ) )
60 eqid 
 |-  ( ( abs o. - ) |` ( RR X. RR ) ) = ( ( abs o. - ) |` ( RR X. RR ) )
61 60 bl2ioo 
 |-  ( ( x e. RR /\ y e. RR ) -> ( x ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) y ) = ( ( x - y ) (,) ( x + y ) ) )
62 30 61 sylan2 
 |-  ( ( x e. RR /\ y e. RR+ ) -> ( x ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) y ) = ( ( x - y ) (,) ( x + y ) ) )
63 59 62 breqtrrd 
 |-  ( ( x e. RR /\ y e. RR+ ) -> ~P NN ~<_ ( x ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) y ) )
64 11 63 sylan 
 |-  ( ( ( A e. ( topGen ` ran (,) ) /\ x e. A ) /\ y e. RR+ ) -> ~P NN ~<_ ( x ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) y ) )
65 simplll 
 |-  ( ( ( ( A e. ( topGen ` ran (,) ) /\ x e. A ) /\ y e. RR+ ) /\ ( x ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) y ) C_ A ) -> A e. ( topGen ` ran (,) ) )
66 simpr 
 |-  ( ( ( ( A e. ( topGen ` ran (,) ) /\ x e. A ) /\ y e. RR+ ) /\ ( x ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) y ) C_ A ) -> ( x ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) y ) C_ A )
67 ssdomg 
 |-  ( A e. ( topGen ` ran (,) ) -> ( ( x ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) y ) C_ A -> ( x ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) y ) ~<_ A ) )
68 65 66 67 sylc 
 |-  ( ( ( ( A e. ( topGen ` ran (,) ) /\ x e. A ) /\ y e. RR+ ) /\ ( x ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) y ) C_ A ) -> ( x ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) y ) ~<_ A )
69 domtr 
 |-  ( ( ~P NN ~<_ ( x ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) y ) /\ ( x ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) y ) ~<_ A ) -> ~P NN ~<_ A )
70 64 68 69 syl2an2r 
 |-  ( ( ( ( A e. ( topGen ` ran (,) ) /\ x e. A ) /\ y e. RR+ ) /\ ( x ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) y ) C_ A ) -> ~P NN ~<_ A )
71 eqid 
 |-  ( MetOpen ` ( ( abs o. - ) |` ( RR X. RR ) ) ) = ( MetOpen ` ( ( abs o. - ) |` ( RR X. RR ) ) )
72 60 71 tgioo 
 |-  ( topGen ` ran (,) ) = ( MetOpen ` ( ( abs o. - ) |` ( RR X. RR ) ) )
73 72 eleq2i 
 |-  ( A e. ( topGen ` ran (,) ) <-> A e. ( MetOpen ` ( ( abs o. - ) |` ( RR X. RR ) ) ) )
74 60 rexmet 
 |-  ( ( abs o. - ) |` ( RR X. RR ) ) e. ( *Met ` RR )
75 71 mopni2 
 |-  ( ( ( ( abs o. - ) |` ( RR X. RR ) ) e. ( *Met ` RR ) /\ A e. ( MetOpen ` ( ( abs o. - ) |` ( RR X. RR ) ) ) /\ x e. A ) -> E. y e. RR+ ( x ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) y ) C_ A )
76 74 75 mp3an1 
 |-  ( ( A e. ( MetOpen ` ( ( abs o. - ) |` ( RR X. RR ) ) ) /\ x e. A ) -> E. y e. RR+ ( x ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) y ) C_ A )
77 73 76 sylanb 
 |-  ( ( A e. ( topGen ` ran (,) ) /\ x e. A ) -> E. y e. RR+ ( x ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) y ) C_ A )
78 70 77 r19.29a 
 |-  ( ( A e. ( topGen ` ran (,) ) /\ x e. A ) -> ~P NN ~<_ A )
79 78 ex 
 |-  ( A e. ( topGen ` ran (,) ) -> ( x e. A -> ~P NN ~<_ A ) )
80 79 exlimdv 
 |-  ( A e. ( topGen ` ran (,) ) -> ( E. x x e. A -> ~P NN ~<_ A ) )
81 10 80 syl5bi 
 |-  ( A e. ( topGen ` ran (,) ) -> ( A =/= (/) -> ~P NN ~<_ A ) )
82 81 imp 
 |-  ( ( A e. ( topGen ` ran (,) ) /\ A =/= (/) ) -> ~P NN ~<_ A )
83 sbth 
 |-  ( ( A ~<_ ~P NN /\ ~P NN ~<_ A ) -> A ~~ ~P NN )
84 9 82 83 syl2an2r 
 |-  ( ( A e. ( topGen ` ran (,) ) /\ A =/= (/) ) -> A ~~ ~P NN )