| 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 5199 | . . 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 23724 | . . 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 5185 × cxp 5649 ↾ cres 5653 Fn wfn 6520 –onto→wfo 6523 ‘cfv 6525 (class class class)co 7400 ∈ cmpo 7402 2nd c2nd 7973 TopOnctopon 23024 Cn ccn 23338 ×t ctx 23674 |
| 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 5250 ax-nul 5260 ax-pow 5326 ax-pr 5394 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 4868 df-iun 4953 df-br 5105 df-opab 5167 df-mpt 5186 df-id 5546 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 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 17484 df-top 23008 df-topon 23025 df-bases 23060 df-cn 23341 df-tx 23676 |
| This theorem is referenced by: cnmptcom 23792 xkofvcn 23798 cnmptk2 23800 txhmeo 23917 txswaphmeo 23919 ptunhmeo 23922 xkohmeo 23929 tgpsubcn 24204 istgp2 24205 oppgtmd 24211 prdstmdd 24238 dvrcn 24298 divcn 24984 cnrehmeo 25069 htpycom 25092 htpyco1 25094 htpycc 25096 reparphti 25113 pcohtpylem 25135 pcorevlem 25142 cxpcn 26864 vmcn 30956 dipcn 30977 mndpluscn 34228 cvxsconn 35601 cvmlift2lem6 35666 |
| Copyright terms: Public domain | W3C validator |