cnmpt21

Description: The composition of continuous functions is continuous. (Contributed by Mario Carneiro, 5-May-2014) (Revised by Mario Carneiro, 22-Aug-2015)

	Ref	Expression
Hypotheses	cnmpt21.j	$⊢ φ \to J \in TopOn (X)$
	cnmpt21.k	$⊢ φ \to K \in TopOn (Y)$
	cnmpt21.a	$⊢ φ \to (x \in X, y \in Y ⟼ A) \in ((J \times_{t} K) Cn L)$
	cnmpt21.l	$⊢ φ \to L \in TopOn (Z)$
	cnmpt21.b	$⊢ φ \to (z \in Z ⟼ B) \in (L Cn M)$
	cnmpt21.c	$⊢ z = A \to B = C$
Assertion	cnmpt21	$⊢ φ \to (x \in X, y \in Y ⟼ C) \in ((J \times_{t} K) Cn M)$

Proof

Step	Hyp	Ref	Expression
1		cnmpt21.j	$⊢ φ \to J \in TopOn (X)$
2		cnmpt21.k	$⊢ φ \to K \in TopOn (Y)$
3		cnmpt21.a	$⊢ φ \to (x \in X, y \in Y ⟼ A) \in ((J \times_{t} K) Cn L)$
4		cnmpt21.l	$⊢ φ \to L \in TopOn (Z)$
5		cnmpt21.b	$⊢ φ \to (z \in Z ⟼ B) \in (L Cn M)$
6		cnmpt21.c	$⊢ z = A \to B = C$
7		df-ov	$⊢ x (x \in X, y \in Y ⟼ A) y = (x \in X, y \in Y ⟼ A) (⟨x, y⟩)$
8		simprl	$⊢ (φ \land (x \in X \land y \in Y)) \to x \in X$
9		simprr	$⊢ (φ \land (x \in X \land y \in Y)) \to y \in Y$
10		txtopon	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to J \times_{t} K \in TopOn (X \times Y)$
11	1 2 10	syl2anc	$⊢ φ \to J \times_{t} K \in TopOn (X \times Y)$
12		cnf2	$⊢ (J \times_{t} K \in TopOn (X \times Y) \land L \in TopOn (Z) \land (x \in X, y \in Y ⟼ A) \in ((J \times_{t} K) Cn L)) \to (x \in X, y \in Y ⟼ A) : X \times Y ⟶ Z$
13	11 4 3 12	syl3anc	$⊢ φ \to (x \in X, y \in Y ⟼ A) : X \times Y ⟶ Z$
14		eqid	$⊢ (x \in X, y \in Y ⟼ A) = (x \in X, y \in Y ⟼ A)$
15	14	fmpo	$⊢ \forall x \in X \forall y \in Y A \in Z \leftrightarrow (x \in X, y \in Y ⟼ A) : X \times Y ⟶ Z$
16	13 15	sylibr	$⊢ φ \to \forall x \in X \forall y \in Y A \in Z$
17		rsp2	$⊢ \forall x \in X \forall y \in Y A \in Z \to ((x \in X \land y \in Y) \to A \in Z)$
18	16 17	syl	$⊢ φ \to ((x \in X \land y \in Y) \to A \in Z)$
19	18	imp	$⊢ (φ \land (x \in X \land y \in Y)) \to A \in Z$
20	14	ovmpt4g	$⊢ (x \in X \land y \in Y \land A \in Z) \to x (x \in X, y \in Y ⟼ A) y = A$
21	8 9 19 20	syl3anc	$⊢ (φ \land (x \in X \land y \in Y)) \to x (x \in X, y \in Y ⟼ A) y = A$
22	7 21	syl5eqr	$⊢ (φ \land (x \in X \land y \in Y)) \to (x \in X, y \in Y ⟼ A) (⟨x, y⟩) = A$
23	22	fveq2d	$⊢ (φ \land (x \in X \land y \in Y)) \to (z \in Z ⟼ B) ((x \in X, y \in Y ⟼ A) (⟨x, y⟩)) = (z \in Z ⟼ B) (A)$
24		eqid	$⊢ (z \in Z ⟼ B) = (z \in Z ⟼ B)$
25	6	eleq1d	$⊢ z = A \to (B \in ⋃ M \leftrightarrow C \in ⋃ M)$
26		cntop2	$⊢ (z \in Z ⟼ B) \in (L Cn M) \to M \in Top$
27	5 26	syl	$⊢ φ \to M \in Top$
28		toptopon2	$⊢ M \in Top \leftrightarrow M \in TopOn (⋃ M)$
29	27 28	sylib	$⊢ φ \to M \in TopOn (⋃ M)$
30		cnf2	$⊢ (L \in TopOn (Z) \land M \in TopOn (⋃ M) \land (z \in Z ⟼ B) \in (L Cn M)) \to (z \in Z ⟼ B) : Z ⟶ ⋃ M$
31	4 29 5 30	syl3anc	$⊢ φ \to (z \in Z ⟼ B) : Z ⟶ ⋃ M$
32	24	fmpt	$⊢ \forall z \in Z B \in ⋃ M \leftrightarrow (z \in Z ⟼ B) : Z ⟶ ⋃ M$
33	31 32	sylibr	$⊢ φ \to \forall z \in Z B \in ⋃ M$
34	33	adantr	$⊢ (φ \land (x \in X \land y \in Y)) \to \forall z \in Z B \in ⋃ M$
35	25 34 19	rspcdva	$⊢ (φ \land (x \in X \land y \in Y)) \to C \in ⋃ M$
36	24 6 19 35	fvmptd3	$⊢ (φ \land (x \in X \land y \in Y)) \to (z \in Z ⟼ B) (A) = C$
37	23 36	eqtrd	$⊢ (φ \land (x \in X \land y \in Y)) \to (z \in Z ⟼ B) ((x \in X, y \in Y ⟼ A) (⟨x, y⟩)) = C$
38		opelxpi	$⊢ (x \in X \land y \in Y) \to ⟨x, y⟩ \in (X \times Y)$
39		fvco3	$⊢ ((x \in X, y \in Y ⟼ A) : X \times Y ⟶ Z \land ⟨x, y⟩ \in (X \times Y)) \to ((z \in Z ⟼ B) \circ (x \in X, y \in Y ⟼ A)) (⟨x, y⟩) = (z \in Z ⟼ B) ((x \in X, y \in Y ⟼ A) (⟨x, y⟩))$
40	13 38 39	syl2an	$⊢ (φ \land (x \in X \land y \in Y)) \to ((z \in Z ⟼ B) \circ (x \in X, y \in Y ⟼ A)) (⟨x, y⟩) = (z \in Z ⟼ B) ((x \in X, y \in Y ⟼ A) (⟨x, y⟩))$
41		df-ov	$⊢ x (x \in X, y \in Y ⟼ C) y = (x \in X, y \in Y ⟼ C) (⟨x, y⟩)$
42		eqid	$⊢ (x \in X, y \in Y ⟼ C) = (x \in X, y \in Y ⟼ C)$
43	42	ovmpt4g	$⊢ (x \in X \land y \in Y \land C \in ⋃ M) \to x (x \in X, y \in Y ⟼ C) y = C$
44	8 9 35 43	syl3anc	$⊢ (φ \land (x \in X \land y \in Y)) \to x (x \in X, y \in Y ⟼ C) y = C$
45	41 44	syl5eqr	$⊢ (φ \land (x \in X \land y \in Y)) \to (x \in X, y \in Y ⟼ C) (⟨x, y⟩) = C$
46	37 40 45	3eqtr4d	$⊢ (φ \land (x \in X \land y \in Y)) \to ((z \in Z ⟼ B) \circ (x \in X, y \in Y ⟼ A)) (⟨x, y⟩) = (x \in X, y \in Y ⟼ C) (⟨x, y⟩)$
47	46	ralrimivva	$⊢ φ \to \forall x \in X \forall y \in Y ((z \in Z ⟼ B) \circ (x \in X, y \in Y ⟼ A)) (⟨x, y⟩) = (x \in X, y \in Y ⟼ C) (⟨x, y⟩)$
48		nfv	$⊢ Ⅎ u \forall y \in Y ((z \in Z ⟼ B) \circ (x \in X, y \in Y ⟼ A)) (⟨x, y⟩) = (x \in X, y \in Y ⟼ C) (⟨x, y⟩)$
49		nfcv	$⊢ \underline{Ⅎ} x Y$
50		nfcv	$⊢ \underline{Ⅎ} x (z \in Z ⟼ B)$
51		nfmpo1	$⊢ \underline{Ⅎ} x (x \in X, y \in Y ⟼ A)$
52	50 51	nfco	$⊢ \underline{Ⅎ} x ((z \in Z ⟼ B) \circ (x \in X, y \in Y ⟼ A))$
53		nfcv	$⊢ \underline{Ⅎ} x ⟨u, v⟩$
54	52 53	nffv	$⊢ \underline{Ⅎ} x ((z \in Z ⟼ B) \circ (x \in X, y \in Y ⟼ A)) (⟨u, v⟩)$
55		nfmpo1	$⊢ \underline{Ⅎ} x (x \in X, y \in Y ⟼ C)$
56	55 53	nffv	$⊢ \underline{Ⅎ} x (x \in X, y \in Y ⟼ C) (⟨u, v⟩)$
57	54 56	nfeq	$⊢ Ⅎ x ((z \in Z ⟼ B) \circ (x \in X, y \in Y ⟼ A)) (⟨u, v⟩) = (x \in X, y \in Y ⟼ C) (⟨u, v⟩)$
58	49 57	nfralw	$⊢ Ⅎ x \forall v \in Y ((z \in Z ⟼ B) \circ (x \in X, y \in Y ⟼ A)) (⟨u, v⟩) = (x \in X, y \in Y ⟼ C) (⟨u, v⟩)$
59		nfv	$⊢ Ⅎ v ((z \in Z ⟼ B) \circ (x \in X, y \in Y ⟼ A)) (⟨x, y⟩) = (x \in X, y \in Y ⟼ C) (⟨x, y⟩)$
60		nfcv	$⊢ \underline{Ⅎ} y (z \in Z ⟼ B)$
61		nfmpo2	$⊢ \underline{Ⅎ} y (x \in X, y \in Y ⟼ A)$
62	60 61	nfco	$⊢ \underline{Ⅎ} y ((z \in Z ⟼ B) \circ (x \in X, y \in Y ⟼ A))$
63		nfcv	$⊢ \underline{Ⅎ} y ⟨x, v⟩$
64	62 63	nffv	$⊢ \underline{Ⅎ} y ((z \in Z ⟼ B) \circ (x \in X, y \in Y ⟼ A)) (⟨x, v⟩)$
65		nfmpo2	$⊢ \underline{Ⅎ} y (x \in X, y \in Y ⟼ C)$
66	65 63	nffv	$⊢ \underline{Ⅎ} y (x \in X, y \in Y ⟼ C) (⟨x, v⟩)$
67	64 66	nfeq	$⊢ Ⅎ y ((z \in Z ⟼ B) \circ (x \in X, y \in Y ⟼ A)) (⟨x, v⟩) = (x \in X, y \in Y ⟼ C) (⟨x, v⟩)$
68		opeq2	$⊢ y = v \to ⟨x, y⟩ = ⟨x, v⟩$
69	68	fveq2d	$⊢ y = v \to ((z \in Z ⟼ B) \circ (x \in X, y \in Y ⟼ A)) (⟨x, y⟩) = ((z \in Z ⟼ B) \circ (x \in X, y \in Y ⟼ A)) (⟨x, v⟩)$
70	68	fveq2d	$⊢ y = v \to (x \in X, y \in Y ⟼ C) (⟨x, y⟩) = (x \in X, y \in Y ⟼ C) (⟨x, v⟩)$
71	69 70	eqeq12d	$⊢ y = v \to (((z \in Z ⟼ B) \circ (x \in X, y \in Y ⟼ A)) (⟨x, y⟩) = (x \in X, y \in Y ⟼ C) (⟨x, y⟩) \leftrightarrow ((z \in Z ⟼ B) \circ (x \in X, y \in Y ⟼ A)) (⟨x, v⟩) = (x \in X, y \in Y ⟼ C) (⟨x, v⟩))$
72	59 67 71	cbvralw	$⊢ \forall y \in Y ((z \in Z ⟼ B) \circ (x \in X, y \in Y ⟼ A)) (⟨x, y⟩) = (x \in X, y \in Y ⟼ C) (⟨x, y⟩) \leftrightarrow \forall v \in Y ((z \in Z ⟼ B) \circ (x \in X, y \in Y ⟼ A)) (⟨x, v⟩) = (x \in X, y \in Y ⟼ C) (⟨x, v⟩)$
73		opeq1	$⊢ x = u \to ⟨x, v⟩ = ⟨u, v⟩$
74	73	fveq2d	$⊢ x = u \to ((z \in Z ⟼ B) \circ (x \in X, y \in Y ⟼ A)) (⟨x, v⟩) = ((z \in Z ⟼ B) \circ (x \in X, y \in Y ⟼ A)) (⟨u, v⟩)$
75	73	fveq2d	$⊢ x = u \to (x \in X, y \in Y ⟼ C) (⟨x, v⟩) = (x \in X, y \in Y ⟼ C) (⟨u, v⟩)$
76	74 75	eqeq12d	$⊢ x = u \to (((z \in Z ⟼ B) \circ (x \in X, y \in Y ⟼ A)) (⟨x, v⟩) = (x \in X, y \in Y ⟼ C) (⟨x, v⟩) \leftrightarrow ((z \in Z ⟼ B) \circ (x \in X, y \in Y ⟼ A)) (⟨u, v⟩) = (x \in X, y \in Y ⟼ C) (⟨u, v⟩))$
77	76	ralbidv	$⊢ x = u \to (\forall v \in Y ((z \in Z ⟼ B) \circ (x \in X, y \in Y ⟼ A)) (⟨x, v⟩) = (x \in X, y \in Y ⟼ C) (⟨x, v⟩) \leftrightarrow \forall v \in Y ((z \in Z ⟼ B) \circ (x \in X, y \in Y ⟼ A)) (⟨u, v⟩) = (x \in X, y \in Y ⟼ C) (⟨u, v⟩))$
78	72 77	syl5bb	$⊢ x = u \to (\forall y \in Y ((z \in Z ⟼ B) \circ (x \in X, y \in Y ⟼ A)) (⟨x, y⟩) = (x \in X, y \in Y ⟼ C) (⟨x, y⟩) \leftrightarrow \forall v \in Y ((z \in Z ⟼ B) \circ (x \in X, y \in Y ⟼ A)) (⟨u, v⟩) = (x \in X, y \in Y ⟼ C) (⟨u, v⟩))$
79	48 58 78	cbvralw	$⊢ \forall x \in X \forall y \in Y ((z \in Z ⟼ B) \circ (x \in X, y \in Y ⟼ A)) (⟨x, y⟩) = (x \in X, y \in Y ⟼ C) (⟨x, y⟩) \leftrightarrow \forall u \in X \forall v \in Y ((z \in Z ⟼ B) \circ (x \in X, y \in Y ⟼ A)) (⟨u, v⟩) = (x \in X, y \in Y ⟼ C) (⟨u, v⟩)$
80	47 79	sylib	$⊢ φ \to \forall u \in X \forall v \in Y ((z \in Z ⟼ B) \circ (x \in X, y \in Y ⟼ A)) (⟨u, v⟩) = (x \in X, y \in Y ⟼ C) (⟨u, v⟩)$
81		fveq2	$⊢ w = ⟨u, v⟩ \to ((z \in Z ⟼ B) \circ (x \in X, y \in Y ⟼ A)) (w) = ((z \in Z ⟼ B) \circ (x \in X, y \in Y ⟼ A)) (⟨u, v⟩)$
82		fveq2	$⊢ w = ⟨u, v⟩ \to (x \in X, y \in Y ⟼ C) (w) = (x \in X, y \in Y ⟼ C) (⟨u, v⟩)$
83	81 82	eqeq12d	$⊢ w = ⟨u, v⟩ \to (((z \in Z ⟼ B) \circ (x \in X, y \in Y ⟼ A)) (w) = (x \in X, y \in Y ⟼ C) (w) \leftrightarrow ((z \in Z ⟼ B) \circ (x \in X, y \in Y ⟼ A)) (⟨u, v⟩) = (x \in X, y \in Y ⟼ C) (⟨u, v⟩))$
84	83	ralxp	$⊢ \forall w \in (X \times Y) ((z \in Z ⟼ B) \circ (x \in X, y \in Y ⟼ A)) (w) = (x \in X, y \in Y ⟼ C) (w) \leftrightarrow \forall u \in X \forall v \in Y ((z \in Z ⟼ B) \circ (x \in X, y \in Y ⟼ A)) (⟨u, v⟩) = (x \in X, y \in Y ⟼ C) (⟨u, v⟩)$
85	80 84	sylibr	$⊢ φ \to \forall w \in (X \times Y) ((z \in Z ⟼ B) \circ (x \in X, y \in Y ⟼ A)) (w) = (x \in X, y \in Y ⟼ C) (w)$
86		fco	$⊢ ((z \in Z ⟼ B) : Z ⟶ ⋃ M \land (x \in X, y \in Y ⟼ A) : X \times Y ⟶ Z) \to ((z \in Z ⟼ B) \circ (x \in X, y \in Y ⟼ A)) : X \times Y ⟶ ⋃ M$
87	31 13 86	syl2anc	$⊢ φ \to ((z \in Z ⟼ B) \circ (x \in X, y \in Y ⟼ A)) : X \times Y ⟶ ⋃ M$
88	87	ffnd	$⊢ φ \to ((z \in Z ⟼ B) \circ (x \in X, y \in Y ⟼ A)) Fn (X \times Y)$
89	35	ralrimivva	$⊢ φ \to \forall x \in X \forall y \in Y C \in ⋃ M$
90	42	fmpo	$⊢ \forall x \in X \forall y \in Y C \in ⋃ M \leftrightarrow (x \in X, y \in Y ⟼ C) : X \times Y ⟶ ⋃ M$
91	89 90	sylib	$⊢ φ \to (x \in X, y \in Y ⟼ C) : X \times Y ⟶ ⋃ M$
92	91	ffnd	$⊢ φ \to (x \in X, y \in Y ⟼ C) Fn (X \times Y)$
93		eqfnfv	$⊢ (((z \in Z ⟼ B) \circ (x \in X, y \in Y ⟼ A)) Fn (X \times Y) \land (x \in X, y \in Y ⟼ C) Fn (X \times Y)) \to ((z \in Z ⟼ B) \circ (x \in X, y \in Y ⟼ A) = (x \in X, y \in Y ⟼ C) \leftrightarrow \forall w \in (X \times Y) ((z \in Z ⟼ B) \circ (x \in X, y \in Y ⟼ A)) (w) = (x \in X, y \in Y ⟼ C) (w))$
94	88 92 93	syl2anc	$⊢ φ \to ((z \in Z ⟼ B) \circ (x \in X, y \in Y ⟼ A) = (x \in X, y \in Y ⟼ C) \leftrightarrow \forall w \in (X \times Y) ((z \in Z ⟼ B) \circ (x \in X, y \in Y ⟼ A)) (w) = (x \in X, y \in Y ⟼ C) (w))$
95	85 94	mpbird	$⊢ φ \to (z \in Z ⟼ B) \circ (x \in X, y \in Y ⟼ A) = (x \in X, y \in Y ⟼ C)$
96		cnco	$⊢ ((x \in X, y \in Y ⟼ A) \in ((J \times_{t} K) Cn L) \land (z \in Z ⟼ B) \in (L Cn M)) \to (z \in Z ⟼ B) \circ (x \in X, y \in Y ⟼ A) \in ((J \times_{t} K) Cn M)$
97	3 5 96	syl2anc	$⊢ φ \to (z \in Z ⟼ B) \circ (x \in X, y \in Y ⟼ A) \in ((J \times_{t} K) Cn M)$
98	95 97	eqeltrrd	$⊢ φ \to (x \in X, y \in Y ⟼ C) \in ((J \times_{t} K) Cn M)$

Metamath Proof Explorer

Theorem cnmpt21

Proof