Metamath Proof Explorer

Theorem 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 ⊢φ→J∈TopOn⁡X
cnmpt11.a ⊢φ→x∈X⟼A∈JCnK
cnmpt1t.b ⊢φ→x∈X⟼B∈JCnL
Assertion cnmpt1t ⊢φ→x∈X⟼AB∈JCnK×tL

Proof

Step Hyp Ref Expression
1 cnmptid.j ⊢φ→J∈TopOn⁡X
2 cnmpt11.a ⊢φ→x∈X⟼A∈JCnK
3 cnmpt1t.b ⊢φ→x∈X⟼B∈JCnL
4 toponuni ⊢J∈TopOn⁡X→X=⋃J
5 mpteq1 ⊢X=⋃J→x∈X⟼x∈X⟼A⁡xx∈X⟼B⁡x=x∈⋃J⟼x∈X⟼A⁡xx∈X⟼B⁡x
6 1 4 5 3syl ⊢φ→x∈X⟼x∈X⟼A⁡xx∈X⟼B⁡x=x∈⋃J⟼x∈X⟼A⁡xx∈X⟼B⁡x
7 simpr ⊢φ∧x∈X→x∈X
8 cntop2 ⊢x∈X⟼A∈JCnK→K∈Top
9 2 8 syl ⊢φ→K∈Top
10 toptopon2 ⊢K∈Top↔K∈TopOn⁡⋃K
11 9 10 sylib ⊢φ→K∈TopOn⁡⋃K
12 cnf2 ⊢J∈TopOn⁡X∧K∈TopOn⁡⋃K∧x∈X⟼A∈JCnK→x∈X⟼A:X⟶⋃K
13 1 11 2 12 syl3anc ⊢φ→x∈X⟼A:X⟶⋃K
14 13 fvmptelcdm ⊢φ∧x∈X→A∈⋃K
15 eqid ⊢x∈X⟼A=x∈X⟼A
16 15 fvmpt2 ⊢x∈X∧A∈⋃K→x∈X⟼A⁡x=A
17 7 14 16 syl2anc ⊢φ∧x∈X→x∈X⟼A⁡x=A
18 cntop2 ⊢x∈X⟼B∈JCnL→L∈Top
19 3 18 syl ⊢φ→L∈Top
20 toptopon2 ⊢L∈Top↔L∈TopOn⁡⋃L
21 19 20 sylib ⊢φ→L∈TopOn⁡⋃L
22 cnf2 ⊢J∈TopOn⁡X∧L∈TopOn⁡⋃L∧x∈X⟼B∈JCnL→x∈X⟼B:X⟶⋃L
23 1 21 3 22 syl3anc ⊢φ→x∈X⟼B:X⟶⋃L
24 23 fvmptelcdm ⊢φ∧x∈X→B∈⋃L
25 eqid ⊢x∈X⟼B=x∈X⟼B
26 25 fvmpt2 ⊢x∈X∧B∈⋃L→x∈X⟼B⁡x=B
27 7 24 26 syl2anc ⊢φ∧x∈X→x∈X⟼B⁡x=B
28 17 27 opeq12d ⊢φ∧x∈X→x∈X⟼A⁡xx∈X⟼B⁡x=AB
29 28 mpteq2dva ⊢φ→x∈X⟼x∈X⟼A⁡xx∈X⟼B⁡x=x∈X⟼AB
30 6 29 eqtr3d ⊢φ→x∈⋃J⟼x∈X⟼A⁡xx∈X⟼B⁡x=x∈X⟼AB
31 eqid ⊢⋃J=⋃J
32 nfcv ⊢Ⅎ_yx∈X⟼A⁡xx∈X⟼B⁡x
33 nffvmpt1 ⊢Ⅎ_xx∈X⟼A⁡y
34 nffvmpt1 ⊢Ⅎ_xx∈X⟼B⁡y
35 33 34 nfop ⊢Ⅎ_xx∈X⟼A⁡yx∈X⟼B⁡y
36 fveq2 ⊢x=y→x∈X⟼A⁡x=x∈X⟼A⁡y
37 fveq2 ⊢x=y→x∈X⟼B⁡x=x∈X⟼B⁡y
38 36 37 opeq12d ⊢x=y→x∈X⟼A⁡xx∈X⟼B⁡x=x∈X⟼A⁡yx∈X⟼B⁡y
39 32 35 38 cbvmpt ⊢x∈⋃J⟼x∈X⟼A⁡xx∈X⟼B⁡x=y∈⋃J⟼x∈X⟼A⁡yx∈X⟼B⁡y
40 31 39 txcnmpt ⊢x∈X⟼A∈JCnK∧x∈X⟼B∈JCnL→x∈⋃J⟼x∈X⟼A⁡xx∈X⟼B⁡x∈JCnK×tL
41 2 3 40 syl2anc ⊢φ→x∈⋃J⟼x∈X⟼A⁡xx∈X⟼B⁡x∈JCnK×tL
42 30 41 eqeltrrd ⊢φ→x∈X⟼AB∈JCnK×tL