cnmpt2t

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)$
Assertion	cnmpt2t	$⊢ φ \to (x \in X, y \in Y ⟼ ⟨A, B⟩) \in ((J \times_{t} K) Cn (L \times_{t} 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		cnmpt2t.b	$⊢ φ \to (x \in X, y \in Y ⟼ B) \in ((J \times_{t} K) Cn M)$
5		fveq2	$⊢ z = ⟨u, v⟩ \to (x \in X, y \in Y ⟼ A) (z) = (x \in X, y \in Y ⟼ A) (⟨u, v⟩)$
6		df-ov	$⊢ u (x \in X, y \in Y ⟼ A) v = (x \in X, y \in Y ⟼ A) (⟨u, v⟩)$
7	5 6	eqtr4di	$⊢ z = ⟨u, v⟩ \to (x \in X, y \in Y ⟼ A) (z) = u (x \in X, y \in Y ⟼ A) v$
8		fveq2	$⊢ z = ⟨u, v⟩ \to (x \in X, y \in Y ⟼ B) (z) = (x \in X, y \in Y ⟼ B) (⟨u, v⟩)$
9		df-ov	$⊢ u (x \in X, y \in Y ⟼ B) v = (x \in X, y \in Y ⟼ B) (⟨u, v⟩)$
10	8 9	eqtr4di	$⊢ z = ⟨u, v⟩ \to (x \in X, y \in Y ⟼ B) (z) = u (x \in X, y \in Y ⟼ B) v$
11	7 10	opeq12d	$⊢ z = ⟨u, v⟩ \to ⟨(x \in X, y \in Y ⟼ A) (z), (x \in X, y \in Y ⟼ B) (z)⟩ = ⟨u (x \in X, y \in Y ⟼ A) v, u (x \in X, y \in Y ⟼ B) v⟩$
12	11	mpompt	$⊢ (z \in (X \times Y) ⟼ ⟨(x \in X, y \in Y ⟼ A) (z), (x \in X, y \in Y ⟼ B) (z)⟩) = (u \in X, v \in Y ⟼ ⟨u (x \in X, y \in Y ⟼ A) v, u (x \in X, y \in Y ⟼ B) v⟩)$
13		nfcv	$⊢ \underline{Ⅎ} x u$
14		nfmpo1	$⊢ \underline{Ⅎ} x (x \in X, y \in Y ⟼ A)$
15		nfcv	$⊢ \underline{Ⅎ} x v$
16	13 14 15	nfov	$⊢ \underline{Ⅎ} x (u (x \in X, y \in Y ⟼ A) v)$
17		nfmpo1	$⊢ \underline{Ⅎ} x (x \in X, y \in Y ⟼ B)$
18	13 17 15	nfov	$⊢ \underline{Ⅎ} x (u (x \in X, y \in Y ⟼ B) v)$
19	16 18	nfop	$⊢ \underline{Ⅎ} x ⟨u (x \in X, y \in Y ⟼ A) v, u (x \in X, y \in Y ⟼ B) v⟩$
20		nfcv	$⊢ \underline{Ⅎ} y u$
21		nfmpo2	$⊢ \underline{Ⅎ} y (x \in X, y \in Y ⟼ A)$
22		nfcv	$⊢ \underline{Ⅎ} y v$
23	20 21 22	nfov	$⊢ \underline{Ⅎ} y (u (x \in X, y \in Y ⟼ A) v)$
24		nfmpo2	$⊢ \underline{Ⅎ} y (x \in X, y \in Y ⟼ B)$
25	20 24 22	nfov	$⊢ \underline{Ⅎ} y (u (x \in X, y \in Y ⟼ B) v)$
26	23 25	nfop	$⊢ \underline{Ⅎ} y ⟨u (x \in X, y \in Y ⟼ A) v, u (x \in X, y \in Y ⟼ B) v⟩$
27		nfcv	$⊢ \underline{Ⅎ} u ⟨x (x \in X, y \in Y ⟼ A) y, x (x \in X, y \in Y ⟼ B) y⟩$
28		nfcv	$⊢ \underline{Ⅎ} v ⟨x (x \in X, y \in Y ⟼ A) y, x (x \in X, y \in Y ⟼ B) y⟩$
29		oveq12	$⊢ (u = x \land v = y) \to u (x \in X, y \in Y ⟼ A) v = x (x \in X, y \in Y ⟼ A) y$
30		oveq12	$⊢ (u = x \land v = y) \to u (x \in X, y \in Y ⟼ B) v = x (x \in X, y \in Y ⟼ B) y$
31	29 30	opeq12d	$⊢ (u = x \land v = y) \to ⟨u (x \in X, y \in Y ⟼ A) v, u (x \in X, y \in Y ⟼ B) v⟩ = ⟨x (x \in X, y \in Y ⟼ A) y, x (x \in X, y \in Y ⟼ B) y⟩$
32	19 26 27 28 31	cbvmpo	$⊢ (u \in X, v \in Y ⟼ ⟨u (x \in X, y \in Y ⟼ A) v, u (x \in X, y \in Y ⟼ B) v⟩) = (x \in X, y \in Y ⟼ ⟨x (x \in X, y \in Y ⟼ A) y, x (x \in X, y \in Y ⟼ B) y⟩)$
33	12 32	eqtri	$⊢ (z \in (X \times Y) ⟼ ⟨(x \in X, y \in Y ⟼ A) (z), (x \in X, y \in Y ⟼ B) (z)⟩) = (x \in X, y \in Y ⟼ ⟨x (x \in X, y \in Y ⟼ A) y, x (x \in X, y \in Y ⟼ B) y⟩)$
34		txtopon	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to J \times_{t} K \in TopOn (X \times Y)$
35	1 2 34	syl2anc	$⊢ φ \to J \times_{t} K \in TopOn (X \times Y)$
36		toponuni	$⊢ J \times_{t} K \in TopOn (X \times Y) \to X \times Y = ⋃ (J \times_{t} K)$
37		mpteq1	$⊢ X \times Y = ⋃ (J \times_{t} K) \to (z \in (X \times Y) ⟼ ⟨(x \in X, y \in Y ⟼ A) (z), (x \in X, y \in Y ⟼ B) (z)⟩) = (z \in ⋃ (J \times_{t} K) ⟼ ⟨(x \in X, y \in Y ⟼ A) (z), (x \in X, y \in Y ⟼ B) (z)⟩)$
38	35 36 37	3syl	$⊢ φ \to (z \in (X \times Y) ⟼ ⟨(x \in X, y \in Y ⟼ A) (z), (x \in X, y \in Y ⟼ B) (z)⟩) = (z \in ⋃ (J \times_{t} K) ⟼ ⟨(x \in X, y \in Y ⟼ A) (z), (x \in X, y \in Y ⟼ B) (z)⟩)$
39		simp2	$⊢ (φ \land x \in X \land y \in Y) \to x \in X$
40		simp3	$⊢ (φ \land x \in X \land y \in Y) \to y \in Y$
41		cntop2	$⊢ (x \in X, y \in Y ⟼ A) \in ((J \times_{t} K) Cn L) \to L \in Top$
42	3 41	syl	$⊢ φ \to L \in Top$
43		toptopon2	$⊢ L \in Top \leftrightarrow L \in TopOn (⋃ L)$
44	42 43	sylib	$⊢ φ \to L \in TopOn (⋃ L)$
45		cnf2	$⊢ (J \times_{t} K \in TopOn (X \times Y) \land L \in TopOn (⋃ L) \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 ⟶ ⋃ L$
46	35 44 3 45	syl3anc	$⊢ φ \to (x \in X, y \in Y ⟼ A) : X \times Y ⟶ ⋃ L$
47		eqid	$⊢ (x \in X, y \in Y ⟼ A) = (x \in X, y \in Y ⟼ A)$
48	47	fmpo	$⊢ \forall x \in X \forall y \in Y A \in ⋃ L \leftrightarrow (x \in X, y \in Y ⟼ A) : X \times Y ⟶ ⋃ L$
49	46 48	sylibr	$⊢ φ \to \forall x \in X \forall y \in Y A \in ⋃ L$
50		rsp2	$⊢ \forall x \in X \forall y \in Y A \in ⋃ L \to ((x \in X \land y \in Y) \to A \in ⋃ L)$
51	49 50	syl	$⊢ φ \to ((x \in X \land y \in Y) \to A \in ⋃ L)$
52	51	3impib	$⊢ (φ \land x \in X \land y \in Y) \to A \in ⋃ L$
53	47	ovmpt4g	$⊢ (x \in X \land y \in Y \land A \in ⋃ L) \to x (x \in X, y \in Y ⟼ A) y = A$
54	39 40 52 53	syl3anc	$⊢ (φ \land x \in X \land y \in Y) \to x (x \in X, y \in Y ⟼ A) y = A$
55		cntop2	$⊢ (x \in X, y \in Y ⟼ B) \in ((J \times_{t} K) Cn M) \to M \in Top$
56	4 55	syl	$⊢ φ \to M \in Top$
57		toptopon2	$⊢ M \in Top \leftrightarrow M \in TopOn (⋃ M)$
58	56 57	sylib	$⊢ φ \to M \in TopOn (⋃ M)$
59		cnf2	$⊢ (J \times_{t} K \in TopOn (X \times Y) \land M \in TopOn (⋃ M) \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 ⟶ ⋃ M$
60	35 58 4 59	syl3anc	$⊢ φ \to (x \in X, y \in Y ⟼ B) : X \times Y ⟶ ⋃ M$
61		eqid	$⊢ (x \in X, y \in Y ⟼ B) = (x \in X, y \in Y ⟼ B)$
62	61	fmpo	$⊢ \forall x \in X \forall y \in Y B \in ⋃ M \leftrightarrow (x \in X, y \in Y ⟼ B) : X \times Y ⟶ ⋃ M$
63	60 62	sylibr	$⊢ φ \to \forall x \in X \forall y \in Y B \in ⋃ M$
64		rsp2	$⊢ \forall x \in X \forall y \in Y B \in ⋃ M \to ((x \in X \land y \in Y) \to B \in ⋃ M)$
65	63 64	syl	$⊢ φ \to ((x \in X \land y \in Y) \to B \in ⋃ M)$
66	65	3impib	$⊢ (φ \land x \in X \land y \in Y) \to B \in ⋃ M$
67	61	ovmpt4g	$⊢ (x \in X \land y \in Y \land B \in ⋃ M) \to x (x \in X, y \in Y ⟼ B) y = B$
68	39 40 66 67	syl3anc	$⊢ (φ \land x \in X \land y \in Y) \to x (x \in X, y \in Y ⟼ B) y = B$
69	54 68	opeq12d	$⊢ (φ \land x \in X \land y \in Y) \to ⟨x (x \in X, y \in Y ⟼ A) y, x (x \in X, y \in Y ⟼ B) y⟩ = ⟨A, B⟩$
70	69	mpoeq3dva	$⊢ φ \to (x \in X, y \in Y ⟼ ⟨x (x \in X, y \in Y ⟼ A) y, x (x \in X, y \in Y ⟼ B) y⟩) = (x \in X, y \in Y ⟼ ⟨A, B⟩)$
71	33 38 70	3eqtr3a	$⊢ φ \to (z \in ⋃ (J \times_{t} K) ⟼ ⟨(x \in X, y \in Y ⟼ A) (z), (x \in X, y \in Y ⟼ B) (z)⟩) = (x \in X, y \in Y ⟼ ⟨A, B⟩)$
72		eqid	$⊢ ⋃ (J \times_{t} K) = ⋃ (J \times_{t} K)$
73		eqid	$⊢ (z \in ⋃ (J \times_{t} K) ⟼ ⟨(x \in X, y \in Y ⟼ A) (z), (x \in X, y \in Y ⟼ B) (z)⟩) = (z \in ⋃ (J \times_{t} K) ⟼ ⟨(x \in X, y \in Y ⟼ A) (z), (x \in X, y \in Y ⟼ B) (z)⟩)$
74	72 73	txcnmpt	$⊢ ((x \in X, y \in Y ⟼ A) \in ((J \times_{t} K) Cn L) \land (x \in X, y \in Y ⟼ B) \in ((J \times_{t} K) Cn M)) \to (z \in ⋃ (J \times_{t} K) ⟼ ⟨(x \in X, y \in Y ⟼ A) (z), (x \in X, y \in Y ⟼ B) (z)⟩) \in ((J \times_{t} K) Cn (L \times_{t} M))$
75	3 4 74	syl2anc	$⊢ φ \to (z \in ⋃ (J \times_{t} K) ⟼ ⟨(x \in X, y \in Y ⟼ A) (z), (x \in X, y \in Y ⟼ B) (z)⟩) \in ((J \times_{t} K) Cn (L \times_{t} M))$
76	71 75	eqeltrrd	$⊢ φ \to (x \in X, y \in Y ⟼ ⟨A, B⟩) \in ((J \times_{t} K) Cn (L \times_{t} M))$

Metamath Proof Explorer

Theorem cnmpt2t

Proof