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	$⊢ φ \to J \in TopOn (X)$
	cnmpt1res.5	$⊢ φ \to Y \subseteq X$
	cnmpt2res.7	$⊢ N = M ↾_{𝑡} W$
	cnmpt2res.8	$⊢ φ \to M \in TopOn (Z)$
	cnmpt2res.9	$⊢ φ \to W \subseteq Z$
	cnmpt2res.10	$⊢ φ \to (x \in X, y \in Z ⟼ A) \in ((J \times_{t} M) Cn L)$
Assertion	cnmpt2res	$⊢ φ \to (x \in Y, y \in W ⟼ A) \in ((K \times_{t} N) Cn L)$

Proof

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

Metamath Proof Explorer

Theorem cnmpt2res

Proof