tgqioo

Description: The topology generated by open intervals of reals with rational endpoints is the same as the open sets of the standard metric space on the reals. In particular, this proves that the standard topology on the reals is second-countable. (Contributed by Mario Carneiro, 17-Jun-2014)

		Ref	Expression
	Hypothesis	tgqioo.1	⊢ 𝑄 = ( topGen ‘ ( (,) “ ( ℚ × ℚ ) ) )
	Assertion	tgqioo	⊢ ( topGen ‘ ran (,) ) = 𝑄

Proof

Step	Hyp	Ref	Expression
1		tgqioo.1	⊢ 𝑄 = ( topGen ‘ ( (,) “ ( ℚ × ℚ ) ) )
2		imassrn	⊢ ( (,) “ ( ℚ × ℚ ) ) ⊆ ran (,)
3		ioof	⊢ (,) : ( ℝ^* × ℝ^* ) ⟶ 𝒫 ℝ
4		ffn	⊢ ( (,) : ( ℝ^* × ℝ^* ) ⟶ 𝒫 ℝ → (,) Fn ( ℝ^* × ℝ^* ) )
5	3 4	ax-mp	⊢ (,) Fn ( ℝ^* × ℝ^* )
6		simpll	⊢ ( ( ( 𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ) ∧ 𝑧 ∈ ( 𝑥 (,) 𝑦 ) ) → 𝑥 ∈ ℝ^* )
7		elioo1	⊢ ( ( 𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ) → ( 𝑧 ∈ ( 𝑥 (,) 𝑦 ) ↔ ( 𝑧 ∈ ℝ^* ∧ 𝑥 < 𝑧 ∧ 𝑧 < 𝑦 ) ) )
8	7	biimpa	⊢ ( ( ( 𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ) ∧ 𝑧 ∈ ( 𝑥 (,) 𝑦 ) ) → ( 𝑧 ∈ ℝ^* ∧ 𝑥 < 𝑧 ∧ 𝑧 < 𝑦 ) )
9	8	simp1d	⊢ ( ( ( 𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ) ∧ 𝑧 ∈ ( 𝑥 (,) 𝑦 ) ) → 𝑧 ∈ ℝ^* )
10	8	simp2d	⊢ ( ( ( 𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ) ∧ 𝑧 ∈ ( 𝑥 (,) 𝑦 ) ) → 𝑥 < 𝑧 )
11		qbtwnxr	⊢ ( ( 𝑥 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^* ∧ 𝑥 < 𝑧 ) → ∃ 𝑢 ∈ ℚ ( 𝑥 < 𝑢 ∧ 𝑢 < 𝑧 ) )
12	6 9 10 11	syl3anc	⊢ ( ( ( 𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ) ∧ 𝑧 ∈ ( 𝑥 (,) 𝑦 ) ) → ∃ 𝑢 ∈ ℚ ( 𝑥 < 𝑢 ∧ 𝑢 < 𝑧 ) )
13		simplr	⊢ ( ( ( 𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ) ∧ 𝑧 ∈ ( 𝑥 (,) 𝑦 ) ) → 𝑦 ∈ ℝ^* )
14	8	simp3d	⊢ ( ( ( 𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ) ∧ 𝑧 ∈ ( 𝑥 (,) 𝑦 ) ) → 𝑧 < 𝑦 )
15		qbtwnxr	⊢ ( ( 𝑧 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 < 𝑦 ) → ∃ 𝑣 ∈ ℚ ( 𝑧 < 𝑣 ∧ 𝑣 < 𝑦 ) )
16	9 13 14 15	syl3anc	⊢ ( ( ( 𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ) ∧ 𝑧 ∈ ( 𝑥 (,) 𝑦 ) ) → ∃ 𝑣 ∈ ℚ ( 𝑧 < 𝑣 ∧ 𝑣 < 𝑦 ) )
17		reeanv	⊢ ( ∃ 𝑢 ∈ ℚ ∃ 𝑣 ∈ ℚ ( ( 𝑥 < 𝑢 ∧ 𝑢 < 𝑧 ) ∧ ( 𝑧 < 𝑣 ∧ 𝑣 < 𝑦 ) ) ↔ ( ∃ 𝑢 ∈ ℚ ( 𝑥 < 𝑢 ∧ 𝑢 < 𝑧 ) ∧ ∃ 𝑣 ∈ ℚ ( 𝑧 < 𝑣 ∧ 𝑣 < 𝑦 ) ) )
18		df-ov	⊢ ( 𝑢 (,) 𝑣 ) = ( (,) ‘ ⟨ 𝑢 , 𝑣 ⟩ )
19		opelxpi	⊢ ( ( 𝑢 ∈ ℚ ∧ 𝑣 ∈ ℚ ) → ⟨ 𝑢 , 𝑣 ⟩ ∈ ( ℚ × ℚ ) )
20	19	3ad2ant2	⊢ ( ( ( ( 𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ) ∧ 𝑧 ∈ ( 𝑥 (,) 𝑦 ) ) ∧ ( 𝑢 ∈ ℚ ∧ 𝑣 ∈ ℚ ) ∧ ( ( 𝑥 < 𝑢 ∧ 𝑢 < 𝑧 ) ∧ ( 𝑧 < 𝑣 ∧ 𝑣 < 𝑦 ) ) ) → ⟨ 𝑢 , 𝑣 ⟩ ∈ ( ℚ × ℚ ) )
21		ffun	⊢ ( (,) : ( ℝ^* × ℝ^* ) ⟶ 𝒫 ℝ → Fun (,) )
22	3 21	ax-mp	⊢ Fun (,)
23		qssre	⊢ ℚ ⊆ ℝ
24		ressxr	⊢ ℝ ⊆ ℝ^*
25	23 24	sstri	⊢ ℚ ⊆ ℝ^*
26		xpss12	⊢ ( ( ℚ ⊆ ℝ^* ∧ ℚ ⊆ ℝ^* ) → ( ℚ × ℚ ) ⊆ ( ℝ^* × ℝ^* ) )
27	25 25 26	mp2an	⊢ ( ℚ × ℚ ) ⊆ ( ℝ^* × ℝ^* )
28	3	fdmi	⊢ dom (,) = ( ℝ^* × ℝ^* )
29	27 28	sseqtrri	⊢ ( ℚ × ℚ ) ⊆ dom (,)
30		funfvima2	⊢ ( ( Fun (,) ∧ ( ℚ × ℚ ) ⊆ dom (,) ) → ( ⟨ 𝑢 , 𝑣 ⟩ ∈ ( ℚ × ℚ ) → ( (,) ‘ ⟨ 𝑢 , 𝑣 ⟩ ) ∈ ( (,) “ ( ℚ × ℚ ) ) ) )
31	22 29 30	mp2an	⊢ ( ⟨ 𝑢 , 𝑣 ⟩ ∈ ( ℚ × ℚ ) → ( (,) ‘ ⟨ 𝑢 , 𝑣 ⟩ ) ∈ ( (,) “ ( ℚ × ℚ ) ) )
32	20 31	syl	⊢ ( ( ( ( 𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ) ∧ 𝑧 ∈ ( 𝑥 (,) 𝑦 ) ) ∧ ( 𝑢 ∈ ℚ ∧ 𝑣 ∈ ℚ ) ∧ ( ( 𝑥 < 𝑢 ∧ 𝑢 < 𝑧 ) ∧ ( 𝑧 < 𝑣 ∧ 𝑣 < 𝑦 ) ) ) → ( (,) ‘ ⟨ 𝑢 , 𝑣 ⟩ ) ∈ ( (,) “ ( ℚ × ℚ ) ) )
33	18 32	eqeltrid	⊢ ( ( ( ( 𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ) ∧ 𝑧 ∈ ( 𝑥 (,) 𝑦 ) ) ∧ ( 𝑢 ∈ ℚ ∧ 𝑣 ∈ ℚ ) ∧ ( ( 𝑥 < 𝑢 ∧ 𝑢 < 𝑧 ) ∧ ( 𝑧 < 𝑣 ∧ 𝑣 < 𝑦 ) ) ) → ( 𝑢 (,) 𝑣 ) ∈ ( (,) “ ( ℚ × ℚ ) ) )
34	9	3ad2ant1	⊢ ( ( ( ( 𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ) ∧ 𝑧 ∈ ( 𝑥 (,) 𝑦 ) ) ∧ ( 𝑢 ∈ ℚ ∧ 𝑣 ∈ ℚ ) ∧ ( ( 𝑥 < 𝑢 ∧ 𝑢 < 𝑧 ) ∧ ( 𝑧 < 𝑣 ∧ 𝑣 < 𝑦 ) ) ) → 𝑧 ∈ ℝ^* )
35		simp3lr	⊢ ( ( ( ( 𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ) ∧ 𝑧 ∈ ( 𝑥 (,) 𝑦 ) ) ∧ ( 𝑢 ∈ ℚ ∧ 𝑣 ∈ ℚ ) ∧ ( ( 𝑥 < 𝑢 ∧ 𝑢 < 𝑧 ) ∧ ( 𝑧 < 𝑣 ∧ 𝑣 < 𝑦 ) ) ) → 𝑢 < 𝑧 )
36		simp3rl	⊢ ( ( ( ( 𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ) ∧ 𝑧 ∈ ( 𝑥 (,) 𝑦 ) ) ∧ ( 𝑢 ∈ ℚ ∧ 𝑣 ∈ ℚ ) ∧ ( ( 𝑥 < 𝑢 ∧ 𝑢 < 𝑧 ) ∧ ( 𝑧 < 𝑣 ∧ 𝑣 < 𝑦 ) ) ) → 𝑧 < 𝑣 )
37		simp2l	⊢ ( ( ( ( 𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ) ∧ 𝑧 ∈ ( 𝑥 (,) 𝑦 ) ) ∧ ( 𝑢 ∈ ℚ ∧ 𝑣 ∈ ℚ ) ∧ ( ( 𝑥 < 𝑢 ∧ 𝑢 < 𝑧 ) ∧ ( 𝑧 < 𝑣 ∧ 𝑣 < 𝑦 ) ) ) → 𝑢 ∈ ℚ )
38	25 37	sseldi	⊢ ( ( ( ( 𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ) ∧ 𝑧 ∈ ( 𝑥 (,) 𝑦 ) ) ∧ ( 𝑢 ∈ ℚ ∧ 𝑣 ∈ ℚ ) ∧ ( ( 𝑥 < 𝑢 ∧ 𝑢 < 𝑧 ) ∧ ( 𝑧 < 𝑣 ∧ 𝑣 < 𝑦 ) ) ) → 𝑢 ∈ ℝ^* )
39		simp2r	⊢ ( ( ( ( 𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ) ∧ 𝑧 ∈ ( 𝑥 (,) 𝑦 ) ) ∧ ( 𝑢 ∈ ℚ ∧ 𝑣 ∈ ℚ ) ∧ ( ( 𝑥 < 𝑢 ∧ 𝑢 < 𝑧 ) ∧ ( 𝑧 < 𝑣 ∧ 𝑣 < 𝑦 ) ) ) → 𝑣 ∈ ℚ )
40	25 39	sseldi	⊢ ( ( ( ( 𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ) ∧ 𝑧 ∈ ( 𝑥 (,) 𝑦 ) ) ∧ ( 𝑢 ∈ ℚ ∧ 𝑣 ∈ ℚ ) ∧ ( ( 𝑥 < 𝑢 ∧ 𝑢 < 𝑧 ) ∧ ( 𝑧 < 𝑣 ∧ 𝑣 < 𝑦 ) ) ) → 𝑣 ∈ ℝ^* )
41		elioo1	⊢ ( ( 𝑢 ∈ ℝ^* ∧ 𝑣 ∈ ℝ^* ) → ( 𝑧 ∈ ( 𝑢 (,) 𝑣 ) ↔ ( 𝑧 ∈ ℝ^* ∧ 𝑢 < 𝑧 ∧ 𝑧 < 𝑣 ) ) )
42	38 40 41	syl2anc	⊢ ( ( ( ( 𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ) ∧ 𝑧 ∈ ( 𝑥 (,) 𝑦 ) ) ∧ ( 𝑢 ∈ ℚ ∧ 𝑣 ∈ ℚ ) ∧ ( ( 𝑥 < 𝑢 ∧ 𝑢 < 𝑧 ) ∧ ( 𝑧 < 𝑣 ∧ 𝑣 < 𝑦 ) ) ) → ( 𝑧 ∈ ( 𝑢 (,) 𝑣 ) ↔ ( 𝑧 ∈ ℝ^* ∧ 𝑢 < 𝑧 ∧ 𝑧 < 𝑣 ) ) )
43	34 35 36 42	mpbir3and	⊢ ( ( ( ( 𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ) ∧ 𝑧 ∈ ( 𝑥 (,) 𝑦 ) ) ∧ ( 𝑢 ∈ ℚ ∧ 𝑣 ∈ ℚ ) ∧ ( ( 𝑥 < 𝑢 ∧ 𝑢 < 𝑧 ) ∧ ( 𝑧 < 𝑣 ∧ 𝑣 < 𝑦 ) ) ) → 𝑧 ∈ ( 𝑢 (,) 𝑣 ) )
44	6	3ad2ant1	⊢ ( ( ( ( 𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ) ∧ 𝑧 ∈ ( 𝑥 (,) 𝑦 ) ) ∧ ( 𝑢 ∈ ℚ ∧ 𝑣 ∈ ℚ ) ∧ ( ( 𝑥 < 𝑢 ∧ 𝑢 < 𝑧 ) ∧ ( 𝑧 < 𝑣 ∧ 𝑣 < 𝑦 ) ) ) → 𝑥 ∈ ℝ^* )
45		simp3ll	⊢ ( ( ( ( 𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ) ∧ 𝑧 ∈ ( 𝑥 (,) 𝑦 ) ) ∧ ( 𝑢 ∈ ℚ ∧ 𝑣 ∈ ℚ ) ∧ ( ( 𝑥 < 𝑢 ∧ 𝑢 < 𝑧 ) ∧ ( 𝑧 < 𝑣 ∧ 𝑣 < 𝑦 ) ) ) → 𝑥 < 𝑢 )
46	44 38 45	xrltled	⊢ ( ( ( ( 𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ) ∧ 𝑧 ∈ ( 𝑥 (,) 𝑦 ) ) ∧ ( 𝑢 ∈ ℚ ∧ 𝑣 ∈ ℚ ) ∧ ( ( 𝑥 < 𝑢 ∧ 𝑢 < 𝑧 ) ∧ ( 𝑧 < 𝑣 ∧ 𝑣 < 𝑦 ) ) ) → 𝑥 ≤ 𝑢 )
47		iooss1	⊢ ( ( 𝑥 ∈ ℝ^* ∧ 𝑥 ≤ 𝑢 ) → ( 𝑢 (,) 𝑣 ) ⊆ ( 𝑥 (,) 𝑣 ) )
48	44 46 47	syl2anc	⊢ ( ( ( ( 𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ) ∧ 𝑧 ∈ ( 𝑥 (,) 𝑦 ) ) ∧ ( 𝑢 ∈ ℚ ∧ 𝑣 ∈ ℚ ) ∧ ( ( 𝑥 < 𝑢 ∧ 𝑢 < 𝑧 ) ∧ ( 𝑧 < 𝑣 ∧ 𝑣 < 𝑦 ) ) ) → ( 𝑢 (,) 𝑣 ) ⊆ ( 𝑥 (,) 𝑣 ) )
49	13	3ad2ant1	⊢ ( ( ( ( 𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ) ∧ 𝑧 ∈ ( 𝑥 (,) 𝑦 ) ) ∧ ( 𝑢 ∈ ℚ ∧ 𝑣 ∈ ℚ ) ∧ ( ( 𝑥 < 𝑢 ∧ 𝑢 < 𝑧 ) ∧ ( 𝑧 < 𝑣 ∧ 𝑣 < 𝑦 ) ) ) → 𝑦 ∈ ℝ^* )
50		simp3rr	⊢ ( ( ( ( 𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ) ∧ 𝑧 ∈ ( 𝑥 (,) 𝑦 ) ) ∧ ( 𝑢 ∈ ℚ ∧ 𝑣 ∈ ℚ ) ∧ ( ( 𝑥 < 𝑢 ∧ 𝑢 < 𝑧 ) ∧ ( 𝑧 < 𝑣 ∧ 𝑣 < 𝑦 ) ) ) → 𝑣 < 𝑦 )
51	40 49 50	xrltled	⊢ ( ( ( ( 𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ) ∧ 𝑧 ∈ ( 𝑥 (,) 𝑦 ) ) ∧ ( 𝑢 ∈ ℚ ∧ 𝑣 ∈ ℚ ) ∧ ( ( 𝑥 < 𝑢 ∧ 𝑢 < 𝑧 ) ∧ ( 𝑧 < 𝑣 ∧ 𝑣 < 𝑦 ) ) ) → 𝑣 ≤ 𝑦 )
52		iooss2	⊢ ( ( 𝑦 ∈ ℝ^* ∧ 𝑣 ≤ 𝑦 ) → ( 𝑥 (,) 𝑣 ) ⊆ ( 𝑥 (,) 𝑦 ) )
53	49 51 52	syl2anc	⊢ ( ( ( ( 𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ) ∧ 𝑧 ∈ ( 𝑥 (,) 𝑦 ) ) ∧ ( 𝑢 ∈ ℚ ∧ 𝑣 ∈ ℚ ) ∧ ( ( 𝑥 < 𝑢 ∧ 𝑢 < 𝑧 ) ∧ ( 𝑧 < 𝑣 ∧ 𝑣 < 𝑦 ) ) ) → ( 𝑥 (,) 𝑣 ) ⊆ ( 𝑥 (,) 𝑦 ) )
54	48 53	sstrd	⊢ ( ( ( ( 𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ) ∧ 𝑧 ∈ ( 𝑥 (,) 𝑦 ) ) ∧ ( 𝑢 ∈ ℚ ∧ 𝑣 ∈ ℚ ) ∧ ( ( 𝑥 < 𝑢 ∧ 𝑢 < 𝑧 ) ∧ ( 𝑧 < 𝑣 ∧ 𝑣 < 𝑦 ) ) ) → ( 𝑢 (,) 𝑣 ) ⊆ ( 𝑥 (,) 𝑦 ) )
55		eleq2	⊢ ( 𝑤 = ( 𝑢 (,) 𝑣 ) → ( 𝑧 ∈ 𝑤 ↔ 𝑧 ∈ ( 𝑢 (,) 𝑣 ) ) )
56		sseq1	⊢ ( 𝑤 = ( 𝑢 (,) 𝑣 ) → ( 𝑤 ⊆ ( 𝑥 (,) 𝑦 ) ↔ ( 𝑢 (,) 𝑣 ) ⊆ ( 𝑥 (,) 𝑦 ) ) )
57	55 56	anbi12d	⊢ ( 𝑤 = ( 𝑢 (,) 𝑣 ) → ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 (,) 𝑦 ) ) ↔ ( 𝑧 ∈ ( 𝑢 (,) 𝑣 ) ∧ ( 𝑢 (,) 𝑣 ) ⊆ ( 𝑥 (,) 𝑦 ) ) ) )
58	57	rspcev	⊢ ( ( ( 𝑢 (,) 𝑣 ) ∈ ( (,) “ ( ℚ × ℚ ) ) ∧ ( 𝑧 ∈ ( 𝑢 (,) 𝑣 ) ∧ ( 𝑢 (,) 𝑣 ) ⊆ ( 𝑥 (,) 𝑦 ) ) ) → ∃ 𝑤 ∈ ( (,) “ ( ℚ × ℚ ) ) ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 (,) 𝑦 ) ) )
59	33 43 54 58	syl12anc	⊢ ( ( ( ( 𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ) ∧ 𝑧 ∈ ( 𝑥 (,) 𝑦 ) ) ∧ ( 𝑢 ∈ ℚ ∧ 𝑣 ∈ ℚ ) ∧ ( ( 𝑥 < 𝑢 ∧ 𝑢 < 𝑧 ) ∧ ( 𝑧 < 𝑣 ∧ 𝑣 < 𝑦 ) ) ) → ∃ 𝑤 ∈ ( (,) “ ( ℚ × ℚ ) ) ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 (,) 𝑦 ) ) )
60	59	3exp	⊢ ( ( ( 𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ) ∧ 𝑧 ∈ ( 𝑥 (,) 𝑦 ) ) → ( ( 𝑢 ∈ ℚ ∧ 𝑣 ∈ ℚ ) → ( ( ( 𝑥 < 𝑢 ∧ 𝑢 < 𝑧 ) ∧ ( 𝑧 < 𝑣 ∧ 𝑣 < 𝑦 ) ) → ∃ 𝑤 ∈ ( (,) “ ( ℚ × ℚ ) ) ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 (,) 𝑦 ) ) ) ) )
61	60	rexlimdvv	⊢ ( ( ( 𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ) ∧ 𝑧 ∈ ( 𝑥 (,) 𝑦 ) ) → ( ∃ 𝑢 ∈ ℚ ∃ 𝑣 ∈ ℚ ( ( 𝑥 < 𝑢 ∧ 𝑢 < 𝑧 ) ∧ ( 𝑧 < 𝑣 ∧ 𝑣 < 𝑦 ) ) → ∃ 𝑤 ∈ ( (,) “ ( ℚ × ℚ ) ) ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 (,) 𝑦 ) ) ) )
62	17 61	syl5bir	⊢ ( ( ( 𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ) ∧ 𝑧 ∈ ( 𝑥 (,) 𝑦 ) ) → ( ( ∃ 𝑢 ∈ ℚ ( 𝑥 < 𝑢 ∧ 𝑢 < 𝑧 ) ∧ ∃ 𝑣 ∈ ℚ ( 𝑧 < 𝑣 ∧ 𝑣 < 𝑦 ) ) → ∃ 𝑤 ∈ ( (,) “ ( ℚ × ℚ ) ) ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 (,) 𝑦 ) ) ) )
63	12 16 62	mp2and	⊢ ( ( ( 𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ) ∧ 𝑧 ∈ ( 𝑥 (,) 𝑦 ) ) → ∃ 𝑤 ∈ ( (,) “ ( ℚ × ℚ ) ) ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 (,) 𝑦 ) ) )
64	63	ralrimiva	⊢ ( ( 𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ) → ∀ 𝑧 ∈ ( 𝑥 (,) 𝑦 ) ∃ 𝑤 ∈ ( (,) “ ( ℚ × ℚ ) ) ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 (,) 𝑦 ) ) )
65		qtopbas	⊢ ( (,) “ ( ℚ × ℚ ) ) ∈ TopBases
66		eltg2b	⊢ ( ( (,) “ ( ℚ × ℚ ) ) ∈ TopBases → ( ( 𝑥 (,) 𝑦 ) ∈ ( topGen ‘ ( (,) “ ( ℚ × ℚ ) ) ) ↔ ∀ 𝑧 ∈ ( 𝑥 (,) 𝑦 ) ∃ 𝑤 ∈ ( (,) “ ( ℚ × ℚ ) ) ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 (,) 𝑦 ) ) ) )
67	65 66	ax-mp	⊢ ( ( 𝑥 (,) 𝑦 ) ∈ ( topGen ‘ ( (,) “ ( ℚ × ℚ ) ) ) ↔ ∀ 𝑧 ∈ ( 𝑥 (,) 𝑦 ) ∃ 𝑤 ∈ ( (,) “ ( ℚ × ℚ ) ) ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 (,) 𝑦 ) ) )
68	64 67	sylibr	⊢ ( ( 𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ) → ( 𝑥 (,) 𝑦 ) ∈ ( topGen ‘ ( (,) “ ( ℚ × ℚ ) ) ) )
69	68	rgen2	⊢ ∀ 𝑥 ∈ ℝ^* ∀ 𝑦 ∈ ℝ^* ( 𝑥 (,) 𝑦 ) ∈ ( topGen ‘ ( (,) “ ( ℚ × ℚ ) ) )
70		ffnov	⊢ ( (,) : ( ℝ^* × ℝ^* ) ⟶ ( topGen ‘ ( (,) “ ( ℚ × ℚ ) ) ) ↔ ( (,) Fn ( ℝ^* × ℝ^* ) ∧ ∀ 𝑥 ∈ ℝ^* ∀ 𝑦 ∈ ℝ^* ( 𝑥 (,) 𝑦 ) ∈ ( topGen ‘ ( (,) “ ( ℚ × ℚ ) ) ) ) )
71	5 69 70	mpbir2an	⊢ (,) : ( ℝ^* × ℝ^* ) ⟶ ( topGen ‘ ( (,) “ ( ℚ × ℚ ) ) )
72		frn	⊢ ( (,) : ( ℝ^* × ℝ^* ) ⟶ ( topGen ‘ ( (,) “ ( ℚ × ℚ ) ) ) → ran (,) ⊆ ( topGen ‘ ( (,) “ ( ℚ × ℚ ) ) ) )
73	71 72	ax-mp	⊢ ran (,) ⊆ ( topGen ‘ ( (,) “ ( ℚ × ℚ ) ) )
74		2basgen	⊢ ( ( ( (,) “ ( ℚ × ℚ ) ) ⊆ ran (,) ∧ ran (,) ⊆ ( topGen ‘ ( (,) “ ( ℚ × ℚ ) ) ) ) → ( topGen ‘ ( (,) “ ( ℚ × ℚ ) ) ) = ( topGen ‘ ran (,) ) )
75	2 73 74	mp2an	⊢ ( topGen ‘ ( (,) “ ( ℚ × ℚ ) ) ) = ( topGen ‘ ran (,) )
76	1 75	eqtr2i	⊢ ( topGen ‘ ran (,) ) = 𝑄

Metamath Proof Explorer

Theorem tgqioo

Proof