![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > cnmpt1st | Structured version Unicode version |
Description: The projection onto the first coordinate is continuous. (Contributed by Mario Carneiro, 6-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.) |
Ref | Expression |
---|---|
cnmpt21.j |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
cnmpt21.k |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
cnmpt1st |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fo1st 6707 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | fofn 5731 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | ax-mp 5 |
. . . . 5
![]() ![]() ![]() ![]() |
4 | ssv 3485 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | fnssres 5633 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | 3, 4, 5 | mp2an 672 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | dffn5 5847 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
8 | 6, 7 | mpbi 208 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | fvres 5814 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
10 | 9 | mpteq2ia 4483 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
11 | vex 3081 |
. . . . 5
![]() ![]() ![]() ![]() | |
12 | vex 3081 |
. . . . 5
![]() ![]() ![]() ![]() | |
13 | 11, 12 | op1std 6698 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
14 | 13 | mpt2mpt 6293 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
15 | 8, 10, 14 | 3eqtri 2487 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
16 | cnmpt21.j |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
17 | cnmpt21.k |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
18 | tx1cn 19315 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
19 | 16, 17, 18 | syl2anc 661 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
20 | 15, 19 | syl5eqelr 2547 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-8 1760 ax-9 1762 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1955 ax-ext 2432 ax-sep 4522 ax-nul 4530 ax-pow 4579 ax-pr 4640 ax-un 6483 |
This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 967 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-eu 2266 df-mo 2267 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2604 df-ne 2650 df-ral 2804 df-rex 2805 df-rab 2808 df-v 3080 df-sbc 3295 df-csb 3397 df-dif 3440 df-un 3442 df-in 3444 df-ss 3451 df-nul 3747 df-if 3901 df-pw 3971 df-sn 3987 df-pr 3989 df-op 3993 df-uni 4201 df-iun 4282 df-br 4402 df-opab 4460 df-mpt 4461 df-id 4745 df-xp 4955 df-rel 4956 df-cnv 4957 df-co 4958 df-dm 4959 df-rn 4960 df-res 4961 df-ima 4962 df-iota 5490 df-fun 5529 df-fn 5530 df-f 5531 df-fo 5533 df-fv 5535 df-ov 6204 df-oprab 6205 df-mpt2 6206 df-1st 6688 df-2nd 6689 df-map 7327 df-topgen 14502 df-top 18636 df-bases 18638 df-topon 18639 df-cn 18964 df-tx 19268 |
This theorem is referenced by: cnmptcom 19384 xkofvcn 19390 cnmptk2 19392 txhmeo 19509 txswaphmeo 19511 ptunhmeo 19514 xkohmeo 19521 tgpsubcn 19794 istgp2 19795 oppgtmd 19801 prdstmdd 19827 dvrcn 19891 divcn 20577 cnrehmeo 20658 htpycom 20681 htpyid 20682 htpyco1 20683 htpycc 20685 reparphti 20702 pcocn 20722 pcohtpylem 20724 pcopt 20727 pcopt2 20728 pcoass 20729 pcorevlem 20731 cxpcn 22317 vmcn 24247 dipcn 24271 mndpluscn 26502 cvxscon 27277 cvmlift2lem12 27348 |
Copyright terms: Public domain | W3C validator |