Metamath Proof Explorer

Theorem tgqioo2

Description: Every open set of reals is the (countable) union of open interval with rational bounds. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses tgqioo2.1 
|- J = ( topGen ` ran (,) )
tgqioo2.2 
|- ( ph -> A e. J )
Assertion tgqioo2 
|- ( ph -> E. q ( q C_ ( (,) " ( QQ X. QQ ) ) /\ A = U. q ) )

Proof

Step Hyp Ref Expression
1 tgqioo2.1 
 |-  J = ( topGen ` ran (,) )
2 tgqioo2.2 
 |-  ( ph -> A e. J )
3 eqid 
 |-  ( topGen ` ( (,) " ( QQ X. QQ ) ) ) = ( topGen ` ( (,) " ( QQ X. QQ ) ) )
4 3 tgqioo 
 |-  ( topGen ` ran (,) ) = ( topGen ` ( (,) " ( QQ X. QQ ) ) )
5 1 4 3 3eqtri 
 |-  J = ( topGen ` ( (,) " ( QQ X. QQ ) ) )
6 5 a1i 
 |-  ( ph -> J = ( topGen ` ( (,) " ( QQ X. QQ ) ) ) )
7 2 6 eleqtrd 
 |-  ( ph -> A e. ( topGen ` ( (,) " ( QQ X. QQ ) ) ) )
8 iooex 
 |-  (,) e. _V
9 imaexg 
 |-  ( (,) e. _V -> ( (,) " ( QQ X. QQ ) ) e. _V )
10 8 9 ax-mp 
 |-  ( (,) " ( QQ X. QQ ) ) e. _V
11 eltg3 
 |-  ( ( (,) " ( QQ X. QQ ) ) e. _V -> ( A e. ( topGen ` ( (,) " ( QQ X. QQ ) ) ) <-> E. q ( q C_ ( (,) " ( QQ X. QQ ) ) /\ A = U. q ) ) )
12 10 11 ax-mp 
 |-  ( A e. ( topGen ` ( (,) " ( QQ X. QQ ) ) ) <-> E. q ( q C_ ( (,) " ( QQ X. QQ ) ) /\ A = U. q ) )
13 7 12 sylib 
 |-  ( ph -> E. q ( q C_ ( (,) " ( QQ X. QQ ) ) /\ A = U. q ) )