Metamath Proof Explorer

Theorem qqtopn

Description: The topology of the field of the rational numbers. (Contributed by Thierry Arnoux, 29-Aug-2020)

Ref Expression
Assertion qqtopn 
|- ( ( TopOpen ` RRfld ) |`t QQ ) = ( TopOpen ` ( CCfld |`s QQ ) )

Proof

Step Hyp Ref Expression
1 retopn 
 |-  ( topGen ` ran (,) ) = ( TopOpen ` RRfld )
2 1 oveq1i 
 |-  ( ( topGen ` ran (,) ) |`t QQ ) = ( ( TopOpen ` RRfld ) |`t QQ )
3 df-refld 
 |-  RRfld = ( CCfld |`s RR )
4 3 oveq1i 
 |-  ( RRfld |`s QQ ) = ( ( CCfld |`s RR ) |`s QQ )
5 reex 
 |-  RR e. _V
6 qssre 
 |-  QQ C_ RR
7 ressabs 
 |-  ( ( RR e. _V /\ QQ C_ RR ) -> ( ( CCfld |`s RR ) |`s QQ ) = ( CCfld |`s QQ ) )
8 5 6 7 mp2an 
 |-  ( ( CCfld |`s RR ) |`s QQ ) = ( CCfld |`s QQ )
9 4 8 eqtr2i 
 |-  ( CCfld |`s QQ ) = ( RRfld |`s QQ )
10 9 1 resstopn 
 |-  ( ( topGen ` ran (,) ) |`t QQ ) = ( TopOpen ` ( CCfld |`s QQ ) )
11 2 10 eqtr3i 
 |-  ( ( TopOpen ` RRfld ) |`t QQ ) = ( TopOpen ` ( CCfld |`s QQ ) )