This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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	$⊢ φ \to A \in J$
	Assertion	tgqioo2	$⊢ φ \to \exists q (q \subseteq (.) [ℚ \times ℚ] \land A = ⋃ q)$

Proof

Step	Hyp	Ref	Expression
1		tgqioo2.1	$⊢ J = topGen (ran (.))$
2		tgqioo2.2	$⊢ φ \to A \in J$
3		eqid	$⊢ topGen ((.) [ℚ \times ℚ]) = topGen ((.) [ℚ \times ℚ])$
4	3	tgqioo	$⊢ topGen (ran (.)) = topGen ((.) [ℚ \times ℚ])$
5	1 4 3	3eqtri	$⊢ J = topGen ((.) [ℚ \times ℚ])$
6	5	a1i	$⊢ φ \to J = topGen ((.) [ℚ \times ℚ])$
7	2 6	eleqtrd	$⊢ φ \to A \in topGen ((.) [ℚ \times ℚ])$
8		iooex	$⊢ (.) \in V$
9		imaexg	$⊢ (.) \in V \to (.) [ℚ \times ℚ] \in V$
10	8 9	ax-mp	$⊢ (.) [ℚ \times ℚ] \in V$
11		eltg3	$⊢ (.) [ℚ \times ℚ] \in V \to (A \in topGen ((.) [ℚ \times ℚ]) \leftrightarrow \exists q (q \subseteq (.) [ℚ \times ℚ] \land A = ⋃ q))$
12	10 11	ax-mp	$⊢ A \in topGen ((.) [ℚ \times ℚ]) \leftrightarrow \exists q (q \subseteq (.) [ℚ \times ℚ] \land A = ⋃ q)$
13	7 12	sylib	$⊢ φ \to \exists q (q \subseteq (.) [ℚ \times ℚ] \land A = ⋃ q)$