![]() |
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 23060 | . . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑥 ∈ 𝐾 (◡𝐹 “ 𝑥) ∈ 𝐽))) | |
2 | 1 | simprbda 498 | . 2 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹:𝑋⟶𝑌) |
3 | 2 | 3impa 1107 | 1 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹:𝑋⟶𝑌) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1084 ∈ wcel 2098 ∀wral 3053 ◡ccnv 5665 “ cima 5669 ⟶wf 6529 ‘cfv 6533 (class class class)co 7401 TopOnctopon 22733 Cn ccn 23049 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2163 ax-ext 2695 ax-sep 5289 ax-nul 5296 ax-pow 5353 ax-pr 5417 ax-un 7718 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2526 df-eu 2555 df-clab 2702 df-cleq 2716 df-clel 2802 df-nfc 2877 df-ne 2933 df-ral 3054 df-rex 3063 df-rab 3425 df-v 3468 df-sbc 3770 df-dif 3943 df-un 3945 df-in 3947 df-ss 3957 df-nul 4315 df-if 4521 df-pw 4596 df-sn 4621 df-pr 4623 df-op 4627 df-uni 4900 df-br 5139 df-opab 5201 df-mpt 5222 df-id 5564 df-xp 5672 df-rel 5673 df-cnv 5674 df-co 5675 df-dm 5676 df-rn 5677 df-res 5678 df-ima 5679 df-iota 6485 df-fun 6535 df-fn 6536 df-f 6537 df-fv 6541 df-ov 7404 df-oprab 7405 df-mpo 7406 df-map 8817 df-top 22717 df-topon 22734 df-cn 23052 |
This theorem is referenced by: iscncl 23094 cncls2 23098 cncls 23099 cnntr 23100 cnrest2 23111 cnrest2r 23112 ptcn 23452 txdis1cn 23460 lmcn2 23474 cnmpt11 23488 cnmpt1t 23490 cnmpt12 23492 cnmpt21 23496 cnmpt2t 23498 cnmpt22 23499 cnmpt22f 23500 cnmptcom 23503 cnmptkp 23505 cnmptk1 23506 cnmpt1k 23507 cnmptkk 23508 cnmptk1p 23510 cnmptk2 23511 cnmpt2k 23513 qtopss 23540 qtopeu 23541 qtopomap 23543 qtopcmap 23544 hmeof1o2 23588 xpstopnlem1 23634 xkocnv 23639 xkohmeo 23640 qtophmeo 23642 cnmpt1plusg 23912 cnmpt2plusg 23913 tsmsmhm 23971 cnmpt1vsca 24019 cnmpt2vsca 24020 cnmpt1ds 24679 cnmpt2ds 24680 fsumcn 24709 cnmpopc 24770 htpyco1 24825 htpyco2 24826 phtpyco2 24837 pi1xfrf 24901 pi1xfr 24903 pi1xfrcnvlem 24904 pi1xfrcnv 24905 pi1cof 24907 pi1coghm 24909 cnmpt1ip 25096 cnmpt2ip 25097 txsconnlem 34686 txsconn 34687 cvmlift3lem6 34770 fcnre 44164 refsumcn 44169 refsum2cnlem1 44176 fprodcnlem 44766 icccncfext 45054 itgsubsticclem 45142 |
Copyright terms: Public domain | W3C validator |