Metamath Proof Explorer

Theorem rectbntr0

Description: A countable subset of the reals has empty interior. (Contributed by Mario Carneiro, 26-Jul-2014)

Ref Expression
Assertion rectbntr0 
|- ( ( A C_ RR /\ A ~<_ NN ) -> ( ( int ` ( topGen ` ran (,) ) ) ` A ) = (/) )

Proof

Step Hyp Ref Expression
1 nnex 
 |-  NN e. _V
2 1 canth2 
 |-  NN ~< ~P NN
3 domnsym 
 |-  ( ~P NN ~<_ NN -> -. NN ~< ~P NN )
4 2 3 mt2 
 |-  -. ~P NN ~<_ NN
5 retop 
 |-  ( topGen ` ran (,) ) e. Top
6 simpl 
 |-  ( ( A C_ RR /\ A ~<_ NN ) -> A C_ RR )
7 uniretop 
 |-  RR = U. ( topGen ` ran (,) )
8 7 ntropn 
 |-  ( ( ( topGen ` ran (,) ) e. Top /\ A C_ RR ) -> ( ( int ` ( topGen ` ran (,) ) ) ` A ) e. ( topGen ` ran (,) ) )
9 5 6 8 sylancr 
 |-  ( ( A C_ RR /\ A ~<_ NN ) -> ( ( int ` ( topGen ` ran (,) ) ) ` A ) e. ( topGen ` ran (,) ) )
10 opnreen 
 |-  ( ( ( ( int ` ( topGen ` ran (,) ) ) ` A ) e. ( topGen ` ran (,) ) /\ ( ( int ` ( topGen ` ran (,) ) ) ` A ) =/= (/) ) -> ( ( int ` ( topGen ` ran (,) ) ) ` A ) ~~ ~P NN )
11 10 ex 
 |-  ( ( ( int ` ( topGen ` ran (,) ) ) ` A ) e. ( topGen ` ran (,) ) -> ( ( ( int ` ( topGen ` ran (,) ) ) ` A ) =/= (/) -> ( ( int ` ( topGen ` ran (,) ) ) ` A ) ~~ ~P NN ) )
12 9 11 syl 
 |-  ( ( A C_ RR /\ A ~<_ NN ) -> ( ( ( int ` ( topGen ` ran (,) ) ) ` A ) =/= (/) -> ( ( int ` ( topGen ` ran (,) ) ) ` A ) ~~ ~P NN ) )
13 reex 
 |-  RR e. _V
14 13 ssex 
 |-  ( A C_ RR -> A e. _V )
15 7 ntrss2 
 |-  ( ( ( topGen ` ran (,) ) e. Top /\ A C_ RR ) -> ( ( int ` ( topGen ` ran (,) ) ) ` A ) C_ A )
16 5 15 mpan 
 |-  ( A C_ RR -> ( ( int ` ( topGen ` ran (,) ) ) ` A ) C_ A )
17 ssdomg 
 |-  ( A e. _V -> ( ( ( int ` ( topGen ` ran (,) ) ) ` A ) C_ A -> ( ( int ` ( topGen ` ran (,) ) ) ` A ) ~<_ A ) )
18 14 16 17 sylc 
 |-  ( A C_ RR -> ( ( int ` ( topGen ` ran (,) ) ) ` A ) ~<_ A )
19 domtr 
 |-  ( ( ( ( int ` ( topGen ` ran (,) ) ) ` A ) ~<_ A /\ A ~<_ NN ) -> ( ( int ` ( topGen ` ran (,) ) ) ` A ) ~<_ NN )
20 18 19 sylan 
 |-  ( ( A C_ RR /\ A ~<_ NN ) -> ( ( int ` ( topGen ` ran (,) ) ) ` A ) ~<_ NN )
21 ensym 
 |-  ( ( ( int ` ( topGen ` ran (,) ) ) ` A ) ~~ ~P NN -> ~P NN ~~ ( ( int ` ( topGen ` ran (,) ) ) ` A ) )
22 endomtr 
 |-  ( ( ~P NN ~~ ( ( int ` ( topGen ` ran (,) ) ) ` A ) /\ ( ( int ` ( topGen ` ran (,) ) ) ` A ) ~<_ NN ) -> ~P NN ~<_ NN )
23 22 expcom 
 |-  ( ( ( int ` ( topGen ` ran (,) ) ) ` A ) ~<_ NN -> ( ~P NN ~~ ( ( int ` ( topGen ` ran (,) ) ) ` A ) -> ~P NN ~<_ NN ) )
24 20 21 23 syl2im 
 |-  ( ( A C_ RR /\ A ~<_ NN ) -> ( ( ( int ` ( topGen ` ran (,) ) ) ` A ) ~~ ~P NN -> ~P NN ~<_ NN ) )
25 12 24 syld 
 |-  ( ( A C_ RR /\ A ~<_ NN ) -> ( ( ( int ` ( topGen ` ran (,) ) ) ` A ) =/= (/) -> ~P NN ~<_ NN ) )
26 25 necon1bd 
 |-  ( ( A C_ RR /\ A ~<_ NN ) -> ( -. ~P NN ~<_ NN -> ( ( int ` ( topGen ` ran (,) ) ) ` A ) = (/) ) )
27 4 26 mpi 
 |-  ( ( A C_ RR /\ A ~<_ NN ) -> ( ( int ` ( topGen ` ran (,) ) ) ` A ) = (/) )