# Metamath Proof Explorer

## Theorem 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 ${⊢}{Q}=\mathrm{topGen}\left(\left(.\right)\left[ℚ×ℚ\right]\right)$
Assertion tgqioo ${⊢}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)={Q}$

### Proof

Step Hyp Ref Expression
1 tgqioo.1 ${⊢}{Q}=\mathrm{topGen}\left(\left(.\right)\left[ℚ×ℚ\right]\right)$
2 imassrn ${⊢}\left(.\right)\left[ℚ×ℚ\right]\subseteq \mathrm{ran}\left(.\right)$
3 ioof ${⊢}\left(.\right):{ℝ}^{*}×{ℝ}^{*}⟶𝒫ℝ$
4 ffn ${⊢}\left(.\right):{ℝ}^{*}×{ℝ}^{*}⟶𝒫ℝ\to \left(.\right)Fn\left({ℝ}^{*}×{ℝ}^{*}\right)$
5 3 4 ax-mp ${⊢}\left(.\right)Fn\left({ℝ}^{*}×{ℝ}^{*}\right)$
6 simpll ${⊢}\left(\left({x}\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\wedge {z}\in \left({x},{y}\right)\right)\to {x}\in {ℝ}^{*}$
7 elioo1 ${⊢}\left({x}\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\to \left({z}\in \left({x},{y}\right)↔\left({z}\in {ℝ}^{*}\wedge {x}<{z}\wedge {z}<{y}\right)\right)$
8 7 biimpa ${⊢}\left(\left({x}\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\wedge {z}\in \left({x},{y}\right)\right)\to \left({z}\in {ℝ}^{*}\wedge {x}<{z}\wedge {z}<{y}\right)$
9 8 simp1d ${⊢}\left(\left({x}\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\wedge {z}\in \left({x},{y}\right)\right)\to {z}\in {ℝ}^{*}$
10 8 simp2d ${⊢}\left(\left({x}\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\wedge {z}\in \left({x},{y}\right)\right)\to {x}<{z}$
11 qbtwnxr ${⊢}\left({x}\in {ℝ}^{*}\wedge {z}\in {ℝ}^{*}\wedge {x}<{z}\right)\to \exists {u}\in ℚ\phantom{\rule{.4em}{0ex}}\left({x}<{u}\wedge {u}<{z}\right)$
12 6 9 10 11 syl3anc ${⊢}\left(\left({x}\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\wedge {z}\in \left({x},{y}\right)\right)\to \exists {u}\in ℚ\phantom{\rule{.4em}{0ex}}\left({x}<{u}\wedge {u}<{z}\right)$
13 simplr ${⊢}\left(\left({x}\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\wedge {z}\in \left({x},{y}\right)\right)\to {y}\in {ℝ}^{*}$
14 8 simp3d ${⊢}\left(\left({x}\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\wedge {z}\in \left({x},{y}\right)\right)\to {z}<{y}$
15 qbtwnxr ${⊢}\left({z}\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\wedge {z}<{y}\right)\to \exists {v}\in ℚ\phantom{\rule{.4em}{0ex}}\left({z}<{v}\wedge {v}<{y}\right)$
16 9 13 14 15 syl3anc ${⊢}\left(\left({x}\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\wedge {z}\in \left({x},{y}\right)\right)\to \exists {v}\in ℚ\phantom{\rule{.4em}{0ex}}\left({z}<{v}\wedge {v}<{y}\right)$
17 reeanv ${⊢}\exists {u}\in ℚ\phantom{\rule{.4em}{0ex}}\exists {v}\in ℚ\phantom{\rule{.4em}{0ex}}\left(\left({x}<{u}\wedge {u}<{z}\right)\wedge \left({z}<{v}\wedge {v}<{y}\right)\right)↔\left(\exists {u}\in ℚ\phantom{\rule{.4em}{0ex}}\left({x}<{u}\wedge {u}<{z}\right)\wedge \exists {v}\in ℚ\phantom{\rule{.4em}{0ex}}\left({z}<{v}\wedge {v}<{y}\right)\right)$
18 df-ov ${⊢}\left({u},{v}\right)=\left(.\right)\left(⟨{u},{v}⟩\right)$
19 opelxpi ${⊢}\left({u}\in ℚ\wedge {v}\in ℚ\right)\to ⟨{u},{v}⟩\in \left(ℚ×ℚ\right)$
20 19 3ad2ant2 ${⊢}\left(\left(\left({x}\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\wedge {z}\in \left({x},{y}\right)\right)\wedge \left({u}\in ℚ\wedge {v}\in ℚ\right)\wedge \left(\left({x}<{u}\wedge {u}<{z}\right)\wedge \left({z}<{v}\wedge {v}<{y}\right)\right)\right)\to ⟨{u},{v}⟩\in \left(ℚ×ℚ\right)$
21 ffun ${⊢}\left(.\right):{ℝ}^{*}×{ℝ}^{*}⟶𝒫ℝ\to \mathrm{Fun}\left(.\right)$
22 3 21 ax-mp ${⊢}\mathrm{Fun}\left(.\right)$
23 qssre ${⊢}ℚ\subseteq ℝ$
24 ressxr ${⊢}ℝ\subseteq {ℝ}^{*}$
25 23 24 sstri ${⊢}ℚ\subseteq {ℝ}^{*}$
26 xpss12 ${⊢}\left(ℚ\subseteq {ℝ}^{*}\wedge ℚ\subseteq {ℝ}^{*}\right)\to ℚ×ℚ\subseteq {ℝ}^{*}×{ℝ}^{*}$
27 25 25 26 mp2an ${⊢}ℚ×ℚ\subseteq {ℝ}^{*}×{ℝ}^{*}$
28 3 fdmi ${⊢}\mathrm{dom}\left(.\right)={ℝ}^{*}×{ℝ}^{*}$
29 27 28 sseqtrri ${⊢}ℚ×ℚ\subseteq \mathrm{dom}\left(.\right)$
30 funfvima2 ${⊢}\left(\mathrm{Fun}\left(.\right)\wedge ℚ×ℚ\subseteq \mathrm{dom}\left(.\right)\right)\to \left(⟨{u},{v}⟩\in \left(ℚ×ℚ\right)\to \left(.\right)\left(⟨{u},{v}⟩\right)\in \left(.\right)\left[ℚ×ℚ\right]\right)$
31 22 29 30 mp2an ${⊢}⟨{u},{v}⟩\in \left(ℚ×ℚ\right)\to \left(.\right)\left(⟨{u},{v}⟩\right)\in \left(.\right)\left[ℚ×ℚ\right]$
32 20 31 syl ${⊢}\left(\left(\left({x}\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\wedge {z}\in \left({x},{y}\right)\right)\wedge \left({u}\in ℚ\wedge {v}\in ℚ\right)\wedge \left(\left({x}<{u}\wedge {u}<{z}\right)\wedge \left({z}<{v}\wedge {v}<{y}\right)\right)\right)\to \left(.\right)\left(⟨{u},{v}⟩\right)\in \left(.\right)\left[ℚ×ℚ\right]$
33 18 32 eqeltrid ${⊢}\left(\left(\left({x}\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\wedge {z}\in \left({x},{y}\right)\right)\wedge \left({u}\in ℚ\wedge {v}\in ℚ\right)\wedge \left(\left({x}<{u}\wedge {u}<{z}\right)\wedge \left({z}<{v}\wedge {v}<{y}\right)\right)\right)\to \left({u},{v}\right)\in \left(.\right)\left[ℚ×ℚ\right]$
34 9 3ad2ant1 ${⊢}\left(\left(\left({x}\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\wedge {z}\in \left({x},{y}\right)\right)\wedge \left({u}\in ℚ\wedge {v}\in ℚ\right)\wedge \left(\left({x}<{u}\wedge {u}<{z}\right)\wedge \left({z}<{v}\wedge {v}<{y}\right)\right)\right)\to {z}\in {ℝ}^{*}$
35 simp3lr ${⊢}\left(\left(\left({x}\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\wedge {z}\in \left({x},{y}\right)\right)\wedge \left({u}\in ℚ\wedge {v}\in ℚ\right)\wedge \left(\left({x}<{u}\wedge {u}<{z}\right)\wedge \left({z}<{v}\wedge {v}<{y}\right)\right)\right)\to {u}<{z}$
36 simp3rl ${⊢}\left(\left(\left({x}\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\wedge {z}\in \left({x},{y}\right)\right)\wedge \left({u}\in ℚ\wedge {v}\in ℚ\right)\wedge \left(\left({x}<{u}\wedge {u}<{z}\right)\wedge \left({z}<{v}\wedge {v}<{y}\right)\right)\right)\to {z}<{v}$
37 simp2l ${⊢}\left(\left(\left({x}\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\wedge {z}\in \left({x},{y}\right)\right)\wedge \left({u}\in ℚ\wedge {v}\in ℚ\right)\wedge \left(\left({x}<{u}\wedge {u}<{z}\right)\wedge \left({z}<{v}\wedge {v}<{y}\right)\right)\right)\to {u}\in ℚ$
38 25 37 sseldi ${⊢}\left(\left(\left({x}\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\wedge {z}\in \left({x},{y}\right)\right)\wedge \left({u}\in ℚ\wedge {v}\in ℚ\right)\wedge \left(\left({x}<{u}\wedge {u}<{z}\right)\wedge \left({z}<{v}\wedge {v}<{y}\right)\right)\right)\to {u}\in {ℝ}^{*}$
39 simp2r ${⊢}\left(\left(\left({x}\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\wedge {z}\in \left({x},{y}\right)\right)\wedge \left({u}\in ℚ\wedge {v}\in ℚ\right)\wedge \left(\left({x}<{u}\wedge {u}<{z}\right)\wedge \left({z}<{v}\wedge {v}<{y}\right)\right)\right)\to {v}\in ℚ$
40 25 39 sseldi ${⊢}\left(\left(\left({x}\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\wedge {z}\in \left({x},{y}\right)\right)\wedge \left({u}\in ℚ\wedge {v}\in ℚ\right)\wedge \left(\left({x}<{u}\wedge {u}<{z}\right)\wedge \left({z}<{v}\wedge {v}<{y}\right)\right)\right)\to {v}\in {ℝ}^{*}$
41 elioo1 ${⊢}\left({u}\in {ℝ}^{*}\wedge {v}\in {ℝ}^{*}\right)\to \left({z}\in \left({u},{v}\right)↔\left({z}\in {ℝ}^{*}\wedge {u}<{z}\wedge {z}<{v}\right)\right)$
42 38 40 41 syl2anc ${⊢}\left(\left(\left({x}\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\wedge {z}\in \left({x},{y}\right)\right)\wedge \left({u}\in ℚ\wedge {v}\in ℚ\right)\wedge \left(\left({x}<{u}\wedge {u}<{z}\right)\wedge \left({z}<{v}\wedge {v}<{y}\right)\right)\right)\to \left({z}\in \left({u},{v}\right)↔\left({z}\in {ℝ}^{*}\wedge {u}<{z}\wedge {z}<{v}\right)\right)$
43 34 35 36 42 mpbir3and ${⊢}\left(\left(\left({x}\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\wedge {z}\in \left({x},{y}\right)\right)\wedge \left({u}\in ℚ\wedge {v}\in ℚ\right)\wedge \left(\left({x}<{u}\wedge {u}<{z}\right)\wedge \left({z}<{v}\wedge {v}<{y}\right)\right)\right)\to {z}\in \left({u},{v}\right)$
44 6 3ad2ant1 ${⊢}\left(\left(\left({x}\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\wedge {z}\in \left({x},{y}\right)\right)\wedge \left({u}\in ℚ\wedge {v}\in ℚ\right)\wedge \left(\left({x}<{u}\wedge {u}<{z}\right)\wedge \left({z}<{v}\wedge {v}<{y}\right)\right)\right)\to {x}\in {ℝ}^{*}$
45 simp3ll ${⊢}\left(\left(\left({x}\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\wedge {z}\in \left({x},{y}\right)\right)\wedge \left({u}\in ℚ\wedge {v}\in ℚ\right)\wedge \left(\left({x}<{u}\wedge {u}<{z}\right)\wedge \left({z}<{v}\wedge {v}<{y}\right)\right)\right)\to {x}<{u}$
46 44 38 45 xrltled ${⊢}\left(\left(\left({x}\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\wedge {z}\in \left({x},{y}\right)\right)\wedge \left({u}\in ℚ\wedge {v}\in ℚ\right)\wedge \left(\left({x}<{u}\wedge {u}<{z}\right)\wedge \left({z}<{v}\wedge {v}<{y}\right)\right)\right)\to {x}\le {u}$
47 iooss1 ${⊢}\left({x}\in {ℝ}^{*}\wedge {x}\le {u}\right)\to \left({u},{v}\right)\subseteq \left({x},{v}\right)$
48 44 46 47 syl2anc ${⊢}\left(\left(\left({x}\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\wedge {z}\in \left({x},{y}\right)\right)\wedge \left({u}\in ℚ\wedge {v}\in ℚ\right)\wedge \left(\left({x}<{u}\wedge {u}<{z}\right)\wedge \left({z}<{v}\wedge {v}<{y}\right)\right)\right)\to \left({u},{v}\right)\subseteq \left({x},{v}\right)$
49 13 3ad2ant1 ${⊢}\left(\left(\left({x}\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\wedge {z}\in \left({x},{y}\right)\right)\wedge \left({u}\in ℚ\wedge {v}\in ℚ\right)\wedge \left(\left({x}<{u}\wedge {u}<{z}\right)\wedge \left({z}<{v}\wedge {v}<{y}\right)\right)\right)\to {y}\in {ℝ}^{*}$
50 simp3rr ${⊢}\left(\left(\left({x}\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\wedge {z}\in \left({x},{y}\right)\right)\wedge \left({u}\in ℚ\wedge {v}\in ℚ\right)\wedge \left(\left({x}<{u}\wedge {u}<{z}\right)\wedge \left({z}<{v}\wedge {v}<{y}\right)\right)\right)\to {v}<{y}$
51 40 49 50 xrltled ${⊢}\left(\left(\left({x}\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\wedge {z}\in \left({x},{y}\right)\right)\wedge \left({u}\in ℚ\wedge {v}\in ℚ\right)\wedge \left(\left({x}<{u}\wedge {u}<{z}\right)\wedge \left({z}<{v}\wedge {v}<{y}\right)\right)\right)\to {v}\le {y}$
52 iooss2 ${⊢}\left({y}\in {ℝ}^{*}\wedge {v}\le {y}\right)\to \left({x},{v}\right)\subseteq \left({x},{y}\right)$
53 49 51 52 syl2anc ${⊢}\left(\left(\left({x}\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\wedge {z}\in \left({x},{y}\right)\right)\wedge \left({u}\in ℚ\wedge {v}\in ℚ\right)\wedge \left(\left({x}<{u}\wedge {u}<{z}\right)\wedge \left({z}<{v}\wedge {v}<{y}\right)\right)\right)\to \left({x},{v}\right)\subseteq \left({x},{y}\right)$
54 48 53 sstrd ${⊢}\left(\left(\left({x}\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\wedge {z}\in \left({x},{y}\right)\right)\wedge \left({u}\in ℚ\wedge {v}\in ℚ\right)\wedge \left(\left({x}<{u}\wedge {u}<{z}\right)\wedge \left({z}<{v}\wedge {v}<{y}\right)\right)\right)\to \left({u},{v}\right)\subseteq \left({x},{y}\right)$
55 eleq2 ${⊢}{w}=\left({u},{v}\right)\to \left({z}\in {w}↔{z}\in \left({u},{v}\right)\right)$
56 sseq1 ${⊢}{w}=\left({u},{v}\right)\to \left({w}\subseteq \left({x},{y}\right)↔\left({u},{v}\right)\subseteq \left({x},{y}\right)\right)$
57 55 56 anbi12d ${⊢}{w}=\left({u},{v}\right)\to \left(\left({z}\in {w}\wedge {w}\subseteq \left({x},{y}\right)\right)↔\left({z}\in \left({u},{v}\right)\wedge \left({u},{v}\right)\subseteq \left({x},{y}\right)\right)\right)$
58 57 rspcev ${⊢}\left(\left({u},{v}\right)\in \left(.\right)\left[ℚ×ℚ\right]\wedge \left({z}\in \left({u},{v}\right)\wedge \left({u},{v}\right)\subseteq \left({x},{y}\right)\right)\right)\to \exists {w}\in \left(.\right)\left[ℚ×ℚ\right]\phantom{\rule{.4em}{0ex}}\left({z}\in {w}\wedge {w}\subseteq \left({x},{y}\right)\right)$
59 33 43 54 58 syl12anc ${⊢}\left(\left(\left({x}\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\wedge {z}\in \left({x},{y}\right)\right)\wedge \left({u}\in ℚ\wedge {v}\in ℚ\right)\wedge \left(\left({x}<{u}\wedge {u}<{z}\right)\wedge \left({z}<{v}\wedge {v}<{y}\right)\right)\right)\to \exists {w}\in \left(.\right)\left[ℚ×ℚ\right]\phantom{\rule{.4em}{0ex}}\left({z}\in {w}\wedge {w}\subseteq \left({x},{y}\right)\right)$
60 59 3exp ${⊢}\left(\left({x}\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\wedge {z}\in \left({x},{y}\right)\right)\to \left(\left({u}\in ℚ\wedge {v}\in ℚ\right)\to \left(\left(\left({x}<{u}\wedge {u}<{z}\right)\wedge \left({z}<{v}\wedge {v}<{y}\right)\right)\to \exists {w}\in \left(.\right)\left[ℚ×ℚ\right]\phantom{\rule{.4em}{0ex}}\left({z}\in {w}\wedge {w}\subseteq \left({x},{y}\right)\right)\right)\right)$
61 60 rexlimdvv ${⊢}\left(\left({x}\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\wedge {z}\in \left({x},{y}\right)\right)\to \left(\exists {u}\in ℚ\phantom{\rule{.4em}{0ex}}\exists {v}\in ℚ\phantom{\rule{.4em}{0ex}}\left(\left({x}<{u}\wedge {u}<{z}\right)\wedge \left({z}<{v}\wedge {v}<{y}\right)\right)\to \exists {w}\in \left(.\right)\left[ℚ×ℚ\right]\phantom{\rule{.4em}{0ex}}\left({z}\in {w}\wedge {w}\subseteq \left({x},{y}\right)\right)\right)$
62 17 61 syl5bir ${⊢}\left(\left({x}\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\wedge {z}\in \left({x},{y}\right)\right)\to \left(\left(\exists {u}\in ℚ\phantom{\rule{.4em}{0ex}}\left({x}<{u}\wedge {u}<{z}\right)\wedge \exists {v}\in ℚ\phantom{\rule{.4em}{0ex}}\left({z}<{v}\wedge {v}<{y}\right)\right)\to \exists {w}\in \left(.\right)\left[ℚ×ℚ\right]\phantom{\rule{.4em}{0ex}}\left({z}\in {w}\wedge {w}\subseteq \left({x},{y}\right)\right)\right)$
63 12 16 62 mp2and ${⊢}\left(\left({x}\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\wedge {z}\in \left({x},{y}\right)\right)\to \exists {w}\in \left(.\right)\left[ℚ×ℚ\right]\phantom{\rule{.4em}{0ex}}\left({z}\in {w}\wedge {w}\subseteq \left({x},{y}\right)\right)$
64 63 ralrimiva ${⊢}\left({x}\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\to \forall {z}\in \left({x},{y}\right)\phantom{\rule{.4em}{0ex}}\exists {w}\in \left(.\right)\left[ℚ×ℚ\right]\phantom{\rule{.4em}{0ex}}\left({z}\in {w}\wedge {w}\subseteq \left({x},{y}\right)\right)$
65 qtopbas ${⊢}\left(.\right)\left[ℚ×ℚ\right]\in \mathrm{TopBases}$
66 eltg2b ${⊢}\left(.\right)\left[ℚ×ℚ\right]\in \mathrm{TopBases}\to \left(\left({x},{y}\right)\in \mathrm{topGen}\left(\left(.\right)\left[ℚ×ℚ\right]\right)↔\forall {z}\in \left({x},{y}\right)\phantom{\rule{.4em}{0ex}}\exists {w}\in \left(.\right)\left[ℚ×ℚ\right]\phantom{\rule{.4em}{0ex}}\left({z}\in {w}\wedge {w}\subseteq \left({x},{y}\right)\right)\right)$
67 65 66 ax-mp ${⊢}\left({x},{y}\right)\in \mathrm{topGen}\left(\left(.\right)\left[ℚ×ℚ\right]\right)↔\forall {z}\in \left({x},{y}\right)\phantom{\rule{.4em}{0ex}}\exists {w}\in \left(.\right)\left[ℚ×ℚ\right]\phantom{\rule{.4em}{0ex}}\left({z}\in {w}\wedge {w}\subseteq \left({x},{y}\right)\right)$
68 64 67 sylibr ${⊢}\left({x}\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\to \left({x},{y}\right)\in \mathrm{topGen}\left(\left(.\right)\left[ℚ×ℚ\right]\right)$
69 68 rgen2 ${⊢}\forall {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({x},{y}\right)\in \mathrm{topGen}\left(\left(.\right)\left[ℚ×ℚ\right]\right)$
70 ffnov ${⊢}\left(.\right):{ℝ}^{*}×{ℝ}^{*}⟶\mathrm{topGen}\left(\left(.\right)\left[ℚ×ℚ\right]\right)↔\left(\left(.\right)Fn\left({ℝ}^{*}×{ℝ}^{*}\right)\wedge \forall {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({x},{y}\right)\in \mathrm{topGen}\left(\left(.\right)\left[ℚ×ℚ\right]\right)\right)$
71 5 69 70 mpbir2an ${⊢}\left(.\right):{ℝ}^{*}×{ℝ}^{*}⟶\mathrm{topGen}\left(\left(.\right)\left[ℚ×ℚ\right]\right)$
72 frn ${⊢}\left(.\right):{ℝ}^{*}×{ℝ}^{*}⟶\mathrm{topGen}\left(\left(.\right)\left[ℚ×ℚ\right]\right)\to \mathrm{ran}\left(.\right)\subseteq \mathrm{topGen}\left(\left(.\right)\left[ℚ×ℚ\right]\right)$
73 71 72 ax-mp ${⊢}\mathrm{ran}\left(.\right)\subseteq \mathrm{topGen}\left(\left(.\right)\left[ℚ×ℚ\right]\right)$
74 2basgen ${⊢}\left(\left(.\right)\left[ℚ×ℚ\right]\subseteq \mathrm{ran}\left(.\right)\wedge \mathrm{ran}\left(.\right)\subseteq \mathrm{topGen}\left(\left(.\right)\left[ℚ×ℚ\right]\right)\right)\to \mathrm{topGen}\left(\left(.\right)\left[ℚ×ℚ\right]\right)=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
75 2 73 74 mp2an ${⊢}\mathrm{topGen}\left(\left(.\right)\left[ℚ×ℚ\right]\right)=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
76 1 75 eqtr2i ${⊢}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)={Q}$