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=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
	tgqioo2.2	$$⊢\phi \to A\in J$$
Assertion	tgqioo2	$$⊢\phi \to \exists q\left(q\subseteq \left(.\right)\left[\mathbb{Q}\times \mathbb{Q}\right]\wedge A=\bigcup q\right)$$

Proof

Step	Hyp	Ref	Expression
1		tgqioo2.1	$$⊢J=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
2		tgqioo2.2	$$⊢\phi \to A\in J$$
3		eqid	$$⊢\mathrm{topGen}\left(\left(.\right)\left[\mathbb{Q}\times \mathbb{Q}\right]\right)=\mathrm{topGen}\left(\left(.\right)\left[\mathbb{Q}\times \mathbb{Q}\right]\right)$$
4	3	tgqioo	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=\mathrm{topGen}\left(\left(.\right)\left[\mathbb{Q}\times \mathbb{Q}\right]\right)$$
5	1 4 3	3eqtri	$$⊢J=\mathrm{topGen}\left(\left(.\right)\left[\mathbb{Q}\times \mathbb{Q}\right]\right)$$
6	5	a1i	$$⊢\phi \to J=\mathrm{topGen}\left(\left(.\right)\left[\mathbb{Q}\times \mathbb{Q}\right]\right)$$
7	2 6	eleqtrd	$$⊢\phi \to A\in \mathrm{topGen}\left(\left(.\right)\left[\mathbb{Q}\times \mathbb{Q}\right]\right)$$
8		iooex	$$⊢\left(.\right)\in \mathrm{V}$$
9		imaexg	$$⊢\left(.\right)\in \mathrm{V}\to \left(.\right)\left[\mathbb{Q}\times \mathbb{Q}\right]\in \mathrm{V}$$
10	8 9	ax-mp	$$⊢\left(.\right)\left[\mathbb{Q}\times \mathbb{Q}\right]\in \mathrm{V}$$
11		eltg3	$$⊢\left(.\right)\left[\mathbb{Q}\times \mathbb{Q}\right]\in \mathrm{V}\to \left(A\in \mathrm{topGen}\left(\left(.\right)\left[\mathbb{Q}\times \mathbb{Q}\right]\right)\leftrightarrow \exists q\left(q\subseteq \left(.\right)\left[\mathbb{Q}\times \mathbb{Q}\right]\wedge A=\bigcup q\right)\right)$$
12	10 11	ax-mp	$$⊢A\in \mathrm{topGen}\left(\left(.\right)\left[\mathbb{Q}\times \mathbb{Q}\right]\right)\leftrightarrow \exists q\left(q\subseteq \left(.\right)\left[\mathbb{Q}\times \mathbb{Q}\right]\wedge A=\bigcup q\right)$$
13	7 12	sylib	$$⊢\phi \to \exists q\left(q\subseteq \left(.\right)\left[\mathbb{Q}\times \mathbb{Q}\right]\wedge A=\bigcup q\right)$$