Metamath Proof Explorer

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){↾}_{𝑡}{A}$
cnmptre.3 ${⊢}{K}=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}{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){↾}_{𝑡}{A}$
3 cnmptre.3 ${⊢}{K}=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}{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}{↾}_{𝑡}{A}={R}{↾}_{𝑡}{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}{↾}_{𝑡}{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}{↾}_{𝑡}{A}=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}{A}$
16 4 15 syl ${⊢}{\phi }\to {R}{↾}_{𝑡}{A}=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}{A}$
17 16 2 eqtr4di ${⊢}{\phi }\to {R}{↾}_{𝑡}{A}={J}$
18 17 oveq1d ${⊢}{\phi }\to \left({R}{↾}_{𝑡}{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)↔\left({x}\in {A}⟼{F}\right)\in \left({J}\mathrm{Cn}\left({R}{↾}_{𝑡}{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)↔\left({x}\in {A}⟼{F}\right)\in \left({J}\mathrm{Cn}\left({R}{↾}_{𝑡}{B}\right)\right)\right)$
25 19 24 mpbid ${⊢}{\phi }\to \left({x}\in {A}⟼{F}\right)\in \left({J}\mathrm{Cn}\left({R}{↾}_{𝑡}{B}\right)\right)$
26 1 14 rerest ${⊢}{B}\subseteq ℝ\to {R}{↾}_{𝑡}{B}=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}{B}$
27 5 26 syl ${⊢}{\phi }\to {R}{↾}_{𝑡}{B}=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}{B}$
28 27 3 eqtr4di ${⊢}{\phi }\to {R}{↾}_{𝑡}{B}={K}$
29 28 oveq2d ${⊢}{\phi }\to {J}\mathrm{Cn}\left({R}{↾}_{𝑡}{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)$