Metamath Proof Explorer

Theorem qndenserrn

Description: n-dimensional rational numbers are dense in the space of n-dimensional real numbers, with respect to the n-dimensional standard topology. (Contributed by Glauco Siliprandi, 24-Dec-2020)

Ref Expression
Hypotheses qndenserrn.i 
|- ( ph -> I e. Fin )
qndenserrn.j 
|- J = ( TopOpen ` ( RR^ ` I ) )
Assertion qndenserrn 
|- ( ph -> ( ( cls ` J ) ` ( QQ ^m I ) ) = ( RR ^m I ) )

Proof

Step Hyp Ref Expression
1 qndenserrn.i 
 |-  ( ph -> I e. Fin )
2 qndenserrn.j 
 |-  J = ( TopOpen ` ( RR^ ` I ) )
3 2 rrxtop 
 |-  ( I e. Fin -> J e. Top )
4 1 3 syl 
 |-  ( ph -> J e. Top )
5 reex 
 |-  RR e. _V
6 qssre 
 |-  QQ C_ RR
7 mapss 
 |-  ( ( RR e. _V /\ QQ C_ RR ) -> ( QQ ^m I ) C_ ( RR ^m I ) )
8 5 6 7 mp2an 
 |-  ( QQ ^m I ) C_ ( RR ^m I )
9 8 a1i 
 |-  ( ph -> ( QQ ^m I ) C_ ( RR ^m I ) )
10 eqid 
 |-  ( RR^ ` I ) = ( RR^ ` I )
11 eqid 
 |-  ( Base ` ( RR^ ` I ) ) = ( Base ` ( RR^ ` I ) )
12 1 10 11 rrxbasefi 
 |-  ( ph -> ( Base ` ( RR^ ` I ) ) = ( RR ^m I ) )
13 12 eqcomd 
 |-  ( ph -> ( RR ^m I ) = ( Base ` ( RR^ ` I ) ) )
14 rrxtps 
 |-  ( I e. Fin -> ( RR^ ` I ) e. TopSp )
15 eqid 
 |-  ( TopOpen ` ( RR^ ` I ) ) = ( TopOpen ` ( RR^ ` I ) )
16 11 15 tpsuni 
 |-  ( ( RR^ ` I ) e. TopSp -> ( Base ` ( RR^ ` I ) ) = U. ( TopOpen ` ( RR^ ` I ) ) )
17 1 14 16 3syl 
 |-  ( ph -> ( Base ` ( RR^ ` I ) ) = U. ( TopOpen ` ( RR^ ` I ) ) )
18 2 unieqi 
 |-  U. J = U. ( TopOpen ` ( RR^ ` I ) )
19 18 eqcomi 
 |-  U. ( TopOpen ` ( RR^ ` I ) ) = U. J
20 19 a1i 
 |-  ( ph -> U. ( TopOpen ` ( RR^ ` I ) ) = U. J )
21 13 17 20 3eqtrd 
 |-  ( ph -> ( RR ^m I ) = U. J )
22 9 21 sseqtrd 
 |-  ( ph -> ( QQ ^m I ) C_ U. J )
23 eqid 
 |-  U. J = U. J
24 23 clsss3 
 |-  ( ( J e. Top /\ ( QQ ^m I ) C_ U. J ) -> ( ( cls ` J ) ` ( QQ ^m I ) ) C_ U. J )
25 4 22 24 syl2anc 
 |-  ( ph -> ( ( cls ` J ) ` ( QQ ^m I ) ) C_ U. J )
26 21 eqcomd 
 |-  ( ph -> U. J = ( RR ^m I ) )
27 25 26 sseqtrd 
 |-  ( ph -> ( ( cls ` J ) ` ( QQ ^m I ) ) C_ ( RR ^m I ) )
28 1 ad2antrr 
 |-  ( ( ( ph /\ v e. J ) /\ x e. v ) -> I e. Fin )
29 id 
 |-  ( v e. J -> v e. J )
30 29 2 eleqtrdi 
 |-  ( v e. J -> v e. ( TopOpen ` ( RR^ ` I ) ) )
31 30 ad2antlr 
 |-  ( ( ( ph /\ v e. J ) /\ x e. v ) -> v e. ( TopOpen ` ( RR^ ` I ) ) )
32 ne0i 
 |-  ( x e. v -> v =/= (/) )
33 32 adantl 
 |-  ( ( ( ph /\ v e. J ) /\ x e. v ) -> v =/= (/) )
34 28 15 31 33 qndenserrnopn 
 |-  ( ( ( ph /\ v e. J ) /\ x e. v ) -> E. y e. ( QQ ^m I ) y e. v )
35 df-rex 
 |-  ( E. y e. ( QQ ^m I ) y e. v <-> E. y ( y e. ( QQ ^m I ) /\ y e. v ) )
36 34 35 sylib 
 |-  ( ( ( ph /\ v e. J ) /\ x e. v ) -> E. y ( y e. ( QQ ^m I ) /\ y e. v ) )
37 simpr 
 |-  ( ( y e. ( QQ ^m I ) /\ y e. v ) -> y e. v )
38 simpl 
 |-  ( ( y e. ( QQ ^m I ) /\ y e. v ) -> y e. ( QQ ^m I ) )
39 37 38 elind 
 |-  ( ( y e. ( QQ ^m I ) /\ y e. v ) -> y e. ( v i^i ( QQ ^m I ) ) )
40 39 a1i 
 |-  ( ( ( ph /\ v e. J ) /\ x e. v ) -> ( ( y e. ( QQ ^m I ) /\ y e. v ) -> y e. ( v i^i ( QQ ^m I ) ) ) )
41 40 eximdv 
 |-  ( ( ( ph /\ v e. J ) /\ x e. v ) -> ( E. y ( y e. ( QQ ^m I ) /\ y e. v ) -> E. y y e. ( v i^i ( QQ ^m I ) ) ) )
42 36 41 mpd 
 |-  ( ( ( ph /\ v e. J ) /\ x e. v ) -> E. y y e. ( v i^i ( QQ ^m I ) ) )
43 n0 
 |-  ( ( v i^i ( QQ ^m I ) ) =/= (/) <-> E. y y e. ( v i^i ( QQ ^m I ) ) )
44 42 43 sylibr 
 |-  ( ( ( ph /\ v e. J ) /\ x e. v ) -> ( v i^i ( QQ ^m I ) ) =/= (/) )
45 44 ex 
 |-  ( ( ph /\ v e. J ) -> ( x e. v -> ( v i^i ( QQ ^m I ) ) =/= (/) ) )
46 45 adantlr 
 |-  ( ( ( ph /\ x e. ( RR ^m I ) ) /\ v e. J ) -> ( x e. v -> ( v i^i ( QQ ^m I ) ) =/= (/) ) )
47 46 ralrimiva 
 |-  ( ( ph /\ x e. ( RR ^m I ) ) -> A. v e. J ( x e. v -> ( v i^i ( QQ ^m I ) ) =/= (/) ) )
48 4 adantr 
 |-  ( ( ph /\ x e. ( RR ^m I ) ) -> J e. Top )
49 22 adantr 
 |-  ( ( ph /\ x e. ( RR ^m I ) ) -> ( QQ ^m I ) C_ U. J )
50 simpr 
 |-  ( ( ph /\ x e. ( RR ^m I ) ) -> x e. ( RR ^m I ) )
51 21 adantr 
 |-  ( ( ph /\ x e. ( RR ^m I ) ) -> ( RR ^m I ) = U. J )
52 50 51 eleqtrd 
 |-  ( ( ph /\ x e. ( RR ^m I ) ) -> x e. U. J )
53 23 elcls 
 |-  ( ( J e. Top /\ ( QQ ^m I ) C_ U. J /\ x e. U. J ) -> ( x e. ( ( cls ` J ) ` ( QQ ^m I ) ) <-> A. v e. J ( x e. v -> ( v i^i ( QQ ^m I ) ) =/= (/) ) ) )
54 48 49 52 53 syl3anc 
 |-  ( ( ph /\ x e. ( RR ^m I ) ) -> ( x e. ( ( cls ` J ) ` ( QQ ^m I ) ) <-> A. v e. J ( x e. v -> ( v i^i ( QQ ^m I ) ) =/= (/) ) ) )
55 47 54 mpbird 
 |-  ( ( ph /\ x e. ( RR ^m I ) ) -> x e. ( ( cls ` J ) ` ( QQ ^m I ) ) )
56 27 55 eqelssd 
 |-  ( ph -> ( ( cls ` J ) ` ( QQ ^m I ) ) = ( RR ^m I ) )