# Metamath Proof Explorer

## Theorem cnmpt2res

Description: The restriction of a continuous function to a subset is continuous. (Contributed by Mario Carneiro, 6-Jun-2014)

Ref Expression
Hypotheses cnmpt1res.2 ${⊢}{K}={J}{↾}_{𝑡}{Y}$
cnmpt1res.3 ${⊢}{\phi }\to {J}\in \mathrm{TopOn}\left({X}\right)$
cnmpt1res.5 ${⊢}{\phi }\to {Y}\subseteq {X}$
cnmpt2res.7 ${⊢}{N}={M}{↾}_{𝑡}{W}$
cnmpt2res.8 ${⊢}{\phi }\to {M}\in \mathrm{TopOn}\left({Z}\right)$
cnmpt2res.9 ${⊢}{\phi }\to {W}\subseteq {Z}$
cnmpt2res.10 ${⊢}{\phi }\to \left({x}\in {X},{y}\in {Z}⟼{A}\right)\in \left(\left({J}{×}_{t}{M}\right)\mathrm{Cn}{L}\right)$
Assertion cnmpt2res ${⊢}{\phi }\to \left({x}\in {Y},{y}\in {W}⟼{A}\right)\in \left(\left({K}{×}_{t}{N}\right)\mathrm{Cn}{L}\right)$

### Proof

Step Hyp Ref Expression
1 cnmpt1res.2 ${⊢}{K}={J}{↾}_{𝑡}{Y}$
2 cnmpt1res.3 ${⊢}{\phi }\to {J}\in \mathrm{TopOn}\left({X}\right)$
3 cnmpt1res.5 ${⊢}{\phi }\to {Y}\subseteq {X}$
4 cnmpt2res.7 ${⊢}{N}={M}{↾}_{𝑡}{W}$
5 cnmpt2res.8 ${⊢}{\phi }\to {M}\in \mathrm{TopOn}\left({Z}\right)$
6 cnmpt2res.9 ${⊢}{\phi }\to {W}\subseteq {Z}$
7 cnmpt2res.10 ${⊢}{\phi }\to \left({x}\in {X},{y}\in {Z}⟼{A}\right)\in \left(\left({J}{×}_{t}{M}\right)\mathrm{Cn}{L}\right)$
8 xpss12 ${⊢}\left({Y}\subseteq {X}\wedge {W}\subseteq {Z}\right)\to {Y}×{W}\subseteq {X}×{Z}$
9 3 6 8 syl2anc ${⊢}{\phi }\to {Y}×{W}\subseteq {X}×{Z}$
10 txtopon ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {M}\in \mathrm{TopOn}\left({Z}\right)\right)\to {J}{×}_{t}{M}\in \mathrm{TopOn}\left({X}×{Z}\right)$
11 2 5 10 syl2anc ${⊢}{\phi }\to {J}{×}_{t}{M}\in \mathrm{TopOn}\left({X}×{Z}\right)$
12 toponuni ${⊢}{J}{×}_{t}{M}\in \mathrm{TopOn}\left({X}×{Z}\right)\to {X}×{Z}=\bigcup \left({J}{×}_{t}{M}\right)$
13 11 12 syl ${⊢}{\phi }\to {X}×{Z}=\bigcup \left({J}{×}_{t}{M}\right)$
14 9 13 sseqtrd ${⊢}{\phi }\to {Y}×{W}\subseteq \bigcup \left({J}{×}_{t}{M}\right)$
15 eqid ${⊢}\bigcup \left({J}{×}_{t}{M}\right)=\bigcup \left({J}{×}_{t}{M}\right)$
16 15 cnrest ${⊢}\left(\left({x}\in {X},{y}\in {Z}⟼{A}\right)\in \left(\left({J}{×}_{t}{M}\right)\mathrm{Cn}{L}\right)\wedge {Y}×{W}\subseteq \bigcup \left({J}{×}_{t}{M}\right)\right)\to {\left({x}\in {X},{y}\in {Z}⟼{A}\right)↾}_{\left({Y}×{W}\right)}\in \left(\left(\left({J}{×}_{t}{M}\right){↾}_{𝑡}\left({Y}×{W}\right)\right)\mathrm{Cn}{L}\right)$
17 7 14 16 syl2anc ${⊢}{\phi }\to {\left({x}\in {X},{y}\in {Z}⟼{A}\right)↾}_{\left({Y}×{W}\right)}\in \left(\left(\left({J}{×}_{t}{M}\right){↾}_{𝑡}\left({Y}×{W}\right)\right)\mathrm{Cn}{L}\right)$
18 resmpo ${⊢}\left({Y}\subseteq {X}\wedge {W}\subseteq {Z}\right)\to {\left({x}\in {X},{y}\in {Z}⟼{A}\right)↾}_{\left({Y}×{W}\right)}=\left({x}\in {Y},{y}\in {W}⟼{A}\right)$
19 3 6 18 syl2anc ${⊢}{\phi }\to {\left({x}\in {X},{y}\in {Z}⟼{A}\right)↾}_{\left({Y}×{W}\right)}=\left({x}\in {Y},{y}\in {W}⟼{A}\right)$
20 topontop ${⊢}{J}\in \mathrm{TopOn}\left({X}\right)\to {J}\in \mathrm{Top}$
21 2 20 syl ${⊢}{\phi }\to {J}\in \mathrm{Top}$
22 topontop ${⊢}{M}\in \mathrm{TopOn}\left({Z}\right)\to {M}\in \mathrm{Top}$
23 5 22 syl ${⊢}{\phi }\to {M}\in \mathrm{Top}$
24 toponmax ${⊢}{J}\in \mathrm{TopOn}\left({X}\right)\to {X}\in {J}$
25 2 24 syl ${⊢}{\phi }\to {X}\in {J}$
26 25 3 ssexd ${⊢}{\phi }\to {Y}\in \mathrm{V}$
27 toponmax ${⊢}{M}\in \mathrm{TopOn}\left({Z}\right)\to {Z}\in {M}$
28 5 27 syl ${⊢}{\phi }\to {Z}\in {M}$
29 28 6 ssexd ${⊢}{\phi }\to {W}\in \mathrm{V}$
30 txrest ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {M}\in \mathrm{Top}\right)\wedge \left({Y}\in \mathrm{V}\wedge {W}\in \mathrm{V}\right)\right)\to \left({J}{×}_{t}{M}\right){↾}_{𝑡}\left({Y}×{W}\right)=\left({J}{↾}_{𝑡}{Y}\right){×}_{t}\left({M}{↾}_{𝑡}{W}\right)$
31 21 23 26 29 30 syl22anc ${⊢}{\phi }\to \left({J}{×}_{t}{M}\right){↾}_{𝑡}\left({Y}×{W}\right)=\left({J}{↾}_{𝑡}{Y}\right){×}_{t}\left({M}{↾}_{𝑡}{W}\right)$
32 1 4 oveq12i ${⊢}{K}{×}_{t}{N}=\left({J}{↾}_{𝑡}{Y}\right){×}_{t}\left({M}{↾}_{𝑡}{W}\right)$
33 31 32 syl6eqr ${⊢}{\phi }\to \left({J}{×}_{t}{M}\right){↾}_{𝑡}\left({Y}×{W}\right)={K}{×}_{t}{N}$
34 33 oveq1d ${⊢}{\phi }\to \left(\left({J}{×}_{t}{M}\right){↾}_{𝑡}\left({Y}×{W}\right)\right)\mathrm{Cn}{L}=\left({K}{×}_{t}{N}\right)\mathrm{Cn}{L}$
35 17 19 34 3eltr3d ${⊢}{\phi }\to \left({x}\in {Y},{y}\in {W}⟼{A}\right)\in \left(\left({K}{×}_{t}{N}\right)\mathrm{Cn}{L}\right)$