| 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 23217 | . . 3 ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) ↔ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐹:𝑋⟶𝑌 ∧ ∀𝑥 ∈ 𝐾 (◡𝐹 “ 𝑥) ∈ 𝐽))) |
| 4 | 3 | simprbi 497 | . 2 ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → (𝐹:𝑋⟶𝑌 ∧ ∀𝑥 ∈ 𝐾 (◡𝐹 “ 𝑥) ∈ 𝐽)) |
| 5 | 4 | simpld 494 | 1 ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹:𝑋⟶𝑌) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 = wceq 1542 ∈ wcel 2114 ∀wral 3052 ∪ cuni 4851 ◡ccnv 5625 “ cima 5629 ⟶wf 6490 (class class class)co 7362 Topctop 22872 Cn ccn 23203 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-sep 5232 ax-nul 5242 ax-pow 5304 ax-pr 5372 ax-un 7684 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-ral 3053 df-rex 3063 df-rab 3391 df-v 3432 df-sbc 3730 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-op 4575 df-uni 4852 df-br 5087 df-opab 5149 df-mpt 5168 df-id 5521 df-xp 5632 df-rel 5633 df-cnv 5634 df-co 5635 df-dm 5636 df-rn 5637 df-res 5638 df-ima 5639 df-iota 6450 df-fun 6496 df-fn 6497 df-f 6498 df-fv 6502 df-ov 7365 df-oprab 7366 df-mpo 7367 df-map 8770 df-top 22873 df-topon 22890 df-cn 23206 |
| This theorem is referenced by: cnco 23245 cnclima 23247 cnntri 23250 cnclsi 23251 cnss1 23255 cnss2 23256 cncnpi 23257 cncnp2 23260 cnrest 23264 cnrest2 23265 cnt0 23325 cnt1 23329 cnhaus 23333 dnsconst 23357 cncmp 23371 rncmp 23375 imacmp 23376 cnconn 23401 connima 23404 conncn 23405 2ndcomap 23437 kgencn2 23536 kgencn3 23537 txcnmpt 23603 uptx 23604 txcn 23605 hauseqlcld 23625 xkohaus 23632 xkoptsub 23633 xkopjcn 23635 xkoco1cn 23636 xkoco2cn 23637 xkococnlem 23638 cnmpt11f 23643 cnmpt21f 23651 hmeocnv 23741 hmeores 23750 txhmeo 23782 cnextfres 24048 bndth 24939 evth 24940 evth2 24941 htpyco2 24960 phtpyco2 24971 reparphti 24978 copco 24999 pcopt 25003 pcopt2 25004 pcoass 25005 pcorevlem 25007 pcorev2 25009 hauseqcn 34062 pl1cn 34119 rrhf 34162 esumcocn 34244 cnmbfm 34427 cnpconn 35432 ptpconn 35435 sconnpi1 35441 txsconnlem 35442 cvxsconn 35445 cvmseu 35478 cvmopnlem 35480 cvmfolem 35481 cvmliftmolem1 35483 cvmliftmolem2 35484 cvmliftlem3 35489 cvmliftlem6 35492 cvmliftlem7 35493 cvmliftlem8 35494 cvmliftlem9 35495 cvmliftlem10 35496 cvmliftlem11 35497 cvmliftlem13 35498 cvmliftlem15 35500 cvmlift2lem3 35507 cvmlift2lem5 35509 cvmlift2lem7 35511 cvmlift2lem9 35513 cvmlift2lem10 35514 cvmliftphtlem 35519 cvmlift3lem1 35521 cvmlift3lem2 35522 cvmlift3lem4 35524 cvmlift3lem5 35525 cvmlift3lem6 35526 cvmlift3lem7 35527 cvmlift3lem8 35528 cvmlift3lem9 35529 poimirlem31 37992 poimir 37994 broucube 37995 cnres2 38104 cnresima 38105 hausgraph 43657 refsum2cnlem1 45492 itgsubsticclem 46427 stoweidlem62 46514 cnfsmf 47192 cnneiima 49410 sepfsepc 49421 |
| Copyright terms: Public domain | W3C validator |