Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  txcnmpt Unicode version

Theorem txcnmpt 12644
 Description: A map into the product of two topological spaces is continuous if both of its projections are continuous. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 22-Aug-2015.)
Hypotheses
Ref Expression
txcnmpt.1
txcnmpt.2
Assertion
Ref Expression
txcnmpt
Distinct variable groups:   ,   ,   ,   ,   ,   ,
Allowed substitution hint:   ()

Proof of Theorem txcnmpt
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 txcnmpt.1 . . . . . . 7
2 eqid 2157 . . . . . . 7
31, 2cnf 12575 . . . . . 6
43adantr 274 . . . . 5
54ffvelrnda 5601 . . . 4
6 eqid 2157 . . . . . . 7
71, 6cnf 12575 . . . . . 6
87adantl 275 . . . . 5
98ffvelrnda 5601 . . . 4
105, 9opelxpd 4618 . . 3
11 txcnmpt.2 . . 3
1210, 11fmptd 5620 . 2
1311mptpreima 5078 . . . . . 6
144adantr 274 . . . . . . . . . . . . 13
1514adantr 274 . . . . . . . . . . . 12
16 ffn 5318 . . . . . . . . . . . 12
17 elpreima 5585 . . . . . . . . . . . 12
1815, 16, 173syl 17 . . . . . . . . . . 11
19 ibar 299 . . . . . . . . . . . 12
2019adantl 275 . . . . . . . . . . 11
2118, 20bitr4d 190 . . . . . . . . . 10
228ad2antrr 480 . . . . . . . . . . . 12
23 ffn 5318 . . . . . . . . . . . 12
24 elpreima 5585 . . . . . . . . . . . 12
2522, 23, 243syl 17 . . . . . . . . . . 11
26 ibar 299 . . . . . . . . . . . 12
2726adantl 275 . . . . . . . . . . 11
2825, 27bitr4d 190 . . . . . . . . . 10
2921, 28anbi12d 465 . . . . . . . . 9
30 elin 3290 . . . . . . . . 9
31 opelxp 4615 . . . . . . . . 9
3229, 30, 313bitr4g 222 . . . . . . . 8
3332rabbi2dva 3315 . . . . . . 7
34 inss1 3327 . . . . . . . . . 10
35 cnvimass 4948 . . . . . . . . . 10
3634, 35sstri 3137 . . . . . . . . 9
3736, 14fssdm 5333 . . . . . . . 8
38 sseqin2 3326 . . . . . . . 8
3937, 38sylib 121 . . . . . . 7
4033, 39eqtr3d 2192 . . . . . 6
4113, 40syl5eq 2202 . . . . 5
42 cntop1 12572 . . . . . . . 8
4342adantl 275 . . . . . . 7
4443adantr 274 . . . . . 6
45 cnima 12591 . . . . . . 7
4645ad2ant2r 501 . . . . . 6
47 cnima 12591 . . . . . . 7
4847ad2ant2l 500 . . . . . 6
49 inopn 12372 . . . . . 6
5044, 46, 48, 49syl3anc 1220 . . . . 5
5141, 50eqeltrd 2234 . . . 4
5251ralrimivva 2539 . . 3
53 vex 2715 . . . . . 6
54 vex 2715 . . . . . 6
5553, 54xpex 4700 . . . . 5
5655rgen2w 2513 . . . 4
57 eqid 2157 . . . . 5
58 imaeq2 4923 . . . . . 6
5958eleq1d 2226 . . . . 5
6057, 59ralrnmpo 5932 . . . 4
6156, 60ax-mp 5 . . 3
6252, 61sylibr 133 . 2
631toptopon 12387 . . . 4 TopOn
6443, 63sylib 121 . . 3 TopOn
65 cntop2 12573 . . . 4
66 cntop2 12573 . . . 4
67 eqid 2157 . . . . 5
6867txval 12626 . . . 4
6965, 66, 68syl2an 287 . . 3
70 toptopon2 12388 . . . . 5 TopOn
7165, 70sylib 121 . . . 4 TopOn
72 toptopon2 12388 . . . . 5 TopOn
7366, 72sylib 121 . . . 4 TopOn
74 txtopon 12633 . . . 4 TopOn TopOn TopOn
7571, 73, 74syl2an 287 . . 3 TopOn
7664, 69, 75tgcn 12579 . 2
7712, 62, 76mpbir2and 929 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 103   wb 104   wceq 1335   wcel 2128  wral 2435  crab 2439  cvv 2712   cin 3101   wss 3102  cop 3563  cuni 3772   cmpt 4025   cxp 4583  ccnv 4584   cdm 4585   crn 4586  cima 4588   wfn 5164  wf 5165  cfv 5169  (class class class)co 5821   cmpo 5823  ctg 12337  ctop 12366  TopOnctopon 12379   ccn 12556   ctx 12623 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-13 2130  ax-14 2131  ax-ext 2139  ax-coll 4079  ax-sep 4082  ax-pow 4135  ax-pr 4169  ax-un 4393  ax-setind 4495 This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1338  df-fal 1341  df-nf 1441  df-sb 1743  df-eu 2009  df-mo 2010  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ne 2328  df-ral 2440  df-rex 2441  df-reu 2442  df-rab 2444  df-v 2714  df-sbc 2938  df-csb 3032  df-dif 3104  df-un 3106  df-in 3108  df-ss 3115  df-nul 3395  df-pw 3545  df-sn 3566  df-pr 3567  df-op 3569  df-uni 3773  df-iun 3851  df-br 3966  df-opab 4026  df-mpt 4027  df-id 4253  df-xp 4591  df-rel 4592  df-cnv 4593  df-co 4594  df-dm 4595  df-rn 4596  df-res 4597  df-ima 4598  df-iota 5134  df-fun 5171  df-fn 5172  df-f 5173  df-f1 5174  df-fo 5175  df-f1o 5176  df-fv 5177  df-ov 5824  df-oprab 5825  df-mpo 5826  df-1st 6085  df-2nd 6086  df-map 6592  df-topgen 12343  df-top 12367  df-topon 12380  df-bases 12412  df-cn 12559  df-tx 12624 This theorem is referenced by:  uptx  12645  cnmpt1t  12656  cnmpt2t  12664
 Copyright terms: Public domain W3C validator