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 21774 | . . 3 ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) ↔ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐹:𝑋⟶𝑌 ∧ ∀𝑥 ∈ 𝐾 (◡𝐹 “ 𝑥) ∈ 𝐽))) |
4 | 3 | simprbi 497 | . 2 ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → (𝐹:𝑋⟶𝑌 ∧ ∀𝑥 ∈ 𝐾 (◡𝐹 “ 𝑥) ∈ 𝐽)) |
5 | 4 | simpld 495 | 1 ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹:𝑋⟶𝑌) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 = wceq 1528 ∈ wcel 2105 ∀wral 3135 ∪ cuni 4830 ◡ccnv 5547 “ cima 5551 ⟶wf 6344 (class class class)co 7145 Topctop 21429 Cn ccn 21760 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 ax-sep 5194 ax-nul 5201 ax-pow 5257 ax-pr 5320 ax-un 7450 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-mo 2615 df-eu 2647 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-ral 3140 df-rex 3141 df-rab 3144 df-v 3494 df-sbc 3770 df-dif 3936 df-un 3938 df-in 3940 df-ss 3949 df-nul 4289 df-if 4464 df-pw 4537 df-sn 4558 df-pr 4560 df-op 4564 df-uni 4831 df-br 5058 df-opab 5120 df-mpt 5138 df-id 5453 df-xp 5554 df-rel 5555 df-cnv 5556 df-co 5557 df-dm 5558 df-rn 5559 df-res 5560 df-ima 5561 df-iota 6307 df-fun 6350 df-fn 6351 df-f 6352 df-fv 6356 df-ov 7148 df-oprab 7149 df-mpo 7150 df-map 8397 df-top 21430 df-topon 21447 df-cn 21763 |
This theorem is referenced by: cnco 21802 cnclima 21804 cnntri 21807 cnclsi 21808 cnss1 21812 cnss2 21813 cncnpi 21814 cncnp2 21817 cnrest 21821 cnrest2 21822 cnt0 21882 cnt1 21886 cnhaus 21890 dnsconst 21914 cncmp 21928 rncmp 21932 imacmp 21933 cnconn 21958 connima 21961 conncn 21962 2ndcomap 21994 kgencn2 22093 kgencn3 22094 txcnmpt 22160 uptx 22161 txcn 22162 hauseqlcld 22182 xkohaus 22189 xkoptsub 22190 xkopjcn 22192 xkoco1cn 22193 xkoco2cn 22194 xkococnlem 22195 cnmpt11f 22200 cnmpt21f 22208 hmeocnv 22298 hmeores 22307 txhmeo 22339 cnextfres 22605 bndth 23489 evth 23490 evth2 23491 htpyco2 23510 phtpyco2 23521 reparphti 23528 copco 23549 pcopt 23553 pcopt2 23554 pcoass 23555 pcorevlem 23557 pcorev2 23559 hauseqcn 31037 pl1cn 31097 rrhf 31138 esumcocn 31238 cnmbfm 31420 cnpconn 32374 ptpconn 32377 sconnpi1 32383 txsconnlem 32384 cvxsconn 32387 cvmseu 32420 cvmopnlem 32422 cvmfolem 32423 cvmliftmolem1 32425 cvmliftmolem2 32426 cvmliftlem3 32431 cvmliftlem6 32434 cvmliftlem7 32435 cvmliftlem8 32436 cvmliftlem9 32437 cvmliftlem10 32438 cvmliftlem11 32439 cvmliftlem13 32440 cvmliftlem15 32442 cvmlift2lem3 32449 cvmlift2lem5 32451 cvmlift2lem7 32453 cvmlift2lem9 32455 cvmlift2lem10 32456 cvmliftphtlem 32461 cvmlift3lem1 32463 cvmlift3lem2 32464 cvmlift3lem4 32466 cvmlift3lem5 32467 cvmlift3lem6 32468 cvmlift3lem7 32469 cvmlift3lem8 32470 cvmlift3lem9 32471 poimirlem31 34804 poimir 34806 broucube 34807 cnres2 34922 cnresima 34923 hausgraph 39690 refsum2cnlem1 41171 itgsubsticclem 42136 stoweidlem62 42224 cnfsmf 42894 |
Copyright terms: Public domain | W3C validator |