cnmpt22

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)$
	cnmpt2t.b	$⊢ φ \to (x \in X, y \in Y ⟼ B) \in ((J \times_{t} K) Cn M)$
	cnmpt22.l	$⊢ φ \to L \in TopOn (Z)$
	cnmpt22.m	$⊢ φ \to M \in TopOn (W)$
	cnmpt22.c	$⊢ φ \to (z \in Z, w \in W ⟼ C) \in ((L \times_{t} M) Cn N)$
	cnmpt22.d	$⊢ (z = A \land w = B) \to C = D$
Assertion	cnmpt22	$⊢ φ \to (x \in X, y \in Y ⟼ D) \in ((J \times_{t} K) Cn N)$

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		cnmpt2t.b	$⊢ φ \to (x \in X, y \in Y ⟼ B) \in ((J \times_{t} K) Cn M)$
5		cnmpt22.l	$⊢ φ \to L \in TopOn (Z)$
6		cnmpt22.m	$⊢ φ \to M \in TopOn (W)$
7		cnmpt22.c	$⊢ φ \to (z \in Z, w \in W ⟼ C) \in ((L \times_{t} M) Cn N)$
8		cnmpt22.d	$⊢ (z = A \land w = B) \to C = D$
9		df-ov	$⊢ A (z \in Z, w \in W ⟼ C) B = (z \in Z, w \in W ⟼ C) (⟨A, B⟩)$
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 5 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	3impib	$⊢ (φ \land x \in X \land y \in Y) \to A \in Z$
20		cnf2	$⊢ (J \times_{t} K \in TopOn (X \times Y) \land M \in TopOn (W) \land (x \in X, y \in Y ⟼ B) \in ((J \times_{t} K) Cn M)) \to (x \in X, y \in Y ⟼ B) : X \times Y ⟶ W$
21	11 6 4 20	syl3anc	$⊢ φ \to (x \in X, y \in Y ⟼ B) : X \times Y ⟶ W$
22		eqid	$⊢ (x \in X, y \in Y ⟼ B) = (x \in X, y \in Y ⟼ B)$
23	22	fmpo	$⊢ \forall x \in X \forall y \in Y B \in W \leftrightarrow (x \in X, y \in Y ⟼ B) : X \times Y ⟶ W$
24	21 23	sylibr	$⊢ φ \to \forall x \in X \forall y \in Y B \in W$
25		rsp2	$⊢ \forall x \in X \forall y \in Y B \in W \to ((x \in X \land y \in Y) \to B \in W)$
26	24 25	syl	$⊢ φ \to ((x \in X \land y \in Y) \to B \in W)$
27	26	3impib	$⊢ (φ \land x \in X \land y \in Y) \to B \in W$
28	19 27	jca	$⊢ (φ \land x \in X \land y \in Y) \to (A \in Z \land B \in W)$
29		txtopon	$⊢ (L \in TopOn (Z) \land M \in TopOn (W)) \to L \times_{t} M \in TopOn (Z \times W)$
30	5 6 29	syl2anc	$⊢ φ \to L \times_{t} M \in TopOn (Z \times W)$
31		cntop2	$⊢ (z \in Z, w \in W ⟼ C) \in ((L \times_{t} M) Cn N) \to N \in Top$
32	7 31	syl	$⊢ φ \to N \in Top$
33		toptopon2	$⊢ N \in Top \leftrightarrow N \in TopOn (⋃ N)$
34	32 33	sylib	$⊢ φ \to N \in TopOn (⋃ N)$
35		cnf2	$⊢ (L \times_{t} M \in TopOn (Z \times W) \land N \in TopOn (⋃ N) \land (z \in Z, w \in W ⟼ C) \in ((L \times_{t} M) Cn N)) \to (z \in Z, w \in W ⟼ C) : Z \times W ⟶ ⋃ N$
36	30 34 7 35	syl3anc	$⊢ φ \to (z \in Z, w \in W ⟼ C) : Z \times W ⟶ ⋃ N$
37		eqid	$⊢ (z \in Z, w \in W ⟼ C) = (z \in Z, w \in W ⟼ C)$
38	37	fmpo	$⊢ \forall z \in Z \forall w \in W C \in ⋃ N \leftrightarrow (z \in Z, w \in W ⟼ C) : Z \times W ⟶ ⋃ N$
39	36 38	sylibr	$⊢ φ \to \forall z \in Z \forall w \in W C \in ⋃ N$
40		r2al	$⊢ \forall z \in Z \forall w \in W C \in ⋃ N \leftrightarrow \forall z \forall w ((z \in Z \land w \in W) \to C \in ⋃ N)$
41	39 40	sylib	$⊢ φ \to \forall z \forall w ((z \in Z \land w \in W) \to C \in ⋃ N)$
42	41	3ad2ant1	$⊢ (φ \land x \in X \land y \in Y) \to \forall z \forall w ((z \in Z \land w \in W) \to C \in ⋃ N)$
43		eleq1	$⊢ z = A \to (z \in Z \leftrightarrow A \in Z)$
44		eleq1	$⊢ w = B \to (w \in W \leftrightarrow B \in W)$
45	43 44	bi2anan9	$⊢ (z = A \land w = B) \to ((z \in Z \land w \in W) \leftrightarrow (A \in Z \land B \in W))$
46	8	eleq1d	$⊢ (z = A \land w = B) \to (C \in ⋃ N \leftrightarrow D \in ⋃ N)$
47	45 46	imbi12d	$⊢ (z = A \land w = B) \to (((z \in Z \land w \in W) \to C \in ⋃ N) \leftrightarrow ((A \in Z \land B \in W) \to D \in ⋃ N))$
48	47	spc2gv	$⊢ (A \in Z \land B \in W) \to (\forall z \forall w ((z \in Z \land w \in W) \to C \in ⋃ N) \to ((A \in Z \land B \in W) \to D \in ⋃ N))$
49	28 42 28 48	syl3c	$⊢ (φ \land x \in X \land y \in Y) \to D \in ⋃ N$
50	8 37	ovmpoga	$⊢ (A \in Z \land B \in W \land D \in ⋃ N) \to A (z \in Z, w \in W ⟼ C) B = D$
51	19 27 49 50	syl3anc	$⊢ (φ \land x \in X \land y \in Y) \to A (z \in Z, w \in W ⟼ C) B = D$
52	9 51	eqtr3id	$⊢ (φ \land x \in X \land y \in Y) \to (z \in Z, w \in W ⟼ C) (⟨A, B⟩) = D$
53	52	mpoeq3dva	$⊢ φ \to (x \in X, y \in Y ⟼ (z \in Z, w \in W ⟼ C) (⟨A, B⟩)) = (x \in X, y \in Y ⟼ D)$
54	1 2 3 4	cnmpt2t	$⊢ φ \to (x \in X, y \in Y ⟼ ⟨A, B⟩) \in ((J \times_{t} K) Cn (L \times_{t} M))$
55	1 2 54 7	cnmpt21f	$⊢ φ \to (x \in X, y \in Y ⟼ (z \in Z, w \in W ⟼ C) (⟨A, B⟩)) \in ((J \times_{t} K) Cn N)$
56	53 55	eqeltrrd	$⊢ φ \to (x \in X, y \in Y ⟼ D) \in ((J \times_{t} K) Cn N)$

Metamath Proof Explorer

Theorem cnmpt22

Proof