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 φ A J
Assertion tgqioo2 φ q q . × A = q

Proof

Step Hyp Ref Expression
1 tgqioo2.1 J = topGen ran .
2 tgqioo2.2 φ A J
3 eqid topGen . × = topGen . ×
4 3 tgqioo topGen ran . = topGen . ×
5 1 4 3 3eqtri J = topGen . ×
6 5 a1i φ J = topGen . ×
7 2 6 eleqtrd φ A topGen . ×
8 iooex . V
9 imaexg . V . × V
10 8 9 ax-mp . × V
11 eltg3 . × V A topGen . × q q . × A = q
12 10 11 ax-mp A topGen . × q q . × A = q
13 7 12 sylib φ q q . × A = q