cnmpt22f

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)$
	cnmpt22f.f	$⊢ φ \to F \in ((L \times_{t} M) Cn N)$
Assertion	cnmpt22f	$⊢ φ \to (x \in X, y \in Y ⟼ A F B) \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		cnmpt22f.f	$⊢ φ \to F \in ((L \times_{t} M) Cn N)$
6		cntop2	$⊢ (x \in X, y \in Y ⟼ A) \in ((J \times_{t} K) Cn L) \to L \in Top$
7	3 6	syl	$⊢ φ \to L \in Top$
8		toptopon2	$⊢ L \in Top \leftrightarrow L \in TopOn (⋃ L)$
9	7 8	sylib	$⊢ φ \to L \in TopOn (⋃ L)$
10		cntop2	$⊢ (x \in X, y \in Y ⟼ B) \in ((J \times_{t} K) Cn M) \to M \in Top$
11	4 10	syl	$⊢ φ \to M \in Top$
12		toptopon2	$⊢ M \in Top \leftrightarrow M \in TopOn (⋃ M)$
13	11 12	sylib	$⊢ φ \to M \in TopOn (⋃ M)$
14		txtopon	$⊢ (L \in TopOn (⋃ L) \land M \in TopOn (⋃ M)) \to L \times_{t} M \in TopOn (⋃ L \times ⋃ M)$
15	9 13 14	syl2anc	$⊢ φ \to L \times_{t} M \in TopOn (⋃ L \times ⋃ M)$
16		cntop2	$⊢ F \in ((L \times_{t} M) Cn N) \to N \in Top$
17	5 16	syl	$⊢ φ \to N \in Top$
18		toptopon2	$⊢ N \in Top \leftrightarrow N \in TopOn (⋃ N)$
19	17 18	sylib	$⊢ φ \to N \in TopOn (⋃ N)$
20		cnf2	$⊢ (L \times_{t} M \in TopOn (⋃ L \times ⋃ M) \land N \in TopOn (⋃ N) \land F \in ((L \times_{t} M) Cn N)) \to F : ⋃ L \times ⋃ M ⟶ ⋃ N$
21	15 19 5 20	syl3anc	$⊢ φ \to F : ⋃ L \times ⋃ M ⟶ ⋃ N$
22	21	ffnd	$⊢ φ \to F Fn (⋃ L \times ⋃ M)$
23		fnov	$⊢ F Fn (⋃ L \times ⋃ M) \leftrightarrow F = (z \in ⋃ L, w \in ⋃ M ⟼ z F w)$
24	22 23	sylib	$⊢ φ \to F = (z \in ⋃ L, w \in ⋃ M ⟼ z F w)$
25	24 5	eqeltrrd	$⊢ φ \to (z \in ⋃ L, w \in ⋃ M ⟼ z F w) \in ((L \times_{t} M) Cn N)$
26		oveq12	$⊢ (z = A \land w = B) \to z F w = A F B$
27	1 2 3 4 9 13 25 26	cnmpt22	$⊢ φ \to (x \in X, y \in Y ⟼ A F B) \in ((J \times_{t} K) Cn N)$

Metamath Proof Explorer

Theorem cnmpt22f

Proof