| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > cnmpt2nd | Structured version Visualization version GIF version | ||
| Description: The projection onto the second coordinate is continuous. (Contributed by Mario Carneiro, 6-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.) |
| Ref | Expression |
|---|---|
| cnmpt21.j | ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) |
| cnmpt21.k | ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) |
| Ref | Expression |
|---|---|
| cnmpt2nd | ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝑦) ∈ ((𝐽 ×t 𝐾) Cn 𝐾)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | fo2nd 7995 | . . . . . 6 ⊢ 2nd :V–onto→V | |
| 2 | fofn 6784 | . . . . . 6 ⊢ (2nd :V–onto→V → 2nd Fn V) | |
| 3 | 1, 2 | ax-mp 5 | . . . . 5 ⊢ 2nd Fn V |
| 4 | ssv 3963 | . . . . 5 ⊢ (𝑋 × 𝑌) ⊆ V | |
| 5 | fnssres 6648 | . . . . 5 ⊢ ((2nd Fn V ∧ (𝑋 × 𝑌) ⊆ V) → (2nd ↾ (𝑋 × 𝑌)) Fn (𝑋 × 𝑌)) | |
| 6 | 3, 4, 5 | mp2an 704 | . . . 4 ⊢ (2nd ↾ (𝑋 × 𝑌)) Fn (𝑋 × 𝑌) |
| 7 | dffn5 6929 | . . . 4 ⊢ ((2nd ↾ (𝑋 × 𝑌)) Fn (𝑋 × 𝑌) ↔ (2nd ↾ (𝑋 × 𝑌)) = (𝑧 ∈ (𝑋 × 𝑌) ↦ ((2nd ↾ (𝑋 × 𝑌))‘𝑧))) | |
| 8 | 6, 7 | mpbi 233 | . . 3 ⊢ (2nd ↾ (𝑋 × 𝑌)) = (𝑧 ∈ (𝑋 × 𝑌) ↦ ((2nd ↾ (𝑋 × 𝑌))‘𝑧)) |
| 9 | fvres 6890 | . . . 4 ⊢ (𝑧 ∈ (𝑋 × 𝑌) → ((2nd ↾ (𝑋 × 𝑌))‘𝑧) = (2nd ‘𝑧)) | |
| 10 | 9 | mpteq2ia 5200 | . . 3 ⊢ (𝑧 ∈ (𝑋 × 𝑌) ↦ ((2nd ↾ (𝑋 × 𝑌))‘𝑧)) = (𝑧 ∈ (𝑋 × 𝑌) ↦ (2nd ‘𝑧)) |
| 11 | vex 3461 | . . . . 5 ⊢ 𝑥 ∈ V | |
| 12 | vex 3461 | . . . . 5 ⊢ 𝑦 ∈ V | |
| 13 | 11, 12 | op2ndd 7985 | . . . 4 ⊢ (𝑧 = 〈𝑥, 𝑦〉 → (2nd ‘𝑧) = 𝑦) |
| 14 | 13 | mpompt 7514 | . . 3 ⊢ (𝑧 ∈ (𝑋 × 𝑌) ↦ (2nd ‘𝑧)) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝑦) |
| 15 | 8, 10, 14 | 3eqtri 2792 | . 2 ⊢ (2nd ↾ (𝑋 × 𝑌)) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝑦) |
| 16 | cnmpt21.j | . . 3 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) | |
| 17 | cnmpt21.k | . . 3 ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) | |
| 18 | tx2cn 23728 | . . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (2nd ↾ (𝑋 × 𝑌)) ∈ ((𝐽 ×t 𝐾) Cn 𝐾)) | |
| 19 | 16, 17, 18 | syl2anc 595 | . 2 ⊢ (𝜑 → (2nd ↾ (𝑋 × 𝑌)) ∈ ((𝐽 ×t 𝐾) Cn 𝐾)) |
| 20 | 15, 19 | eqeltrrid 2870 | 1 ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝑦) ∈ ((𝐽 ×t 𝐾) Cn 𝐾)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 = wceq 1563 ∈ wcel 2145 Vcvv 3457 ⊆ wss 3907 ↦ cmpt 5186 × cxp 5650 ↾ cres 5654 Fn wfn 6520 –onto→wfo 6523 ‘cfv 6525 (class class class)co 7400 ∈ cmpo 7402 2nd c2nd 7973 TopOnctopon 23028 Cn ccn 23342 ×t ctx 23678 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 ax-5 1933 ax-6 1990 ax-7 2031 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2737 ax-sep 5251 ax-nul 5261 ax-pow 5327 ax-pr 5395 ax-un 7722 |
| This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3an 1103 df-tru 1566 df-fal 1576 df-ex 1803 df-nf 1807 df-sb 2094 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-ral 3080 df-rex 3090 df-rab 3418 df-v 3459 df-sbc 3748 df-csb 3856 df-dif 3910 df-un 3912 df-in 3914 df-ss 3924 df-nul 4289 df-if 4484 df-pw 4560 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4869 df-iun 4954 df-br 5106 df-opab 5168 df-mpt 5187 df-id 5547 df-xp 5658 df-rel 5659 df-cnv 5660 df-co 5661 df-dm 5662 df-rn 5663 df-res 5664 df-ima 5665 df-iota 6481 df-fun 6527 df-fn 6528 df-f 6529 df-fo 6531 df-fv 6533 df-ov 7403 df-oprab 7404 df-mpo 7405 df-1st 7974 df-2nd 7975 df-map 8814 df-topgen 17486 df-top 23012 df-topon 23029 df-bases 23064 df-cn 23345 df-tx 23680 |
| This theorem is referenced by: cnmptcom 23796 xkofvcn 23802 cnmptk2 23804 txhmeo 23921 txswaphmeo 23923 ptunhmeo 23926 xkohmeo 23933 tgpsubcn 24208 istgp2 24209 oppgtmd 24215 prdstmdd 24242 dvrcn 24302 divcn 24988 cnrehmeo 25073 htpycom 25096 htpyco1 25098 htpycc 25100 reparphti 25117 pcohtpylem 25139 pcorevlem 25146 cxpcn 26868 vmcn 30960 dipcn 30981 mndpluscn 34233 cvxsconn 35606 cvmlift2lem6 35671 |
| Copyright terms: Public domain | W3C validator |