![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > cnmptid | Structured version Visualization version GIF version |
Description: The identity function is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.) |
Ref | Expression |
---|---|
cnmptid.j | ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) |
Ref | Expression |
---|---|
cnmptid | ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝑥) ∈ (𝐽 Cn 𝐽)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | equcom 2065 | . . . . . 6 ⊢ (𝑥 = 𝑦 ↔ 𝑦 = 𝑥) | |
2 | 1 | opabbii 4953 | . . . . 5 ⊢ {〈𝑥, 𝑦〉 ∣ 𝑥 = 𝑦} = {〈𝑥, 𝑦〉 ∣ 𝑦 = 𝑥} |
3 | df-id 5261 | . . . . 5 ⊢ I = {〈𝑥, 𝑦〉 ∣ 𝑥 = 𝑦} | |
4 | mptv 4986 | . . . . 5 ⊢ (𝑥 ∈ V ↦ 𝑥) = {〈𝑥, 𝑦〉 ∣ 𝑦 = 𝑥} | |
5 | 2, 3, 4 | 3eqtr4i 2812 | . . . 4 ⊢ I = (𝑥 ∈ V ↦ 𝑥) |
6 | 5 | reseq1i 5638 | . . 3 ⊢ ( I ↾ 𝑋) = ((𝑥 ∈ V ↦ 𝑥) ↾ 𝑋) |
7 | ssv 3844 | . . . 4 ⊢ 𝑋 ⊆ V | |
8 | resmpt 5699 | . . . 4 ⊢ (𝑋 ⊆ V → ((𝑥 ∈ V ↦ 𝑥) ↾ 𝑋) = (𝑥 ∈ 𝑋 ↦ 𝑥)) | |
9 | 7, 8 | ax-mp 5 | . . 3 ⊢ ((𝑥 ∈ V ↦ 𝑥) ↾ 𝑋) = (𝑥 ∈ 𝑋 ↦ 𝑥) |
10 | 6, 9 | eqtri 2802 | . 2 ⊢ ( I ↾ 𝑋) = (𝑥 ∈ 𝑋 ↦ 𝑥) |
11 | cnmptid.j | . . 3 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) | |
12 | idcn 21469 | . . 3 ⊢ (𝐽 ∈ (TopOn‘𝑋) → ( I ↾ 𝑋) ∈ (𝐽 Cn 𝐽)) | |
13 | 11, 12 | syl 17 | . 2 ⊢ (𝜑 → ( I ↾ 𝑋) ∈ (𝐽 Cn 𝐽)) |
14 | 10, 13 | syl5eqelr 2864 | 1 ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝑥) ∈ (𝐽 Cn 𝐽)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1601 ∈ wcel 2107 Vcvv 3398 ⊆ wss 3792 {copab 4948 ↦ cmpt 4965 I cid 5260 ↾ cres 5357 ‘cfv 6135 (class class class)co 6922 TopOnctopon 21122 Cn ccn 21436 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-8 2109 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-13 2334 ax-ext 2754 ax-sep 5017 ax-nul 5025 ax-pow 5077 ax-pr 5138 ax-un 7226 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-3an 1073 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-mo 2551 df-eu 2587 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-ral 3095 df-rex 3096 df-rab 3099 df-v 3400 df-sbc 3653 df-dif 3795 df-un 3797 df-in 3799 df-ss 3806 df-nul 4142 df-if 4308 df-pw 4381 df-sn 4399 df-pr 4401 df-op 4405 df-uni 4672 df-br 4887 df-opab 4949 df-mpt 4966 df-id 5261 df-xp 5361 df-rel 5362 df-cnv 5363 df-co 5364 df-dm 5365 df-rn 5366 df-res 5367 df-ima 5368 df-iota 6099 df-fun 6137 df-fn 6138 df-f 6139 df-f1 6140 df-fo 6141 df-f1o 6142 df-fv 6143 df-ov 6925 df-oprab 6926 df-mpt2 6927 df-map 8142 df-top 21106 df-topon 21123 df-cn 21439 |
This theorem is referenced by: xkoinjcn 21899 txconn 21901 imasnopn 21902 imasncld 21903 imasncls 21904 pt1hmeo 22018 istgp2 22303 tmdmulg 22304 tmdlactcn 22314 clsnsg 22321 tgpt0 22330 tlmtgp 22407 nmcn 23055 expcn 23083 divccn 23084 cncfmptid 23123 cdivcncf 23128 iirevcn 23137 iihalf1cn 23139 iihalf2cn 23141 icchmeo 23148 evth2 23167 pcocn 23224 pcopt 23229 pcopt2 23230 pcoass 23231 csscld 23455 clsocv 23456 dvcnvlem 24176 resqrtcn 24930 sqrtcn 24931 efrlim 25148 ipasslem7 28263 occllem 28734 hmopidmchi 29582 rmulccn 30572 cxpcncf1 31275 cvxpconn 31823 cvmlift2lem2 31885 cvmlift2lem3 31886 cvmliftphtlem 31898 knoppcnlem10 33075 cxpcncf2 41041 |
Copyright terms: Public domain | W3C validator |