![]() |
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 8022 | . . . . . 6 β’ 2nd :VβontoβV | |
2 | fofn 6818 | . . . . . 6 β’ (2nd :VβontoβV β 2nd Fn V) | |
3 | 1, 2 | ax-mp 5 | . . . . 5 β’ 2nd Fn V |
4 | ssv 4006 | . . . . 5 β’ (π Γ π) β V | |
5 | fnssres 6683 | . . . . 5 β’ ((2nd Fn V β§ (π Γ π) β V) β (2nd βΎ (π Γ π)) Fn (π Γ π)) | |
6 | 3, 4, 5 | mp2an 690 | . . . 4 β’ (2nd βΎ (π Γ π)) Fn (π Γ π) |
7 | dffn5 6962 | . . . 4 β’ ((2nd βΎ (π Γ π)) Fn (π Γ π) β (2nd βΎ (π Γ π)) = (π§ β (π Γ π) β¦ ((2nd βΎ (π Γ π))βπ§))) | |
8 | 6, 7 | mpbi 229 | . . 3 β’ (2nd βΎ (π Γ π)) = (π§ β (π Γ π) β¦ ((2nd βΎ (π Γ π))βπ§)) |
9 | fvres 6921 | . . . 4 β’ (π§ β (π Γ π) β ((2nd βΎ (π Γ π))βπ§) = (2nd βπ§)) | |
10 | 9 | mpteq2ia 5255 | . . 3 β’ (π§ β (π Γ π) β¦ ((2nd βΎ (π Γ π))βπ§)) = (π§ β (π Γ π) β¦ (2nd βπ§)) |
11 | vex 3477 | . . . . 5 β’ π₯ β V | |
12 | vex 3477 | . . . . 5 β’ π¦ β V | |
13 | 11, 12 | op2ndd 8012 | . . . 4 β’ (π§ = β¨π₯, π¦β© β (2nd βπ§) = π¦) |
14 | 13 | mpompt 7541 | . . 3 β’ (π§ β (π Γ π) β¦ (2nd βπ§)) = (π₯ β π, π¦ β π β¦ π¦) |
15 | 8, 10, 14 | 3eqtri 2760 | . 2 β’ (2nd βΎ (π Γ π)) = (π₯ β π, π¦ β π β¦ π¦) |
16 | cnmpt21.j | . . 3 β’ (π β π½ β (TopOnβπ)) | |
17 | cnmpt21.k | . . 3 β’ (π β πΎ β (TopOnβπ)) | |
18 | tx2cn 23542 | . . 3 β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β (2nd βΎ (π Γ π)) β ((π½ Γt πΎ) Cn πΎ)) | |
19 | 16, 17, 18 | syl2anc 582 | . 2 β’ (π β (2nd βΎ (π Γ π)) β ((π½ Γt πΎ) Cn πΎ)) |
20 | 15, 19 | eqeltrrid 2834 | 1 β’ (π β (π₯ β π, π¦ β π β¦ π¦) β ((π½ Γt πΎ) Cn πΎ)) |
Colors of variables: wff setvar class |
Syntax hints: β wi 4 = wceq 1533 β wcel 2098 Vcvv 3473 β wss 3949 β¦ cmpt 5235 Γ cxp 5680 βΎ cres 5684 Fn wfn 6548 βontoβwfo 6551 βcfv 6553 (class class class)co 7426 β cmpo 7428 2nd c2nd 8000 TopOnctopon 22840 Cn ccn 23156 Γt ctx 23492 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2166 ax-ext 2699 ax-sep 5303 ax-nul 5310 ax-pow 5369 ax-pr 5433 ax-un 7748 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2529 df-eu 2558 df-clab 2706 df-cleq 2720 df-clel 2806 df-nfc 2881 df-ne 2938 df-ral 3059 df-rex 3068 df-rab 3431 df-v 3475 df-sbc 3779 df-csb 3895 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-nul 4327 df-if 4533 df-pw 4608 df-sn 4633 df-pr 4635 df-op 4639 df-uni 4913 df-iun 5002 df-br 5153 df-opab 5215 df-mpt 5236 df-id 5580 df-xp 5688 df-rel 5689 df-cnv 5690 df-co 5691 df-dm 5692 df-rn 5693 df-res 5694 df-ima 5695 df-iota 6505 df-fun 6555 df-fn 6556 df-f 6557 df-fo 6559 df-fv 6561 df-ov 7429 df-oprab 7430 df-mpo 7431 df-1st 8001 df-2nd 8002 df-map 8855 df-topgen 17434 df-top 22824 df-topon 22841 df-bases 22877 df-cn 23159 df-tx 23494 |
This theorem is referenced by: cnmptcom 23610 xkofvcn 23616 cnmptk2 23618 txhmeo 23735 txswaphmeo 23737 ptunhmeo 23740 xkohmeo 23747 tgpsubcn 24022 istgp2 24023 oppgtmd 24029 prdstmdd 24056 dvrcn 24116 divcnOLD 24812 divcn 24814 cnrehmeo 24906 cnrehmeoOLD 24907 htpycom 24930 htpyco1 24932 htpycc 24934 reparphti 24951 reparphtiOLD 24952 pcohtpylem 24974 pcorevlem 24981 cxpcn 26707 cxpcnOLD 26708 vmcn 30537 dipcn 30558 mndpluscn 33568 cvxsconn 34894 cvmlift2lem6 34959 |
Copyright terms: Public domain | W3C validator |