![]() |
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 21562 | . . 3 ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) ↔ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐹:𝑋⟶𝑌 ∧ ∀𝑥 ∈ 𝐾 (◡𝐹 “ 𝑥) ∈ 𝐽))) |
4 | 3 | simprbi 489 | . 2 ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → (𝐹:𝑋⟶𝑌 ∧ ∀𝑥 ∈ 𝐾 (◡𝐹 “ 𝑥) ∈ 𝐽)) |
5 | 4 | simpld 487 | 1 ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹:𝑋⟶𝑌) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 387 = wceq 1507 ∈ wcel 2050 ∀wral 3082 ∪ cuni 4708 ◡ccnv 5402 “ cima 5406 ⟶wf 6181 (class class class)co 6974 Topctop 21217 Cn ccn 21548 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-13 2301 ax-ext 2744 ax-sep 5056 ax-nul 5063 ax-pow 5115 ax-pr 5182 ax-un 7277 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-mo 2547 df-eu 2584 df-clab 2753 df-cleq 2765 df-clel 2840 df-nfc 2912 df-ral 3087 df-rex 3088 df-rab 3091 df-v 3411 df-sbc 3676 df-dif 3826 df-un 3828 df-in 3830 df-ss 3837 df-nul 4173 df-if 4345 df-pw 4418 df-sn 4436 df-pr 4438 df-op 4442 df-uni 4709 df-br 4926 df-opab 4988 df-mpt 5005 df-id 5308 df-xp 5409 df-rel 5410 df-cnv 5411 df-co 5412 df-dm 5413 df-rn 5414 df-res 5415 df-ima 5416 df-iota 6149 df-fun 6187 df-fn 6188 df-f 6189 df-fv 6193 df-ov 6977 df-oprab 6978 df-mpo 6979 df-map 8206 df-top 21218 df-topon 21235 df-cn 21551 |
This theorem is referenced by: cnco 21590 cnclima 21592 cnntri 21595 cnclsi 21596 cnss1 21600 cnss2 21601 cncnpi 21602 cncnp2 21605 cnrest 21609 cnrest2 21610 cnt0 21670 cnt1 21674 cnhaus 21678 dnsconst 21702 cncmp 21716 rncmp 21720 imacmp 21721 cnconn 21746 connima 21749 conncn 21750 2ndcomap 21782 kgencn2 21881 kgencn3 21882 txcnmpt 21948 uptx 21949 txcn 21950 hauseqlcld 21970 xkohaus 21977 xkoptsub 21978 xkopjcn 21980 xkoco1cn 21981 xkoco2cn 21982 xkococnlem 21983 cnmpt11f 21988 cnmpt21f 21996 hmeocnv 22086 hmeores 22095 txhmeo 22127 cnextfres 22393 bndth 23277 evth 23278 evth2 23279 htpyco2 23298 phtpyco2 23309 reparphti 23316 copco 23337 pcopt 23341 pcopt2 23342 pcoass 23343 pcorevlem 23345 pcorev2 23347 hauseqcn 30811 pl1cn 30871 rrhf 30912 esumcocn 31012 cnmbfm 31195 cnpconn 32091 ptpconn 32094 sconnpi1 32100 txsconnlem 32101 cvxsconn 32104 cvmseu 32137 cvmopnlem 32139 cvmfolem 32140 cvmliftmolem1 32142 cvmliftmolem2 32143 cvmliftlem3 32148 cvmliftlem6 32151 cvmliftlem7 32152 cvmliftlem8 32153 cvmliftlem9 32154 cvmliftlem10 32155 cvmliftlem11 32156 cvmliftlem13 32157 cvmliftlem15 32159 cvmlift2lem3 32166 cvmlift2lem5 32168 cvmlift2lem7 32170 cvmlift2lem9 32172 cvmlift2lem10 32173 cvmliftphtlem 32178 cvmlift3lem1 32180 cvmlift3lem2 32181 cvmlift3lem4 32183 cvmlift3lem5 32184 cvmlift3lem6 32185 cvmlift3lem7 32186 cvmlift3lem8 32187 cvmlift3lem9 32188 poimirlem31 34393 poimir 34395 broucube 34396 cnres2 34512 cnresima 34513 hausgraph 39237 refsum2cnlem1 40742 itgsubsticclem 41715 stoweidlem62 41803 cnfsmf 42473 |
Copyright terms: Public domain | W3C validator |