cnmpt1t

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)$
	cnmpt1t.b	$⊢ φ \to (x \in X ⟼ B) \in (J Cn L)$
Assertion	cnmpt1t	$⊢ φ \to (x \in X ⟼ ⟨A, B⟩) \in (J Cn (K \times_{t} 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		cnmpt1t.b	$⊢ φ \to (x \in X ⟼ B) \in (J Cn L)$
4		toponuni	$⊢ J \in TopOn (X) \to X = ⋃ J$
5		mpteq1	$⊢ X = ⋃ J \to (x \in X ⟼ ⟨(x \in X ⟼ A) (x), (x \in X ⟼ B) (x)⟩) = (x \in ⋃ J ⟼ ⟨(x \in X ⟼ A) (x), (x \in X ⟼ B) (x)⟩)$
6	1 4 5	3syl	$⊢ φ \to (x \in X ⟼ ⟨(x \in X ⟼ A) (x), (x \in X ⟼ B) (x)⟩) = (x \in ⋃ J ⟼ ⟨(x \in X ⟼ A) (x), (x \in X ⟼ B) (x)⟩)$
7		simpr	$⊢ (φ \land x \in X) \to x \in X$
8		cntop2	$⊢ (x \in X ⟼ A) \in (J Cn K) \to K \in Top$
9	2 8	syl	$⊢ φ \to K \in Top$
10		toptopon2	$⊢ K \in Top \leftrightarrow K \in TopOn (⋃ K)$
11	9 10	sylib	$⊢ φ \to K \in TopOn (⋃ K)$
12		cnf2	$⊢ (J \in TopOn (X) \land K \in TopOn (⋃ K) \land (x \in X ⟼ A) \in (J Cn K)) \to (x \in X ⟼ A) : X ⟶ ⋃ K$
13	1 11 2 12	syl3anc	$⊢ φ \to (x \in X ⟼ A) : X ⟶ ⋃ K$
14	13	fvmptelrn	$⊢ (φ \land x \in X) \to A \in ⋃ K$
15		eqid	$⊢ (x \in X ⟼ A) = (x \in X ⟼ A)$
16	15	fvmpt2	$⊢ (x \in X \land A \in ⋃ K) \to (x \in X ⟼ A) (x) = A$
17	7 14 16	syl2anc	$⊢ (φ \land x \in X) \to (x \in X ⟼ A) (x) = A$
18		cntop2	$⊢ (x \in X ⟼ B) \in (J Cn L) \to L \in Top$
19	3 18	syl	$⊢ φ \to L \in Top$
20		toptopon2	$⊢ L \in Top \leftrightarrow L \in TopOn (⋃ L)$
21	19 20	sylib	$⊢ φ \to L \in TopOn (⋃ L)$
22		cnf2	$⊢ (J \in TopOn (X) \land L \in TopOn (⋃ L) \land (x \in X ⟼ B) \in (J Cn L)) \to (x \in X ⟼ B) : X ⟶ ⋃ L$
23	1 21 3 22	syl3anc	$⊢ φ \to (x \in X ⟼ B) : X ⟶ ⋃ L$
24	23	fvmptelrn	$⊢ (φ \land x \in X) \to B \in ⋃ L$
25		eqid	$⊢ (x \in X ⟼ B) = (x \in X ⟼ B)$
26	25	fvmpt2	$⊢ (x \in X \land B \in ⋃ L) \to (x \in X ⟼ B) (x) = B$
27	7 24 26	syl2anc	$⊢ (φ \land x \in X) \to (x \in X ⟼ B) (x) = B$
28	17 27	opeq12d	$⊢ (φ \land x \in X) \to ⟨(x \in X ⟼ A) (x), (x \in X ⟼ B) (x)⟩ = ⟨A, B⟩$
29	28	mpteq2dva	$⊢ φ \to (x \in X ⟼ ⟨(x \in X ⟼ A) (x), (x \in X ⟼ B) (x)⟩) = (x \in X ⟼ ⟨A, B⟩)$
30	6 29	eqtr3d	$⊢ φ \to (x \in ⋃ J ⟼ ⟨(x \in X ⟼ A) (x), (x \in X ⟼ B) (x)⟩) = (x \in X ⟼ ⟨A, B⟩)$
31		eqid	$⊢ ⋃ J = ⋃ J$
32		nfcv	$⊢ \underline{Ⅎ} y ⟨(x \in X ⟼ A) (x), (x \in X ⟼ B) (x)⟩$
33		nffvmpt1	$⊢ \underline{Ⅎ} x (x \in X ⟼ A) (y)$
34		nffvmpt1	$⊢ \underline{Ⅎ} x (x \in X ⟼ B) (y)$
35	33 34	nfop	$⊢ \underline{Ⅎ} x ⟨(x \in X ⟼ A) (y), (x \in X ⟼ B) (y)⟩$
36		fveq2	$⊢ x = y \to (x \in X ⟼ A) (x) = (x \in X ⟼ A) (y)$
37		fveq2	$⊢ x = y \to (x \in X ⟼ B) (x) = (x \in X ⟼ B) (y)$
38	36 37	opeq12d	$⊢ x = y \to ⟨(x \in X ⟼ A) (x), (x \in X ⟼ B) (x)⟩ = ⟨(x \in X ⟼ A) (y), (x \in X ⟼ B) (y)⟩$
39	32 35 38	cbvmpt	$⊢ (x \in ⋃ J ⟼ ⟨(x \in X ⟼ A) (x), (x \in X ⟼ B) (x)⟩) = (y \in ⋃ J ⟼ ⟨(x \in X ⟼ A) (y), (x \in X ⟼ B) (y)⟩)$
40	31 39	txcnmpt	$⊢ ((x \in X ⟼ A) \in (J Cn K) \land (x \in X ⟼ B) \in (J Cn L)) \to (x \in ⋃ J ⟼ ⟨(x \in X ⟼ A) (x), (x \in X ⟼ B) (x)⟩) \in (J Cn (K \times_{t} L))$
41	2 3 40	syl2anc	$⊢ φ \to (x \in ⋃ J ⟼ ⟨(x \in X ⟼ A) (x), (x \in X ⟼ B) (x)⟩) \in (J Cn (K \times_{t} L))$
42	30 41	eqeltrrd	$⊢ φ \to (x \in X ⟼ ⟨A, B⟩) \in (J Cn (K \times_{t} L))$

Metamath Proof Explorer

Theorem cnmpt1t

Proof