Theorem rrhre

Description: The RRHom homomorphism for the real numbers structure is the identity. (Contributed by Thierry Arnoux, 22-Oct-2017)

	Ref	Expression
Assertion	rrhre	$$⊢\mathrm{ℝHom}\left({ℝ}_{\mathrm{fld}}\right)={\mathrm{I}\upharpoonright }_{ℝ}$$

Proof

Step	Hyp	Ref	Expression
1		uniretop	$$⊢ℝ=\bigcup \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
2		rehaus	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{Haus}$$
3	2	a1i	$$⊢\top \to \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{Haus}$$
4		rerrext	$$⊢{ℝ}_{\mathrm{fld}}\in \mathrm{ℝExt}$$
5		eqid	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
6		retopn	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=\mathrm{TopOpen}\left({ℝ}_{\mathrm{fld}}\right)$$
7	5 6	rrhcne	$$⊢{ℝ}_{\mathrm{fld}}\in \mathrm{ℝExt}\to \mathrm{ℝHom}\left({ℝ}_{\mathrm{fld}}\right)\in \left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\mathrm{Cn}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)$$
8	4 7	mp1i	$$⊢\top \to \mathrm{ℝHom}\left({ℝ}_{\mathrm{fld}}\right)\in \left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\mathrm{Cn}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)$$
9		retop	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{Top}$$
10	1	toptopon	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{Top}\leftrightarrow \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{TopOn}\left(ℝ\right)$$
11	9 10	mpbi	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{TopOn}\left(ℝ\right)$$
12		idcn	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{TopOn}\left(ℝ\right)\to {\mathrm{I}\upharpoonright }_{ℝ}\in \left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\mathrm{Cn}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)$$
13	11 12	ax-mp	$$⊢{\mathrm{I}\upharpoonright }_{ℝ}\in \left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\mathrm{Cn}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)$$
14	13	a1i	$$⊢\top \to {\mathrm{I}\upharpoonright }_{ℝ}\in \left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\mathrm{Cn}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)$$
15	9	a1i	$$⊢\top \to \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{Top}$$
16		f1oi	$$⊢\left({\mathrm{I}\upharpoonright }_{\mathbb{Q}}\right):\mathbb{Q}\underset{1-1\; onto}{⟶}\mathbb{Q}$$
17		f1of	$$⊢\left({\mathrm{I}\upharpoonright }_{\mathbb{Q}}\right):\mathbb{Q}\underset{1-1\; onto}{⟶}\mathbb{Q}\to \left({\mathrm{I}\upharpoonright }_{\mathbb{Q}}\right):\mathbb{Q}⟶\mathbb{Q}$$
18	16 17	ax-mp	$$⊢\left({\mathrm{I}\upharpoonright }_{\mathbb{Q}}\right):\mathbb{Q}⟶\mathbb{Q}$$
19		qssre	$$⊢\mathbb{Q}\subseteq ℝ$$
20		fss	$$⊢\left(\left({\mathrm{I}\upharpoonright }_{\mathbb{Q}}\right):\mathbb{Q}⟶\mathbb{Q}\wedge \mathbb{Q}\subseteq ℝ\right)\to \left({\mathrm{I}\upharpoonright }_{\mathbb{Q}}\right):\mathbb{Q}⟶ℝ$$
21	18 19 20	mp2an	$$⊢\left({\mathrm{I}\upharpoonright }_{\mathbb{Q}}\right):\mathbb{Q}⟶ℝ$$
22	21	a1i	$$⊢\top \to \left({\mathrm{I}\upharpoonright }_{\mathbb{Q}}\right):\mathbb{Q}⟶ℝ$$
23	19	a1i	$$⊢\top \to \mathbb{Q}\subseteq ℝ$$
24		qdensere	$$⊢\mathrm{cls}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\mathbb{Q}\right)=ℝ$$
25	24	a1i	$$⊢\top \to \mathrm{cls}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\mathbb{Q}\right)=ℝ$$
26	9	a1i	$$⊢\left(\left(x\in ℝ\wedge a\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\wedge x\in a\right)\to \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{Top}$$
27		simplr	$$⊢\left(\left(x\in ℝ\wedge a\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\wedge x\in a\right)\to a\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
28		simpr	$$⊢\left(\left(x\in ℝ\wedge a\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\wedge x\in a\right)\to x\in a$$
29		opnneip	$$⊢\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{Top}\wedge a\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\wedge x\in a\right)\to a\in \mathrm{nei}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\left\{x\right\}\right)$$
30	26 27 28 29	syl3anc	$$⊢\left(\left(x\in ℝ\wedge a\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\wedge x\in a\right)\to a\in \mathrm{nei}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\left\{x\right\}\right)$$
31		fvex	$$⊢\mathrm{nei}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\left\{x\right\}\right)\in \mathrm{V}$$
32		qex	$$⊢\mathbb{Q}\in \mathrm{V}$$
33		elrestr	$$⊢\left(\mathrm{nei}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\left\{x\right\}\right)\in \mathrm{V}\wedge \mathbb{Q}\in \mathrm{V}\wedge a\in \mathrm{nei}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\left\{x\right\}\right)\right)\to a\cap \mathbb{Q}\in \left(\mathrm{nei}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\left\{x\right\}\right){\upharpoonright }_{𝑡}\mathbb{Q}\right)$$
34	31 32 33	mp3an12	$$⊢a\in \mathrm{nei}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\left\{x\right\}\right)\to a\cap \mathbb{Q}\in \left(\mathrm{nei}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\left\{x\right\}\right){\upharpoonright }_{𝑡}\mathbb{Q}\right)$$
35	30 34	syl	$$⊢\left(\left(x\in ℝ\wedge a\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\wedge x\in a\right)\to a\cap \mathbb{Q}\in \left(\mathrm{nei}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\left\{x\right\}\right){\upharpoonright }_{𝑡}\mathbb{Q}\right)$$
36		inss2	$$⊢a\cap \mathbb{Q}\subseteq \mathbb{Q}$$
37		resiima	$$⊢a\cap \mathbb{Q}\subseteq \mathbb{Q}\to \left({\mathrm{I}\upharpoonright }_{\mathbb{Q}}\right)\left[a\cap \mathbb{Q}\right]=a\cap \mathbb{Q}$$
38	36 37	ax-mp	$$⊢\left({\mathrm{I}\upharpoonright }_{\mathbb{Q}}\right)\left[a\cap \mathbb{Q}\right]=a\cap \mathbb{Q}$$
39		inss1	$$⊢a\cap \mathbb{Q}\subseteq a$$
40	38 39	eqsstri	$$⊢\left({\mathrm{I}\upharpoonright }_{\mathbb{Q}}\right)\left[a\cap \mathbb{Q}\right]\subseteq a$$
41	40	a1i	$$⊢\left(\left(x\in ℝ\wedge a\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\wedge x\in a\right)\to \left({\mathrm{I}\upharpoonright }_{\mathbb{Q}}\right)\left[a\cap \mathbb{Q}\right]\subseteq a$$
42		imaeq2	$$⊢b=a\cap \mathbb{Q}\to \left({\mathrm{I}\upharpoonright }_{\mathbb{Q}}\right)\left[b\right]=\left({\mathrm{I}\upharpoonright }_{\mathbb{Q}}\right)\left[a\cap \mathbb{Q}\right]$$
43	42	sseq1d	$$⊢b=a\cap \mathbb{Q}\to \left(\left({\mathrm{I}\upharpoonright }_{\mathbb{Q}}\right)\left[b\right]\subseteq a\leftrightarrow \left({\mathrm{I}\upharpoonright }_{\mathbb{Q}}\right)\left[a\cap \mathbb{Q}\right]\subseteq a\right)$$
44	43	rspcev	$$⊢\left(a\cap \mathbb{Q}\in \left(\mathrm{nei}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\left\{x\right\}\right){\upharpoonright }_{𝑡}\mathbb{Q}\right)\wedge \left({\mathrm{I}\upharpoonright }_{\mathbb{Q}}\right)\left[a\cap \mathbb{Q}\right]\subseteq a\right)\to \exists b\in \left(\mathrm{nei}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\left\{x\right\}\right){\upharpoonright }_{𝑡}\mathbb{Q}\right)\left({\mathrm{I}\upharpoonright }_{\mathbb{Q}}\right)\left[b\right]\subseteq a$$
45	35 41 44	syl2anc	$$⊢\left(\left(x\in ℝ\wedge a\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\wedge x\in a\right)\to \exists b\in \left(\mathrm{nei}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\left\{x\right\}\right){\upharpoonright }_{𝑡}\mathbb{Q}\right)\left({\mathrm{I}\upharpoonright }_{\mathbb{Q}}\right)\left[b\right]\subseteq a$$
46	45	ex	$$⊢\left(x\in ℝ\wedge a\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\to \left(x\in a\to \exists b\in \left(\mathrm{nei}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\left\{x\right\}\right){\upharpoonright }_{𝑡}\mathbb{Q}\right)\left({\mathrm{I}\upharpoonright }_{\mathbb{Q}}\right)\left[b\right]\subseteq a\right)$$
47	46	ralrimiva	$$⊢x\in ℝ\to \forall a\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\left(x\in a\to \exists b\in \left(\mathrm{nei}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\left\{x\right\}\right){\upharpoonright }_{𝑡}\mathbb{Q}\right)\left({\mathrm{I}\upharpoonright }_{\mathbb{Q}}\right)\left[b\right]\subseteq a\right)$$
48	47	ancli	$$⊢x\in ℝ\to \left(x\in ℝ\wedge \forall a\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\left(x\in a\to \exists b\in \left(\mathrm{nei}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\left\{x\right\}\right){\upharpoonright }_{𝑡}\mathbb{Q}\right)\left({\mathrm{I}\upharpoonright }_{\mathbb{Q}}\right)\left[b\right]\subseteq a\right)\right)$$
49	24	eleq2i	$$⊢x\in \mathrm{cls}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\mathbb{Q}\right)\leftrightarrow x\in ℝ$$
50	49	biimpri	$$⊢x\in ℝ\to x\in \mathrm{cls}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\mathbb{Q}\right)$$
51		trnei	$$⊢\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{TopOn}\left(ℝ\right)\wedge \mathbb{Q}\subseteq ℝ\wedge x\in ℝ\right)\to \left(x\in \mathrm{cls}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\mathbb{Q}\right)\leftrightarrow \mathrm{nei}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\left\{x\right\}\right){\upharpoonright }_{𝑡}\mathbb{Q}\in \mathrm{Fil}\left(\mathbb{Q}\right)\right)$$
52	11 19 51	mp3an12	$$⊢x\in ℝ\to \left(x\in \mathrm{cls}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\mathbb{Q}\right)\leftrightarrow \mathrm{nei}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\left\{x\right\}\right){\upharpoonright }_{𝑡}\mathbb{Q}\in \mathrm{Fil}\left(\mathbb{Q}\right)\right)$$
53	50 52	mpbid	$$⊢x\in ℝ\to \mathrm{nei}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\left\{x\right\}\right){\upharpoonright }_{𝑡}\mathbb{Q}\in \mathrm{Fil}\left(\mathbb{Q}\right)$$
54		isflf	$$⊢\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{TopOn}\left(ℝ\right)\wedge \mathrm{nei}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\left\{x\right\}\right){\upharpoonright }_{𝑡}\mathbb{Q}\in \mathrm{Fil}\left(\mathbb{Q}\right)\wedge \left({\mathrm{I}\upharpoonright }_{\mathbb{Q}}\right):\mathbb{Q}⟶ℝ\right)\to \left(x\in \left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\mathrm{fLimf}\left(\mathrm{nei}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\left\{x\right\}\right){\upharpoonright }_{𝑡}\mathbb{Q}\right)\right)\left({\mathrm{I}\upharpoonright }_{\mathbb{Q}}\right)\leftrightarrow \left(x\in ℝ\wedge \forall a\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\left(x\in a\to \exists b\in \left(\mathrm{nei}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\left\{x\right\}\right){\upharpoonright }_{𝑡}\mathbb{Q}\right)\left({\mathrm{I}\upharpoonright }_{\mathbb{Q}}\right)\left[b\right]\subseteq a\right)\right)\right)$$
55	11 21 54	mp3an13	$$⊢\mathrm{nei}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\left\{x\right\}\right){\upharpoonright }_{𝑡}\mathbb{Q}\in \mathrm{Fil}\left(\mathbb{Q}\right)\to \left(x\in \left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\mathrm{fLimf}\left(\mathrm{nei}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\left\{x\right\}\right){\upharpoonright }_{𝑡}\mathbb{Q}\right)\right)\left({\mathrm{I}\upharpoonright }_{\mathbb{Q}}\right)\leftrightarrow \left(x\in ℝ\wedge \forall a\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\left(x\in a\to \exists b\in \left(\mathrm{nei}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\left\{x\right\}\right){\upharpoonright }_{𝑡}\mathbb{Q}\right)\left({\mathrm{I}\upharpoonright }_{\mathbb{Q}}\right)\left[b\right]\subseteq a\right)\right)\right)$$
56	53 55	syl	$$⊢x\in ℝ\to \left(x\in \left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\mathrm{fLimf}\left(\mathrm{nei}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\left\{x\right\}\right){\upharpoonright }_{𝑡}\mathbb{Q}\right)\right)\left({\mathrm{I}\upharpoonright }_{\mathbb{Q}}\right)\leftrightarrow \left(x\in ℝ\wedge \forall a\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\left(x\in a\to \exists b\in \left(\mathrm{nei}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\left\{x\right\}\right){\upharpoonright }_{𝑡}\mathbb{Q}\right)\left({\mathrm{I}\upharpoonright }_{\mathbb{Q}}\right)\left[b\right]\subseteq a\right)\right)\right)$$
57	48 56	mpbird	$$⊢x\in ℝ\to x\in \left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\mathrm{fLimf}\left(\mathrm{nei}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\left\{x\right\}\right){\upharpoonright }_{𝑡}\mathbb{Q}\right)\right)\left({\mathrm{I}\upharpoonright }_{\mathbb{Q}}\right)$$
58	57	ne0d	$$⊢x\in ℝ\to \left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\mathrm{fLimf}\left(\mathrm{nei}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\left\{x\right\}\right){\upharpoonright }_{𝑡}\mathbb{Q}\right)\right)\left({\mathrm{I}\upharpoonright }_{\mathbb{Q}}\right)\ne \varnothing$$
59	58	adantl	$$⊢\left(\top \wedge x\in ℝ\right)\to \left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\mathrm{fLimf}\left(\mathrm{nei}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\left\{x\right\}\right){\upharpoonright }_{𝑡}\mathbb{Q}\right)\right)\left({\mathrm{I}\upharpoonright }_{\mathbb{Q}}\right)\ne \varnothing$$
60		recusp	$$⊢{ℝ}_{\mathrm{fld}}\in \mathrm{CUnifSp}$$
61		cuspusp	$$⊢{ℝ}_{\mathrm{fld}}\in \mathrm{CUnifSp}\to {ℝ}_{\mathrm{fld}}\in \mathrm{UnifSp}$$
62	60 61	ax-mp	$$⊢{ℝ}_{\mathrm{fld}}\in \mathrm{UnifSp}$$
63	6	uspreg	$$⊢\left({ℝ}_{\mathrm{fld}}\in \mathrm{UnifSp}\wedge \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{Haus}\right)\to \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{Reg}$$
64	62 2 63	mp2an	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{Reg}$$
65	64	a1i	$$⊢\top \to \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{Reg}$$
66		resabs1	$$⊢\mathbb{Q}\subseteq ℝ\to {\left({\mathrm{I}\upharpoonright }_{ℝ}\right)\upharpoonright }_{\mathbb{Q}}={\mathrm{I}\upharpoonright }_{\mathbb{Q}}$$
67	19 66	ax-mp	$$⊢{\left({\mathrm{I}\upharpoonright }_{ℝ}\right)\upharpoonright }_{\mathbb{Q}}={\mathrm{I}\upharpoonright }_{\mathbb{Q}}$$
68	1	cnrest	$$⊢\left({\mathrm{I}\upharpoonright }_{ℝ}\in \left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\mathrm{Cn}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\wedge \mathbb{Q}\subseteq ℝ\right)\to {\left({\mathrm{I}\upharpoonright }_{ℝ}\right)\upharpoonright }_{\mathbb{Q}}\in \left(\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){\upharpoonright }_{𝑡}\mathbb{Q}\right)\mathrm{Cn}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)$$
69	13 19 68	mp2an	$$⊢{\left({\mathrm{I}\upharpoonright }_{ℝ}\right)\upharpoonright }_{\mathbb{Q}}\in \left(\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){\upharpoonright }_{𝑡}\mathbb{Q}\right)\mathrm{Cn}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)$$
70	67 69	eqeltrri	$$⊢{\mathrm{I}\upharpoonright }_{\mathbb{Q}}\in \left(\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){\upharpoonright }_{𝑡}\mathbb{Q}\right)\mathrm{Cn}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)$$
71	70	a1i	$$⊢\top \to {\mathrm{I}\upharpoonright }_{\mathbb{Q}}\in \left(\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){\upharpoonright }_{𝑡}\mathbb{Q}\right)\mathrm{Cn}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)$$
72	1 1 15 3 22 23 25 59 65 71	cnextfres1	$$⊢\top \to {\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\mathrm{CnExt}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left({\mathrm{I}\upharpoonright }_{\mathbb{Q}}\right)\upharpoonright }_{\mathbb{Q}}={\mathrm{I}\upharpoonright }_{\mathbb{Q}}$$
73	72	mptru	$$⊢{\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\mathrm{CnExt}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left({\mathrm{I}\upharpoonright }_{\mathbb{Q}}\right)\upharpoonright }_{\mathbb{Q}}={\mathrm{I}\upharpoonright }_{\mathbb{Q}}$$
74		recms	$$⊢{ℝ}_{\mathrm{fld}}\in \mathrm{CMetSp}$$
75	74	elexi	$$⊢{ℝ}_{\mathrm{fld}}\in \mathrm{V}$$
76	5 6	rrhval	$$⊢{ℝ}_{\mathrm{fld}}\in \mathrm{V}\to \mathrm{ℝHom}\left({ℝ}_{\mathrm{fld}}\right)=\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\mathrm{CnExt}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\mathrm{\mathbb{Q}Hom}\left({ℝ}_{\mathrm{fld}}\right)\right)$$
77	75 76	ax-mp	$$⊢\mathrm{ℝHom}\left({ℝ}_{\mathrm{fld}}\right)=\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\mathrm{CnExt}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\mathrm{\mathbb{Q}Hom}\left({ℝ}_{\mathrm{fld}}\right)\right)$$
78		qqhre	$$⊢\mathrm{\mathbb{Q}Hom}\left({ℝ}_{\mathrm{fld}}\right)={\mathrm{I}\upharpoonright }_{\mathbb{Q}}$$
79	78	fveq2i	$$⊢\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\mathrm{CnExt}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\mathrm{\mathbb{Q}Hom}\left({ℝ}_{\mathrm{fld}}\right)\right)=\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\mathrm{CnExt}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left({\mathrm{I}\upharpoonright }_{\mathbb{Q}}\right)$$
80	77 79	eqtri	$$⊢\mathrm{ℝHom}\left({ℝ}_{\mathrm{fld}}\right)=\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\mathrm{CnExt}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left({\mathrm{I}\upharpoonright }_{\mathbb{Q}}\right)$$
81	80	reseq1i	$$⊢{\mathrm{ℝHom}\left({ℝ}_{\mathrm{fld}}\right)\upharpoonright }_{\mathbb{Q}}={\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\mathrm{CnExt}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left({\mathrm{I}\upharpoonright }_{\mathbb{Q}}\right)\upharpoonright }_{\mathbb{Q}}$$
82	73 81 67	3eqtr4i	$$⊢{\mathrm{ℝHom}\left({ℝ}_{\mathrm{fld}}\right)\upharpoonright }_{\mathbb{Q}}={\left({\mathrm{I}\upharpoonright }_{ℝ}\right)\upharpoonright }_{\mathbb{Q}}$$
83	82	a1i	$$⊢\top \to {\mathrm{ℝHom}\left({ℝ}_{\mathrm{fld}}\right)\upharpoonright }_{\mathbb{Q}}={\left({\mathrm{I}\upharpoonright }_{ℝ}\right)\upharpoonright }_{\mathbb{Q}}$$
84	1 3 8 14 83 23 25	hauseqcn	$$⊢\top \to \mathrm{ℝHom}\left({ℝ}_{\mathrm{fld}}\right)={\mathrm{I}\upharpoonright }_{ℝ}$$
85	84	mptru	$$⊢\mathrm{ℝHom}\left({ℝ}_{\mathrm{fld}}\right)={\mathrm{I}\upharpoonright }_{ℝ}$$