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	⊢ 𝐽 = ( topGen ‘ ran (,) )
	tgqioo2.2	⊢ ( 𝜑 → 𝐴 ∈ 𝐽 )
Assertion	tgqioo2	⊢ ( 𝜑 → ∃ 𝑞 ( 𝑞 ⊆ ( (,) “ ( ℚ × ℚ ) ) ∧ 𝐴 = ∪ 𝑞 ) )

Proof

Step	Hyp	Ref	Expression
1		tgqioo2.1	⊢ 𝐽 = ( topGen ‘ ran (,) )
2		tgqioo2.2	⊢ ( 𝜑 → 𝐴 ∈ 𝐽 )
3		eqid	⊢ ( topGen ‘ ( (,) “ ( ℚ × ℚ ) ) ) = ( topGen ‘ ( (,) “ ( ℚ × ℚ ) ) )
4	3	tgqioo	⊢ ( topGen ‘ ran (,) ) = ( topGen ‘ ( (,) “ ( ℚ × ℚ ) ) )
5	1 4 3	3eqtri	⊢ 𝐽 = ( topGen ‘ ( (,) “ ( ℚ × ℚ ) ) )
6	5	a1i	⊢ ( 𝜑 → 𝐽 = ( topGen ‘ ( (,) “ ( ℚ × ℚ ) ) ) )
7	2 6	eleqtrd	⊢ ( 𝜑 → 𝐴 ∈ ( topGen ‘ ( (,) “ ( ℚ × ℚ ) ) ) )
8		iooex	⊢ (,) ∈ V
9		imaexg	⊢ ( (,) ∈ V → ( (,) “ ( ℚ × ℚ ) ) ∈ V )
10	8 9	ax-mp	⊢ ( (,) “ ( ℚ × ℚ ) ) ∈ V
11		eltg3	⊢ ( ( (,) “ ( ℚ × ℚ ) ) ∈ V → ( 𝐴 ∈ ( topGen ‘ ( (,) “ ( ℚ × ℚ ) ) ) ↔ ∃ 𝑞 ( 𝑞 ⊆ ( (,) “ ( ℚ × ℚ ) ) ∧ 𝐴 = ∪ 𝑞 ) ) )
12	10 11	ax-mp	⊢ ( 𝐴 ∈ ( topGen ‘ ( (,) “ ( ℚ × ℚ ) ) ) ↔ ∃ 𝑞 ( 𝑞 ⊆ ( (,) “ ( ℚ × ℚ ) ) ∧ 𝐴 = ∪ 𝑞 ) )
13	7 12	sylib	⊢ ( 𝜑 → ∃ 𝑞 ( 𝑞 ⊆ ( (,) “ ( ℚ × ℚ ) ) ∧ 𝐴 = ∪ 𝑞 ) )