cnmpt11

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	cnmptid.j	$⊢ φ \to J \in TopOn (X)$
	cnmpt11.a	$⊢ φ \to (x \in X ⟼ A) \in (J Cn K)$
	cnmpt11.k	$⊢ φ \to K \in TopOn (Y)$
	cnmpt11.b	$⊢ φ \to (y \in Y ⟼ B) \in (K Cn L)$
	cnmpt11.c	$⊢ y = A \to B = C$
Assertion	cnmpt11	$⊢ φ \to (x \in X ⟼ C) \in (J Cn L)$

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		cnmpt11.k	$⊢ φ \to K \in TopOn (Y)$
4		cnmpt11.b	$⊢ φ \to (y \in Y ⟼ B) \in (K Cn L)$
5		cnmpt11.c	$⊢ y = A \to B = C$
6		simpr	$⊢ (φ \land x \in X) \to x \in X$
7		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$
8	1 3 2 7	syl3anc	$⊢ φ \to (x \in X ⟼ A) : X ⟶ Y$
9	8	fvmptelcdm	$⊢ (φ \land x \in X) \to A \in Y$
10		eqid	$⊢ (x \in X ⟼ A) = (x \in X ⟼ A)$
11	10	fvmpt2	$⊢ (x \in X \land A \in Y) \to (x \in X ⟼ A) (x) = A$
12	6 9 11	syl2anc	$⊢ (φ \land x \in X) \to (x \in X ⟼ A) (x) = A$
13	12	fveq2d	$⊢ (φ \land x \in X) \to (y \in Y ⟼ B) ((x \in X ⟼ A) (x)) = (y \in Y ⟼ B) (A)$
14		eqid	$⊢ (y \in Y ⟼ B) = (y \in Y ⟼ B)$
15	5	eleq1d	$⊢ y = A \to (B \in ⋃ L \leftrightarrow C \in ⋃ L)$
16		cntop2	$⊢ (y \in Y ⟼ B) \in (K Cn L) \to L \in Top$
17	4 16	syl	$⊢ φ \to L \in Top$
18		toptopon2	$⊢ L \in Top \leftrightarrow L \in TopOn (⋃ L)$
19	17 18	sylib	$⊢ φ \to L \in TopOn (⋃ L)$
20		cnf2	$⊢ (K \in TopOn (Y) \land L \in TopOn (⋃ L) \land (y \in Y ⟼ B) \in (K Cn L)) \to (y \in Y ⟼ B) : Y ⟶ ⋃ L$
21	3 19 4 20	syl3anc	$⊢ φ \to (y \in Y ⟼ B) : Y ⟶ ⋃ L$
22	14	fmpt	$⊢ \forall y \in Y B \in ⋃ L \leftrightarrow (y \in Y ⟼ B) : Y ⟶ ⋃ L$
23	21 22	sylibr	$⊢ φ \to \forall y \in Y B \in ⋃ L$
24	23	adantr	$⊢ (φ \land x \in X) \to \forall y \in Y B \in ⋃ L$
25	15 24 9	rspcdva	$⊢ (φ \land x \in X) \to C \in ⋃ L$
26	14 5 9 25	fvmptd3	$⊢ (φ \land x \in X) \to (y \in Y ⟼ B) (A) = C$
27	13 26	eqtrd	$⊢ (φ \land x \in X) \to (y \in Y ⟼ B) ((x \in X ⟼ A) (x)) = C$
28		fvco3	$⊢ ((x \in X ⟼ A) : X ⟶ Y \land x \in X) \to ((y \in Y ⟼ B) \circ (x \in X ⟼ A)) (x) = (y \in Y ⟼ B) ((x \in X ⟼ A) (x))$
29	8 28	sylan	$⊢ (φ \land x \in X) \to ((y \in Y ⟼ B) \circ (x \in X ⟼ A)) (x) = (y \in Y ⟼ B) ((x \in X ⟼ A) (x))$
30		eqid	$⊢ (x \in X ⟼ C) = (x \in X ⟼ C)$
31	30	fvmpt2	$⊢ (x \in X \land C \in ⋃ L) \to (x \in X ⟼ C) (x) = C$
32	6 25 31	syl2anc	$⊢ (φ \land x \in X) \to (x \in X ⟼ C) (x) = C$
33	27 29 32	3eqtr4d	$⊢ (φ \land x \in X) \to ((y \in Y ⟼ B) \circ (x \in X ⟼ A)) (x) = (x \in X ⟼ C) (x)$
34	33	ralrimiva	$⊢ φ \to \forall x \in X ((y \in Y ⟼ B) \circ (x \in X ⟼ A)) (x) = (x \in X ⟼ C) (x)$
35		nfv	$⊢ Ⅎ z ((y \in Y ⟼ B) \circ (x \in X ⟼ A)) (x) = (x \in X ⟼ C) (x)$
36		nfcv	$⊢ \underline{Ⅎ} x (y \in Y ⟼ B)$
37		nfmpt1	$⊢ \underline{Ⅎ} x (x \in X ⟼ A)$
38	36 37	nfco	$⊢ \underline{Ⅎ} x ((y \in Y ⟼ B) \circ (x \in X ⟼ A))$
39		nfcv	$⊢ \underline{Ⅎ} x z$
40	38 39	nffv	$⊢ \underline{Ⅎ} x ((y \in Y ⟼ B) \circ (x \in X ⟼ A)) (z)$
41		nfmpt1	$⊢ \underline{Ⅎ} x (x \in X ⟼ C)$
42	41 39	nffv	$⊢ \underline{Ⅎ} x (x \in X ⟼ C) (z)$
43	40 42	nfeq	$⊢ Ⅎ x ((y \in Y ⟼ B) \circ (x \in X ⟼ A)) (z) = (x \in X ⟼ C) (z)$
44		fveq2	$⊢ x = z \to ((y \in Y ⟼ B) \circ (x \in X ⟼ A)) (x) = ((y \in Y ⟼ B) \circ (x \in X ⟼ A)) (z)$
45		fveq2	$⊢ x = z \to (x \in X ⟼ C) (x) = (x \in X ⟼ C) (z)$
46	44 45	eqeq12d	$⊢ x = z \to (((y \in Y ⟼ B) \circ (x \in X ⟼ A)) (x) = (x \in X ⟼ C) (x) \leftrightarrow ((y \in Y ⟼ B) \circ (x \in X ⟼ A)) (z) = (x \in X ⟼ C) (z))$
47	35 43 46	cbvralw	$⊢ \forall x \in X ((y \in Y ⟼ B) \circ (x \in X ⟼ A)) (x) = (x \in X ⟼ C) (x) \leftrightarrow \forall z \in X ((y \in Y ⟼ B) \circ (x \in X ⟼ A)) (z) = (x \in X ⟼ C) (z)$
48	34 47	sylib	$⊢ φ \to \forall z \in X ((y \in Y ⟼ B) \circ (x \in X ⟼ A)) (z) = (x \in X ⟼ C) (z)$
49		fco	$⊢ ((y \in Y ⟼ B) : Y ⟶ ⋃ L \land (x \in X ⟼ A) : X ⟶ Y) \to ((y \in Y ⟼ B) \circ (x \in X ⟼ A)) : X ⟶ ⋃ L$
50	21 8 49	syl2anc	$⊢ φ \to ((y \in Y ⟼ B) \circ (x \in X ⟼ A)) : X ⟶ ⋃ L$
51	50	ffnd	$⊢ φ \to ((y \in Y ⟼ B) \circ (x \in X ⟼ A)) Fn X$
52	25	fmpttd	$⊢ φ \to (x \in X ⟼ C) : X ⟶ ⋃ L$
53	52	ffnd	$⊢ φ \to (x \in X ⟼ C) Fn X$
54		eqfnfv	$⊢ (((y \in Y ⟼ B) \circ (x \in X ⟼ A)) Fn X \land (x \in X ⟼ C) Fn X) \to ((y \in Y ⟼ B) \circ (x \in X ⟼ A) = (x \in X ⟼ C) \leftrightarrow \forall z \in X ((y \in Y ⟼ B) \circ (x \in X ⟼ A)) (z) = (x \in X ⟼ C) (z))$
55	51 53 54	syl2anc	$⊢ φ \to ((y \in Y ⟼ B) \circ (x \in X ⟼ A) = (x \in X ⟼ C) \leftrightarrow \forall z \in X ((y \in Y ⟼ B) \circ (x \in X ⟼ A)) (z) = (x \in X ⟼ C) (z))$
56	48 55	mpbird	$⊢ φ \to (y \in Y ⟼ B) \circ (x \in X ⟼ A) = (x \in X ⟼ C)$
57		cnco	$⊢ ((x \in X ⟼ A) \in (J Cn K) \land (y \in Y ⟼ B) \in (K Cn L)) \to (y \in Y ⟼ B) \circ (x \in X ⟼ A) \in (J Cn L)$
58	2 4 57	syl2anc	$⊢ φ \to (y \in Y ⟼ B) \circ (x \in X ⟼ A) \in (J Cn L)$
59	56 58	eqeltrrd	$⊢ φ \to (x \in X ⟼ C) \in (J Cn L)$

Metamath Proof Explorer

Theorem cnmpt11

Proof