Theorem cnmptre

Description: Lemma for iirevcn and related functions. (Contributed by Mario Carneiro, 6-Jun-2014)

	Ref	Expression
Hypotheses	cnmptre.1	$$⊢R=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
	cnmptre.2	$$⊢J=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){\upharpoonright }_{𝑡}A$$
	cnmptre.3	$$⊢K=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){\upharpoonright }_{𝑡}B$$
	cnmptre.4	$$⊢\phi \to A\subseteq ℝ$$
	cnmptre.5	$$⊢\phi \to B\subseteq ℝ$$
	cnmptre.6	$$⊢\left(\phi \wedge x\in A\right)\to F\in B$$
	cnmptre.7	$$⊢\phi \to \left(x\in ℂ⟼F\right)\in \left(R\mathrm{Cn}R\right)$$
Assertion	cnmptre	$$⊢\phi \to \left(x\in A⟼F\right)\in \left(J\mathrm{Cn}K\right)$$

Proof

Step	Hyp	Ref	Expression
1		cnmptre.1	$$⊢R=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
2		cnmptre.2	$$⊢J=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){\upharpoonright }_{𝑡}A$$
3		cnmptre.3	$$⊢K=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){\upharpoonright }_{𝑡}B$$
4		cnmptre.4	$$⊢\phi \to A\subseteq ℝ$$
5		cnmptre.5	$$⊢\phi \to B\subseteq ℝ$$
6		cnmptre.6	$$⊢\left(\phi \wedge x\in A\right)\to F\in B$$
7		cnmptre.7	$$⊢\phi \to \left(x\in ℂ⟼F\right)\in \left(R\mathrm{Cn}R\right)$$
8		eqid	$$⊢R{\upharpoonright }_{𝑡}A=R{\upharpoonright }_{𝑡}A$$
9	1	cnfldtopon	$$⊢R\in \mathrm{TopOn}\left(ℂ\right)$$
10	9	a1i	$$⊢\phi \to R\in \mathrm{TopOn}\left(ℂ\right)$$
11		ax-resscn	$$⊢ℝ\subseteq ℂ$$
12	4 11	sstrdi	$$⊢\phi \to A\subseteq ℂ$$
13	8 10 12 7	cnmpt1res	$$⊢\phi \to \left(x\in A⟼F\right)\in \left(\left(R{\upharpoonright }_{𝑡}A\right)\mathrm{Cn}R\right)$$
14		eqid	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
15	1 14	rerest	$$⊢A\subseteq ℝ\to R{\upharpoonright }_{𝑡}A=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){\upharpoonright }_{𝑡}A$$
16	4 15	syl	$$⊢\phi \to R{\upharpoonright }_{𝑡}A=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){\upharpoonright }_{𝑡}A$$
17	16 2	syl6eqr	$$⊢\phi \to R{\upharpoonright }_{𝑡}A=J$$
18	17	oveq1d	$$⊢\phi \to \left(R{\upharpoonright }_{𝑡}A\right)\mathrm{Cn}R=J\mathrm{Cn}R$$
19	13 18	eleqtrd	$$⊢\phi \to \left(x\in A⟼F\right)\in \left(J\mathrm{Cn}R\right)$$
20	6	fmpttd	$$⊢\phi \to \left(x\in A⟼F\right):A⟶B$$
21	20	frnd	$$⊢\phi \to \mathrm{ran}\left(x\in A⟼F\right)\subseteq B$$
22	5 11	sstrdi	$$⊢\phi \to B\subseteq ℂ$$
23		cnrest2	$$⊢\left(R\in \mathrm{TopOn}\left(ℂ\right)\wedge \mathrm{ran}\left(x\in A⟼F\right)\subseteq B\wedge B\subseteq ℂ\right)\to \left(\left(x\in A⟼F\right)\in \left(J\mathrm{Cn}R\right)\leftrightarrow \left(x\in A⟼F\right)\in \left(J\mathrm{Cn}\left(R{\upharpoonright }_{𝑡}B\right)\right)\right)$$
24	9 21 22 23	mp3an2i	$$⊢\phi \to \left(\left(x\in A⟼F\right)\in \left(J\mathrm{Cn}R\right)\leftrightarrow \left(x\in A⟼F\right)\in \left(J\mathrm{Cn}\left(R{\upharpoonright }_{𝑡}B\right)\right)\right)$$
25	19 24	mpbid	$$⊢\phi \to \left(x\in A⟼F\right)\in \left(J\mathrm{Cn}\left(R{\upharpoonright }_{𝑡}B\right)\right)$$
26	1 14	rerest	$$⊢B\subseteq ℝ\to R{\upharpoonright }_{𝑡}B=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){\upharpoonright }_{𝑡}B$$
27	5 26	syl	$$⊢\phi \to R{\upharpoonright }_{𝑡}B=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){\upharpoonright }_{𝑡}B$$
28	27 3	syl6eqr	$$⊢\phi \to R{\upharpoonright }_{𝑡}B=K$$
29	28	oveq2d	$$⊢\phi \to J\mathrm{Cn}\left(R{\upharpoonright }_{𝑡}B\right)=J\mathrm{Cn}K$$
30	25 29	eleqtrd	$$⊢\phi \to \left(x\in A⟼F\right)\in \left(J\mathrm{Cn}K\right)$$