![]() |
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 7943 | . . . . . 6 β’ 2nd :VβontoβV | |
2 | fofn 6759 | . . . . . 6 β’ (2nd :VβontoβV β 2nd Fn V) | |
3 | 1, 2 | ax-mp 5 | . . . . 5 β’ 2nd Fn V |
4 | ssv 3969 | . . . . 5 β’ (π Γ π) β V | |
5 | fnssres 6625 | . . . . 5 β’ ((2nd Fn V β§ (π Γ π) β V) β (2nd βΎ (π Γ π)) Fn (π Γ π)) | |
6 | 3, 4, 5 | mp2an 691 | . . . 4 β’ (2nd βΎ (π Γ π)) Fn (π Γ π) |
7 | dffn5 6902 | . . . 4 β’ ((2nd βΎ (π Γ π)) Fn (π Γ π) β (2nd βΎ (π Γ π)) = (π§ β (π Γ π) β¦ ((2nd βΎ (π Γ π))βπ§))) | |
8 | 6, 7 | mpbi 229 | . . 3 β’ (2nd βΎ (π Γ π)) = (π§ β (π Γ π) β¦ ((2nd βΎ (π Γ π))βπ§)) |
9 | fvres 6862 | . . . 4 β’ (π§ β (π Γ π) β ((2nd βΎ (π Γ π))βπ§) = (2nd βπ§)) | |
10 | 9 | mpteq2ia 5209 | . . 3 β’ (π§ β (π Γ π) β¦ ((2nd βΎ (π Γ π))βπ§)) = (π§ β (π Γ π) β¦ (2nd βπ§)) |
11 | vex 3448 | . . . . 5 β’ π₯ β V | |
12 | vex 3448 | . . . . 5 β’ π¦ β V | |
13 | 11, 12 | op2ndd 7933 | . . . 4 β’ (π§ = β¨π₯, π¦β© β (2nd βπ§) = π¦) |
14 | 13 | mpompt 7471 | . . 3 β’ (π§ β (π Γ π) β¦ (2nd βπ§)) = (π₯ β π, π¦ β π β¦ π¦) |
15 | 8, 10, 14 | 3eqtri 2765 | . 2 β’ (2nd βΎ (π Γ π)) = (π₯ β π, π¦ β π β¦ π¦) |
16 | cnmpt21.j | . . 3 β’ (π β π½ β (TopOnβπ)) | |
17 | cnmpt21.k | . . 3 β’ (π β πΎ β (TopOnβπ)) | |
18 | tx2cn 22977 | . . 3 β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β (2nd βΎ (π Γ π)) β ((π½ Γt πΎ) Cn πΎ)) | |
19 | 16, 17, 18 | syl2anc 585 | . 2 β’ (π β (2nd βΎ (π Γ π)) β ((π½ Γt πΎ) Cn πΎ)) |
20 | 15, 19 | eqeltrrid 2839 | 1 β’ (π β (π₯ β π, π¦ β π β¦ π¦) β ((π½ Γt πΎ) Cn πΎ)) |
Colors of variables: wff setvar class |
Syntax hints: β wi 4 = wceq 1542 β wcel 2107 Vcvv 3444 β wss 3911 β¦ cmpt 5189 Γ cxp 5632 βΎ cres 5636 Fn wfn 6492 βontoβwfo 6495 βcfv 6497 (class class class)co 7358 β cmpo 7360 2nd c2nd 7921 TopOnctopon 22275 Cn ccn 22591 Γt ctx 22927 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-sep 5257 ax-nul 5264 ax-pow 5321 ax-pr 5385 ax-un 7673 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2941 df-ral 3062 df-rex 3071 df-rab 3407 df-v 3446 df-sbc 3741 df-csb 3857 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-nul 4284 df-if 4488 df-pw 4563 df-sn 4588 df-pr 4590 df-op 4594 df-uni 4867 df-iun 4957 df-br 5107 df-opab 5169 df-mpt 5190 df-id 5532 df-xp 5640 df-rel 5641 df-cnv 5642 df-co 5643 df-dm 5644 df-rn 5645 df-res 5646 df-ima 5647 df-iota 6449 df-fun 6499 df-fn 6500 df-f 6501 df-fo 6503 df-fv 6505 df-ov 7361 df-oprab 7362 df-mpo 7363 df-1st 7922 df-2nd 7923 df-map 8770 df-topgen 17330 df-top 22259 df-topon 22276 df-bases 22312 df-cn 22594 df-tx 22929 |
This theorem is referenced by: cnmptcom 23045 xkofvcn 23051 cnmptk2 23053 txhmeo 23170 txswaphmeo 23172 ptunhmeo 23175 xkohmeo 23182 tgpsubcn 23457 istgp2 23458 oppgtmd 23464 prdstmdd 23491 dvrcn 23551 divcn 24247 cnrehmeo 24332 htpycom 24355 htpyco1 24357 htpycc 24359 reparphti 24376 pcohtpylem 24398 pcorevlem 24405 cxpcn 26114 vmcn 29683 dipcn 29704 mndpluscn 32564 cvxsconn 33894 cvmlift2lem6 33959 |
Copyright terms: Public domain | W3C validator |