| 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 23213 | . . 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 5623 “ cima 5627 ⟶wf 6488 (class class class)co 7360 Topctop 22868 Cn ccn 23199 |
| 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 5231 ax-nul 5241 ax-pow 5302 ax-pr 5370 ax-un 7682 |
| 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 5519 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-res 5636 df-ima 5637 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-fv 6500 df-ov 7363 df-oprab 7364 df-mpo 7365 df-map 8768 df-top 22869 df-topon 22886 df-cn 23202 |
| This theorem is referenced by: cnco 23241 cnclima 23243 cnntri 23246 cnclsi 23247 cnss1 23251 cnss2 23252 cncnpi 23253 cncnp2 23256 cnrest 23260 cnrest2 23261 cnt0 23321 cnt1 23325 cnhaus 23329 dnsconst 23353 cncmp 23367 rncmp 23371 imacmp 23372 cnconn 23397 connima 23400 conncn 23401 2ndcomap 23433 kgencn2 23532 kgencn3 23533 txcnmpt 23599 uptx 23600 txcn 23601 hauseqlcld 23621 xkohaus 23628 xkoptsub 23629 xkopjcn 23631 xkoco1cn 23632 xkoco2cn 23633 xkococnlem 23634 cnmpt11f 23639 cnmpt21f 23647 hmeocnv 23737 hmeores 23746 txhmeo 23778 cnextfres 24044 bndth 24935 evth 24936 evth2 24937 htpyco2 24956 phtpyco2 24967 reparphti 24974 copco 24995 pcopt 24999 pcopt2 25000 pcoass 25001 pcorevlem 25003 pcorev2 25005 hauseqcn 34058 pl1cn 34115 rrhf 34158 esumcocn 34240 cnmbfm 34423 cnpconn 35428 ptpconn 35431 sconnpi1 35437 txsconnlem 35438 cvxsconn 35441 cvmseu 35474 cvmopnlem 35476 cvmfolem 35477 cvmliftmolem1 35479 cvmliftmolem2 35480 cvmliftlem3 35485 cvmliftlem6 35488 cvmliftlem7 35489 cvmliftlem8 35490 cvmliftlem9 35491 cvmliftlem10 35492 cvmliftlem11 35493 cvmliftlem13 35494 cvmliftlem15 35496 cvmlift2lem3 35503 cvmlift2lem5 35505 cvmlift2lem7 35507 cvmlift2lem9 35509 cvmlift2lem10 35510 cvmliftphtlem 35515 cvmlift3lem1 35517 cvmlift3lem2 35518 cvmlift3lem4 35520 cvmlift3lem5 35521 cvmlift3lem6 35522 cvmlift3lem7 35523 cvmlift3lem8 35524 cvmlift3lem9 35525 poimirlem31 37986 poimir 37988 broucube 37989 cnres2 38098 cnresima 38099 hausgraph 43651 refsum2cnlem1 45486 itgsubsticclem 46421 stoweidlem62 46508 cnfsmf 47186 cnneiima 49404 sepfsepc 49415 |
| Copyright terms: Public domain | W3C validator |