![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > cnmpt12f | Structured version Visualization version GIF version |
Description: The composition of continuous functions is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.) |
Ref | Expression |
---|---|
cnmptid.j | ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) |
cnmpt11.a | ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝐽 Cn 𝐾)) |
cnmpt1t.b | ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝐽 Cn 𝐿)) |
cnmpt12f.f | ⊢ (𝜑 → 𝐹 ∈ ((𝐾 ×t 𝐿) Cn 𝑀)) |
Ref | Expression |
---|---|
cnmpt12f | ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐴𝐹𝐵)) ∈ (𝐽 Cn 𝑀)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ov 6978 | . . 3 ⊢ (𝐴𝐹𝐵) = (𝐹‘〈𝐴, 𝐵〉) | |
2 | 1 | mpteq2i 5016 | . 2 ⊢ (𝑥 ∈ 𝑋 ↦ (𝐴𝐹𝐵)) = (𝑥 ∈ 𝑋 ↦ (𝐹‘〈𝐴, 𝐵〉)) |
3 | cnmptid.j | . . 3 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) | |
4 | cnmpt11.a | . . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝐽 Cn 𝐾)) | |
5 | cnmpt1t.b | . . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝐽 Cn 𝐿)) | |
6 | 3, 4, 5 | cnmpt1t 21993 | . . 3 ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 〈𝐴, 𝐵〉) ∈ (𝐽 Cn (𝐾 ×t 𝐿))) |
7 | cnmpt12f.f | . . 3 ⊢ (𝜑 → 𝐹 ∈ ((𝐾 ×t 𝐿) Cn 𝑀)) | |
8 | 3, 6, 7 | cnmpt11f 21992 | . 2 ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐹‘〈𝐴, 𝐵〉)) ∈ (𝐽 Cn 𝑀)) |
9 | 2, 8 | syl5eqel 2865 | 1 ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐴𝐹𝐵)) ∈ (𝐽 Cn 𝑀)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2051 〈cop 4442 ↦ cmpt 5005 ‘cfv 6186 (class class class)co 6975 TopOnctopon 21238 Cn ccn 21552 ×t ctx 21888 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1759 ax-4 1773 ax-5 1870 ax-6 1929 ax-7 1966 ax-8 2053 ax-9 2060 ax-10 2080 ax-11 2094 ax-12 2107 ax-13 2302 ax-ext 2745 ax-sep 5057 ax-nul 5064 ax-pow 5116 ax-pr 5183 ax-un 7278 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 835 df-3an 1071 df-tru 1511 df-ex 1744 df-nf 1748 df-sb 2017 df-mo 2548 df-eu 2585 df-clab 2754 df-cleq 2766 df-clel 2841 df-nfc 2913 df-ne 2963 df-ral 3088 df-rex 3089 df-rab 3092 df-v 3412 df-sbc 3677 df-csb 3782 df-dif 3827 df-un 3829 df-in 3831 df-ss 3838 df-nul 4174 df-if 4346 df-pw 4419 df-sn 4437 df-pr 4439 df-op 4443 df-uni 4710 df-iun 4791 df-br 4927 df-opab 4989 df-mpt 5006 df-id 5309 df-xp 5410 df-rel 5411 df-cnv 5412 df-co 5413 df-dm 5414 df-rn 5415 df-res 5416 df-ima 5417 df-iota 6150 df-fun 6188 df-fn 6189 df-f 6190 df-fv 6194 df-ov 6978 df-oprab 6979 df-mpo 6980 df-1st 7500 df-2nd 7501 df-map 8207 df-topgen 16572 df-top 21222 df-topon 21239 df-bases 21274 df-cn 21555 df-tx 21890 |
This theorem is referenced by: cnmpt12 21995 cnmpt1plusg 22415 istgp2 22419 clsnsg 22437 tgpt0 22446 cnmpt1vsca 22521 cnmpt1ds 23169 fsumcn 23197 expcn 23199 divccn 23200 cncfmpt2f 23241 cdivcncf 23244 iirevcn 23253 iihalf1cn 23255 iihalf2cn 23257 icchmeo 23264 evth 23282 evth2 23283 pcoass 23347 cnmpt1ip 23569 dvcnvlem 24292 plycn 24570 psercn2 24730 atansopn 25227 efrlim 25265 ipasslem7 28406 occllem 28877 hmopidmchi 29725 cvxpconn 32107 cvmlift2lem2 32169 cvmlift2lem3 32170 cvmliftphtlem 32182 sinccvglem 32468 knoppcnlem10 33394 broucube 34400 areacirclem2 34457 fprodcnlem 41341 |
Copyright terms: Public domain | W3C validator |