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 φ J TopOn X
cnmpt1res.5 φ Y X
cnmpt2res.7 N = M 𝑡 W
cnmpt2res.8 φ M TopOn Z
cnmpt2res.9 φ W Z
cnmpt2res.10 φ x X , y Z A J × t M Cn L
Assertion cnmpt2res φ x Y , y W A K × t N Cn L

Proof

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