cnmpt12

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

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

Proof

Step	Hyp	Ref	Expression
1		cnmptid.j	$⊢ φ \to J \in TopOn (X)$
2		cnmpt11.a	$⊢ φ \to (x \in X ⟼ A) \in (J Cn K)$
3		cnmpt1t.b	$⊢ φ \to (x \in X ⟼ B) \in (J Cn L)$
4		cnmpt12.k	$⊢ φ \to K \in TopOn (Y)$
5		cnmpt12.l	$⊢ φ \to L \in TopOn (Z)$
6		cnmpt12.c	$⊢ φ \to (y \in Y, z \in Z ⟼ C) \in ((K \times_{t} L) Cn M)$
7		cnmpt12.d	$⊢ (y = A \land z = B) \to C = D$
8		cnf2	$⊢ (J \in TopOn (X) \land K \in TopOn (Y) \land (x \in X ⟼ A) \in (J Cn K)) \to (x \in X ⟼ A) : X ⟶ Y$
9	1 4 2 8	syl3anc	$⊢ φ \to (x \in X ⟼ A) : X ⟶ Y$
10	9	fvmptelrn	$⊢ (φ \land x \in X) \to A \in Y$
11		cnf2	$⊢ (J \in TopOn (X) \land L \in TopOn (Z) \land (x \in X ⟼ B) \in (J Cn L)) \to (x \in X ⟼ B) : X ⟶ Z$
12	1 5 3 11	syl3anc	$⊢ φ \to (x \in X ⟼ B) : X ⟶ Z$
13	12	fvmptelrn	$⊢ (φ \land x \in X) \to B \in Z$
14	10 13	jca	$⊢ (φ \land x \in X) \to (A \in Y \land B \in Z)$
15		txtopon	$⊢ (K \in TopOn (Y) \land L \in TopOn (Z)) \to K \times_{t} L \in TopOn (Y \times Z)$
16	4 5 15	syl2anc	$⊢ φ \to K \times_{t} L \in TopOn (Y \times Z)$
17		cntop2	$⊢ (y \in Y, z \in Z ⟼ C) \in ((K \times_{t} L) Cn M) \to M \in Top$
18	6 17	syl	$⊢ φ \to M \in Top$
19		toptopon2	$⊢ M \in Top \leftrightarrow M \in TopOn (⋃ M)$
20	18 19	sylib	$⊢ φ \to M \in TopOn (⋃ M)$
21		cnf2	$⊢ (K \times_{t} L \in TopOn (Y \times Z) \land M \in TopOn (⋃ M) \land (y \in Y, z \in Z ⟼ C) \in ((K \times_{t} L) Cn M)) \to (y \in Y, z \in Z ⟼ C) : Y \times Z ⟶ ⋃ M$
22	16 20 6 21	syl3anc	$⊢ φ \to (y \in Y, z \in Z ⟼ C) : Y \times Z ⟶ ⋃ M$
23		eqid	$⊢ (y \in Y, z \in Z ⟼ C) = (y \in Y, z \in Z ⟼ C)$
24	23	fmpo	$⊢ \forall y \in Y \forall z \in Z C \in ⋃ M \leftrightarrow (y \in Y, z \in Z ⟼ C) : Y \times Z ⟶ ⋃ M$
25	22 24	sylibr	$⊢ φ \to \forall y \in Y \forall z \in Z C \in ⋃ M$
26		r2al	$⊢ \forall y \in Y \forall z \in Z C \in ⋃ M \leftrightarrow \forall y \forall z ((y \in Y \land z \in Z) \to C \in ⋃ M)$
27	25 26	sylib	$⊢ φ \to \forall y \forall z ((y \in Y \land z \in Z) \to C \in ⋃ M)$
28	27	adantr	$⊢ (φ \land x \in X) \to \forall y \forall z ((y \in Y \land z \in Z) \to C \in ⋃ M)$
29		eleq1	$⊢ y = A \to (y \in Y \leftrightarrow A \in Y)$
30		eleq1	$⊢ z = B \to (z \in Z \leftrightarrow B \in Z)$
31	29 30	bi2anan9	$⊢ (y = A \land z = B) \to ((y \in Y \land z \in Z) \leftrightarrow (A \in Y \land B \in Z))$
32	7	eleq1d	$⊢ (y = A \land z = B) \to (C \in ⋃ M \leftrightarrow D \in ⋃ M)$
33	31 32	imbi12d	$⊢ (y = A \land z = B) \to (((y \in Y \land z \in Z) \to C \in ⋃ M) \leftrightarrow ((A \in Y \land B \in Z) \to D \in ⋃ M))$
34	33	spc2gv	$⊢ (A \in Y \land B \in Z) \to (\forall y \forall z ((y \in Y \land z \in Z) \to C \in ⋃ M) \to ((A \in Y \land B \in Z) \to D \in ⋃ M))$
35	14 28 14 34	syl3c	$⊢ (φ \land x \in X) \to D \in ⋃ M$
36	7 23	ovmpoga	$⊢ (A \in Y \land B \in Z \land D \in ⋃ M) \to A (y \in Y, z \in Z ⟼ C) B = D$
37	10 13 35 36	syl3anc	$⊢ (φ \land x \in X) \to A (y \in Y, z \in Z ⟼ C) B = D$
38	37	mpteq2dva	$⊢ φ \to (x \in X ⟼ A (y \in Y, z \in Z ⟼ C) B) = (x \in X ⟼ D)$
39	1 2 3 6	cnmpt12f	$⊢ φ \to (x \in X ⟼ A (y \in Y, z \in Z ⟼ C) B) \in (J Cn M)$
40	38 39	eqeltrrd	$⊢ φ \to (x \in X ⟼ D) \in (J Cn M)$

Metamath Proof Explorer

Theorem cnmpt12

Proof