Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > cnf | Structured version Visualization version GIF version |
Description: A continuous function is a mapping. (Contributed by FL, 8-Dec-2006.) (Revised by Mario Carneiro, 21-Aug-2015.) |
Ref | Expression |
---|---|
iscnp2.1 | ⊢ 𝑋 = ∪ 𝐽 |
iscnp2.2 | ⊢ 𝑌 = ∪ 𝐾 |
Ref | Expression |
---|---|
cnf | ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹:𝑋⟶𝑌) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | iscnp2.1 | . . . 4 ⊢ 𝑋 = ∪ 𝐽 | |
2 | iscnp2.2 | . . . 4 ⊢ 𝑌 = ∪ 𝐾 | |
3 | 1, 2 | iscn2 21776 | . . 3 ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) ↔ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐹:𝑋⟶𝑌 ∧ ∀𝑥 ∈ 𝐾 (◡𝐹 “ 𝑥) ∈ 𝐽))) |
4 | 3 | simprbi 497 | . 2 ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → (𝐹:𝑋⟶𝑌 ∧ ∀𝑥 ∈ 𝐾 (◡𝐹 “ 𝑥) ∈ 𝐽)) |
5 | 4 | simpld 495 | 1 ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹:𝑋⟶𝑌) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 = wceq 1528 ∈ wcel 2105 ∀wral 3138 ∪ cuni 4832 ◡ccnv 5548 “ cima 5552 ⟶wf 6345 (class class class)co 7145 Topctop 21431 Cn ccn 21762 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2793 ax-sep 5195 ax-nul 5202 ax-pow 5258 ax-pr 5321 ax-un 7450 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-mo 2618 df-eu 2650 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ral 3143 df-rex 3144 df-rab 3147 df-v 3497 df-sbc 3772 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-nul 4291 df-if 4466 df-pw 4539 df-sn 4560 df-pr 4562 df-op 4566 df-uni 4833 df-br 5059 df-opab 5121 df-mpt 5139 df-id 5454 df-xp 5555 df-rel 5556 df-cnv 5557 df-co 5558 df-dm 5559 df-rn 5560 df-res 5561 df-ima 5562 df-iota 6308 df-fun 6351 df-fn 6352 df-f 6353 df-fv 6357 df-ov 7148 df-oprab 7149 df-mpo 7150 df-map 8398 df-top 21432 df-topon 21449 df-cn 21765 |
This theorem is referenced by: cnco 21804 cnclima 21806 cnntri 21809 cnclsi 21810 cnss1 21814 cnss2 21815 cncnpi 21816 cncnp2 21819 cnrest 21823 cnrest2 21824 cnt0 21884 cnt1 21888 cnhaus 21892 dnsconst 21916 cncmp 21930 rncmp 21934 imacmp 21935 cnconn 21960 connima 21963 conncn 21964 2ndcomap 21996 kgencn2 22095 kgencn3 22096 txcnmpt 22162 uptx 22163 txcn 22164 hauseqlcld 22184 xkohaus 22191 xkoptsub 22192 xkopjcn 22194 xkoco1cn 22195 xkoco2cn 22196 xkococnlem 22197 cnmpt11f 22202 cnmpt21f 22210 hmeocnv 22300 hmeores 22309 txhmeo 22341 cnextfres 22607 bndth 23491 evth 23492 evth2 23493 htpyco2 23512 phtpyco2 23523 reparphti 23530 copco 23551 pcopt 23555 pcopt2 23556 pcoass 23557 pcorevlem 23559 pcorev2 23561 hauseqcn 31038 pl1cn 31098 rrhf 31139 esumcocn 31239 cnmbfm 31421 cnpconn 32375 ptpconn 32378 sconnpi1 32384 txsconnlem 32385 cvxsconn 32388 cvmseu 32421 cvmopnlem 32423 cvmfolem 32424 cvmliftmolem1 32426 cvmliftmolem2 32427 cvmliftlem3 32432 cvmliftlem6 32435 cvmliftlem7 32436 cvmliftlem8 32437 cvmliftlem9 32438 cvmliftlem10 32439 cvmliftlem11 32440 cvmliftlem13 32441 cvmliftlem15 32443 cvmlift2lem3 32450 cvmlift2lem5 32452 cvmlift2lem7 32454 cvmlift2lem9 32456 cvmlift2lem10 32457 cvmliftphtlem 32462 cvmlift3lem1 32464 cvmlift3lem2 32465 cvmlift3lem4 32467 cvmlift3lem5 32468 cvmlift3lem6 32469 cvmlift3lem7 32470 cvmlift3lem8 32471 cvmlift3lem9 32472 poimirlem31 34805 poimir 34807 broucube 34808 cnres2 34924 cnresima 34925 hausgraph 39692 refsum2cnlem1 41174 itgsubsticclem 42140 stoweidlem62 42228 cnfsmf 42898 |
Copyright terms: Public domain | W3C validator |