Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > cnf2 | Structured version Visualization version GIF version |
Description: A continuous function is a mapping. (Contributed by Mario Carneiro, 21-Aug-2015.) |
Ref | Expression |
---|---|
cnf2 | ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹:𝑋⟶𝑌) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | iscn 21986 | . . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑥 ∈ 𝐾 (◡𝐹 “ 𝑥) ∈ 𝐽))) | |
2 | 1 | simprbda 502 | . 2 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹:𝑋⟶𝑌) |
3 | 2 | 3impa 1111 | 1 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹:𝑋⟶𝑌) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 ∧ w3a 1088 ∈ wcel 2114 ∀wral 3053 ◡ccnv 5524 “ cima 5528 ⟶wf 6335 ‘cfv 6339 (class class class)co 7170 TopOnctopon 21661 Cn ccn 21975 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2162 ax-12 2179 ax-ext 2710 ax-sep 5167 ax-nul 5174 ax-pow 5232 ax-pr 5296 ax-un 7479 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1787 df-nf 1791 df-sb 2075 df-mo 2540 df-eu 2570 df-clab 2717 df-cleq 2730 df-clel 2811 df-nfc 2881 df-ne 2935 df-ral 3058 df-rex 3059 df-rab 3062 df-v 3400 df-sbc 3681 df-dif 3846 df-un 3848 df-in 3850 df-ss 3860 df-nul 4212 df-if 4415 df-pw 4490 df-sn 4517 df-pr 4519 df-op 4523 df-uni 4797 df-br 5031 df-opab 5093 df-mpt 5111 df-id 5429 df-xp 5531 df-rel 5532 df-cnv 5533 df-co 5534 df-dm 5535 df-rn 5536 df-res 5537 df-ima 5538 df-iota 6297 df-fun 6341 df-fn 6342 df-f 6343 df-fv 6347 df-ov 7173 df-oprab 7174 df-mpo 7175 df-map 8439 df-top 21645 df-topon 21662 df-cn 21978 |
This theorem is referenced by: iscncl 22020 cncls2 22024 cncls 22025 cnntr 22026 cnrest2 22037 cnrest2r 22038 ptcn 22378 txdis1cn 22386 lmcn2 22400 cnmpt11 22414 cnmpt1t 22416 cnmpt12 22418 cnmpt21 22422 cnmpt2t 22424 cnmpt22 22425 cnmpt22f 22426 cnmptcom 22429 cnmptkp 22431 cnmptk1 22432 cnmpt1k 22433 cnmptkk 22434 cnmptk1p 22436 cnmptk2 22437 cnmpt2k 22439 qtopss 22466 qtopeu 22467 qtopomap 22469 qtopcmap 22470 hmeof1o2 22514 xpstopnlem1 22560 xkocnv 22565 xkohmeo 22566 qtophmeo 22568 cnmpt1plusg 22838 cnmpt2plusg 22839 tsmsmhm 22897 cnmpt1vsca 22945 cnmpt2vsca 22946 cnmpt1ds 23594 cnmpt2ds 23595 fsumcn 23622 cnmpopc 23680 htpyco1 23730 htpyco2 23731 phtpyco2 23742 pi1xfrf 23805 pi1xfr 23807 pi1xfrcnvlem 23808 pi1xfrcnv 23809 pi1cof 23811 pi1coghm 23813 cnmpt1ip 23999 cnmpt2ip 24000 txsconnlem 32773 txsconn 32774 cvmlift3lem6 32857 fcnre 42126 refsumcn 42131 refsum2cnlem1 42138 fprodcnlem 42702 icccncfext 42990 itgsubsticclem 43078 |
Copyright terms: Public domain | W3C validator |