![]() |
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 23233 | . . 3 ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) ↔ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐹:𝑋⟶𝑌 ∧ ∀𝑥 ∈ 𝐾 (◡𝐹 “ 𝑥) ∈ 𝐽))) |
4 | 3 | simprbi 495 | . 2 ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → (𝐹:𝑋⟶𝑌 ∧ ∀𝑥 ∈ 𝐾 (◡𝐹 “ 𝑥) ∈ 𝐽)) |
5 | 4 | simpld 493 | 1 ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹:𝑋⟶𝑌) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 = wceq 1534 ∈ wcel 2099 ∀wral 3051 ∪ cuni 4913 ◡ccnv 5681 “ cima 5685 ⟶wf 6550 (class class class)co 7424 Topctop 22886 Cn ccn 23219 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2167 ax-ext 2697 ax-sep 5304 ax-nul 5311 ax-pow 5369 ax-pr 5433 ax-un 7746 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2529 df-eu 2558 df-clab 2704 df-cleq 2718 df-clel 2803 df-nfc 2878 df-ne 2931 df-ral 3052 df-rex 3061 df-rab 3420 df-v 3464 df-sbc 3777 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4326 df-if 4534 df-pw 4609 df-sn 4634 df-pr 4636 df-op 4640 df-uni 4914 df-br 5154 df-opab 5216 df-mpt 5237 df-id 5580 df-xp 5688 df-rel 5689 df-cnv 5690 df-co 5691 df-dm 5692 df-rn 5693 df-res 5694 df-ima 5695 df-iota 6506 df-fun 6556 df-fn 6557 df-f 6558 df-fv 6562 df-ov 7427 df-oprab 7428 df-mpo 7429 df-map 8857 df-top 22887 df-topon 22904 df-cn 23222 |
This theorem is referenced by: cnco 23261 cnclima 23263 cnntri 23266 cnclsi 23267 cnss1 23271 cnss2 23272 cncnpi 23273 cncnp2 23276 cnrest 23280 cnrest2 23281 cnt0 23341 cnt1 23345 cnhaus 23349 dnsconst 23373 cncmp 23387 rncmp 23391 imacmp 23392 cnconn 23417 connima 23420 conncn 23421 2ndcomap 23453 kgencn2 23552 kgencn3 23553 txcnmpt 23619 uptx 23620 txcn 23621 hauseqlcld 23641 xkohaus 23648 xkoptsub 23649 xkopjcn 23651 xkoco1cn 23652 xkoco2cn 23653 xkococnlem 23654 cnmpt11f 23659 cnmpt21f 23667 hmeocnv 23757 hmeores 23766 txhmeo 23798 cnextfres 24064 bndth 24975 evth 24976 evth2 24977 htpyco2 24996 phtpyco2 25007 reparphti 25014 reparphtiOLD 25015 copco 25036 pcopt 25040 pcopt2 25041 pcoass 25042 pcorevlem 25044 pcorev2 25046 hauseqcn 33713 pl1cn 33770 rrhf 33813 esumcocn 33913 cnmbfm 34097 cnpconn 35058 ptpconn 35061 sconnpi1 35067 txsconnlem 35068 cvxsconn 35071 cvmseu 35104 cvmopnlem 35106 cvmfolem 35107 cvmliftmolem1 35109 cvmliftmolem2 35110 cvmliftlem3 35115 cvmliftlem6 35118 cvmliftlem7 35119 cvmliftlem8 35120 cvmliftlem9 35121 cvmliftlem10 35122 cvmliftlem11 35123 cvmliftlem13 35124 cvmliftlem15 35126 cvmlift2lem3 35133 cvmlift2lem5 35135 cvmlift2lem7 35137 cvmlift2lem9 35139 cvmlift2lem10 35140 cvmliftphtlem 35145 cvmlift3lem1 35147 cvmlift3lem2 35148 cvmlift3lem4 35150 cvmlift3lem5 35151 cvmlift3lem6 35152 cvmlift3lem7 35153 cvmlift3lem8 35154 cvmlift3lem9 35155 poimirlem31 37352 poimir 37354 broucube 37355 cnres2 37464 cnresima 37465 hausgraph 42870 refsum2cnlem1 44636 itgsubsticclem 45596 stoweidlem62 45683 cnfsmf 46361 cnneiima 48250 sepfsepc 48261 |
Copyright terms: Public domain | W3C validator |