![]() |
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 21242 | . . 3 ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) ↔ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐹:𝑋⟶𝑌 ∧ ∀𝑥 ∈ 𝐾 (◡𝐹 “ 𝑥) ∈ 𝐽))) |
4 | 3 | simprbi 483 | . 2 ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → (𝐹:𝑋⟶𝑌 ∧ ∀𝑥 ∈ 𝐾 (◡𝐹 “ 𝑥) ∈ 𝐽)) |
5 | 4 | simpld 477 | 1 ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹:𝑋⟶𝑌) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 = wceq 1630 ∈ wcel 2137 ∀wral 3048 ∪ cuni 4586 ◡ccnv 5263 “ cima 5267 ⟶wf 6043 (class class class)co 6811 Topctop 20898 Cn ccn 21228 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1869 ax-4 1884 ax-5 1986 ax-6 2052 ax-7 2088 ax-8 2139 ax-9 2146 ax-10 2166 ax-11 2181 ax-12 2194 ax-13 2389 ax-ext 2738 ax-sep 4931 ax-nul 4939 ax-pow 4990 ax-pr 5053 ax-un 7112 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1074 df-tru 1633 df-ex 1852 df-nf 1857 df-sb 2045 df-eu 2609 df-mo 2610 df-clab 2745 df-cleq 2751 df-clel 2754 df-nfc 2889 df-ne 2931 df-ral 3053 df-rex 3054 df-rab 3057 df-v 3340 df-sbc 3575 df-dif 3716 df-un 3718 df-in 3720 df-ss 3727 df-nul 4057 df-if 4229 df-pw 4302 df-sn 4320 df-pr 4322 df-op 4326 df-uni 4587 df-br 4803 df-opab 4863 df-mpt 4880 df-id 5172 df-xp 5270 df-rel 5271 df-cnv 5272 df-co 5273 df-dm 5274 df-rn 5275 df-res 5276 df-ima 5277 df-iota 6010 df-fun 6049 df-fn 6050 df-f 6051 df-fv 6055 df-ov 6814 df-oprab 6815 df-mpt2 6816 df-map 8023 df-top 20899 df-topon 20916 df-cn 21231 |
This theorem is referenced by: cnco 21270 cnclima 21272 cnntri 21275 cnclsi 21276 cnss1 21280 cnss2 21281 cncnpi 21282 cncnp2 21285 cnrest 21289 cnrest2 21290 cnt0 21350 cnt1 21354 cnhaus 21358 dnsconst 21382 cncmp 21395 rncmp 21399 imacmp 21400 cnconn 21425 connima 21428 conncn 21429 2ndcomap 21461 kgencn2 21560 kgencn3 21561 txcnmpt 21627 uptx 21628 txcn 21629 hauseqlcld 21649 xkohaus 21656 xkoptsub 21657 xkopjcn 21659 xkoco1cn 21660 xkoco2cn 21661 xkococnlem 21662 cnmpt11f 21667 cnmpt21f 21675 hmeocnv 21765 hmeores 21774 txhmeo 21806 cnextfres 22072 bndth 22956 evth 22957 evth2 22958 htpyco2 22977 phtpyco2 22988 reparphti 22995 copco 23016 pcopt 23020 pcopt2 23021 pcoass 23022 pcorevlem 23024 pcorev2 23026 hauseqcn 30248 pl1cn 30308 rrhf 30349 esumcocn 30449 cnmbfm 30632 cnpconn 31517 ptpconn 31520 sconnpi1 31526 txsconnlem 31527 cvxsconn 31530 cvmseu 31563 cvmopnlem 31565 cvmfolem 31566 cvmliftmolem1 31568 cvmliftmolem2 31569 cvmliftlem3 31574 cvmliftlem6 31577 cvmliftlem7 31578 cvmliftlem8 31579 cvmliftlem9 31580 cvmliftlem10 31581 cvmliftlem11 31582 cvmliftlem13 31583 cvmliftlem15 31585 cvmlift2lem3 31592 cvmlift2lem5 31594 cvmlift2lem7 31596 cvmlift2lem9 31598 cvmlift2lem10 31599 cvmliftphtlem 31604 cvmlift3lem1 31606 cvmlift3lem2 31607 cvmlift3lem4 31609 cvmlift3lem5 31610 cvmlift3lem6 31611 cvmlift3lem7 31612 cvmlift3lem8 31613 cvmlift3lem9 31614 poimirlem31 33751 poimir 33753 broucube 33754 cnres2 33873 cnresima 33874 hausgraph 38290 refsum2cnlem1 39693 itgsubsticclem 40692 stoweidlem62 40780 cnfsmf 41453 |
Copyright terms: Public domain | W3C validator |