![]() |
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 8008 | . . . . . 6 ⊢ 2nd :V–onto→V | |
2 | fofn 6807 | . . . . . 6 ⊢ (2nd :V–onto→V → 2nd Fn V) | |
3 | 1, 2 | ax-mp 5 | . . . . 5 ⊢ 2nd Fn V |
4 | ssv 4002 | . . . . 5 ⊢ (𝑋 × 𝑌) ⊆ V | |
5 | fnssres 6672 | . . . . 5 ⊢ ((2nd Fn V ∧ (𝑋 × 𝑌) ⊆ V) → (2nd ↾ (𝑋 × 𝑌)) Fn (𝑋 × 𝑌)) | |
6 | 3, 4, 5 | mp2an 691 | . . . 4 ⊢ (2nd ↾ (𝑋 × 𝑌)) Fn (𝑋 × 𝑌) |
7 | dffn5 6951 | . . . 4 ⊢ ((2nd ↾ (𝑋 × 𝑌)) Fn (𝑋 × 𝑌) ↔ (2nd ↾ (𝑋 × 𝑌)) = (𝑧 ∈ (𝑋 × 𝑌) ↦ ((2nd ↾ (𝑋 × 𝑌))‘𝑧))) | |
8 | 6, 7 | mpbi 229 | . . 3 ⊢ (2nd ↾ (𝑋 × 𝑌)) = (𝑧 ∈ (𝑋 × 𝑌) ↦ ((2nd ↾ (𝑋 × 𝑌))‘𝑧)) |
9 | fvres 6910 | . . . 4 ⊢ (𝑧 ∈ (𝑋 × 𝑌) → ((2nd ↾ (𝑋 × 𝑌))‘𝑧) = (2nd ‘𝑧)) | |
10 | 9 | mpteq2ia 5245 | . . 3 ⊢ (𝑧 ∈ (𝑋 × 𝑌) ↦ ((2nd ↾ (𝑋 × 𝑌))‘𝑧)) = (𝑧 ∈ (𝑋 × 𝑌) ↦ (2nd ‘𝑧)) |
11 | vex 3473 | . . . . 5 ⊢ 𝑥 ∈ V | |
12 | vex 3473 | . . . . 5 ⊢ 𝑦 ∈ V | |
13 | 11, 12 | op2ndd 7998 | . . . 4 ⊢ (𝑧 = 〈𝑥, 𝑦〉 → (2nd ‘𝑧) = 𝑦) |
14 | 13 | mpompt 7528 | . . 3 ⊢ (𝑧 ∈ (𝑋 × 𝑌) ↦ (2nd ‘𝑧)) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝑦) |
15 | 8, 10, 14 | 3eqtri 2759 | . 2 ⊢ (2nd ↾ (𝑋 × 𝑌)) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝑦) |
16 | cnmpt21.j | . . 3 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) | |
17 | cnmpt21.k | . . 3 ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) | |
18 | tx2cn 23501 | . . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (2nd ↾ (𝑋 × 𝑌)) ∈ ((𝐽 ×t 𝐾) Cn 𝐾)) | |
19 | 16, 17, 18 | syl2anc 583 | . 2 ⊢ (𝜑 → (2nd ↾ (𝑋 × 𝑌)) ∈ ((𝐽 ×t 𝐾) Cn 𝐾)) |
20 | 15, 19 | eqeltrrid 2833 | 1 ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝑦) ∈ ((𝐽 ×t 𝐾) Cn 𝐾)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1534 ∈ wcel 2099 Vcvv 3469 ⊆ wss 3944 ↦ cmpt 5225 × cxp 5670 ↾ cres 5674 Fn wfn 6537 –onto→wfo 6540 ‘cfv 6542 (class class class)co 7414 ∈ cmpo 7416 2nd c2nd 7986 TopOnctopon 22799 Cn ccn 23115 ×t ctx 23451 |
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 2164 ax-ext 2698 ax-sep 5293 ax-nul 5300 ax-pow 5359 ax-pr 5423 ax-un 7734 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 847 df-3an 1087 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2529 df-eu 2558 df-clab 2705 df-cleq 2719 df-clel 2805 df-nfc 2880 df-ne 2936 df-ral 3057 df-rex 3066 df-rab 3428 df-v 3471 df-sbc 3775 df-csb 3890 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-nul 4319 df-if 4525 df-pw 4600 df-sn 4625 df-pr 4627 df-op 4631 df-uni 4904 df-iun 4993 df-br 5143 df-opab 5205 df-mpt 5226 df-id 5570 df-xp 5678 df-rel 5679 df-cnv 5680 df-co 5681 df-dm 5682 df-rn 5683 df-res 5684 df-ima 5685 df-iota 6494 df-fun 6544 df-fn 6545 df-f 6546 df-fo 6548 df-fv 6550 df-ov 7417 df-oprab 7418 df-mpo 7419 df-1st 7987 df-2nd 7988 df-map 8838 df-topgen 17416 df-top 22783 df-topon 22800 df-bases 22836 df-cn 23118 df-tx 23453 |
This theorem is referenced by: cnmptcom 23569 xkofvcn 23575 cnmptk2 23577 txhmeo 23694 txswaphmeo 23696 ptunhmeo 23699 xkohmeo 23706 tgpsubcn 23981 istgp2 23982 oppgtmd 23988 prdstmdd 24015 dvrcn 24075 divcnOLD 24771 divcn 24773 cnrehmeo 24865 cnrehmeoOLD 24866 htpycom 24889 htpyco1 24891 htpycc 24893 reparphti 24910 reparphtiOLD 24911 pcohtpylem 24933 pcorevlem 24940 cxpcn 26666 cxpcnOLD 26667 vmcn 30496 dipcn 30517 mndpluscn 33463 cvxsconn 34789 cvmlift2lem6 34854 |
Copyright terms: Public domain | W3C validator |