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 ) )