Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  txcn Unicode version

Theorem txcn 17376
 Description: A map into the product of two topological spaces is continuous iff both of its projections are continuous. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 22-Aug-2015.)
Hypotheses
Ref Expression
txcn.1
txcn.2
txcn.3
txcn.4
txcn.5
txcn.6
Assertion
Ref Expression
txcn

Proof of Theorem txcn
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 txcn.1 . . . . 5
21toptopon 16727 . . . 4 TopOn
3 txcn.2 . . . . 5
43toptopon 16727 . . . 4 TopOn
5 txcn.5 . . . . . . 7
6 txcn.3 . . . . . . . 8
76reseq2i 4989 . . . . . . 7
85, 7eqtri 2336 . . . . . 6
9 tx1cn 17359 . . . . . 6 TopOn TopOn
108, 9syl5eqel 2400 . . . . 5 TopOn TopOn
11 txcn.6 . . . . . . 7
126reseq2i 4989 . . . . . . 7
1311, 12eqtri 2336 . . . . . 6
14 tx2cn 17360 . . . . . 6 TopOn TopOn
1513, 14syl5eqel 2400 . . . . 5 TopOn TopOn
16 cnco 17051 . . . . . . 7
17 cnco 17051 . . . . . . 7
1816, 17anim12dan 810 . . . . . 6
1918expcom 424 . . . . 5
2010, 15, 19syl2anc 642 . . . 4 TopOn TopOn
212, 4, 20syl2anb 465 . . 3
23 cntop1 17026 . . . . . . . 8
2423ad2antrl 708 . . . . . . 7
25 txcn.4 . . . . . . . 8
2625topopn 16708 . . . . . . 7
2724, 26syl 15 . . . . . 6
2825, 1cnf 17032 . . . . . . 7
2928ad2antrl 708 . . . . . 6
3025, 3cnf 17032 . . . . . . 7
3130ad2antll 709 . . . . . 6
328, 13upxp 17373 . . . . . . 7
33 feq3 5414 . . . . . . . . . 10
346, 33ax-mp 8 . . . . . . . . 9
35343anbi1i 1142 . . . . . . . 8
3635eubii 2185 . . . . . . 7
3732, 36sylibr 203 . . . . . 6
3827, 29, 31, 37syl3anc 1182 . . . . 5
39 euex 2199 . . . . 5
4038, 39syl 15 . . . 4
41 simpll3 996 . . . . . . . . 9
4227adantr 451 . . . . . . . . 9
431topopn 16708 . . . . . . . . . . . 12
443topopn 16708 . . . . . . . . . . . 12
45 xpexg 4837 . . . . . . . . . . . . 13
466, 45syl5eqel 2400 . . . . . . . . . . . 12
4743, 44, 46syl2an 463 . . . . . . . . . . 11
48473adant3 975 . . . . . . . . . 10
4948ad2antrr 706 . . . . . . . . 9
50 fex2 5439 . . . . . . . . 9
5141, 42, 49, 50syl3anc 1182 . . . . . . . 8
52 eumo 2216 . . . . . . . . . 10
5338, 52syl 15 . . . . . . . . 9
5453adantr 451 . . . . . . . 8
55 simpr 447 . . . . . . . 8
56 3anass 938 . . . . . . . . . 10
57 coeq2 4879 . . . . . . . . . . . . . 14
58 coeq2 4879 . . . . . . . . . . . . . 14
5957, 58jca 518 . . . . . . . . . . . . 13
6059eqcoms 2319 . . . . . . . . . . . 12
6160biantrud 493 . . . . . . . . . . 11
62 feq1 5412 . . . . . . . . . . 11
6361, 62bitr3d 246 . . . . . . . . . 10
6456, 63syl5bb 248 . . . . . . . . 9
6564moi2 2980 . . . . . . . 8
6651, 54, 55, 41, 65syl22anc 1183 . . . . . . 7
67 eqid 2316 . . . . . . . . . . . 12
6867, 1, 3, 6, 5, 11uptx 17375 . . . . . . . . . . 11
6968adantl 452 . . . . . . . . . 10
70 df-reu 2584 . . . . . . . . . . . 12
71 euex 2199 . . . . . . . . . . . 12
7270, 71sylbi 187 . . . . . . . . . . 11
73 eqid 2316 . . . . . . . . . . . . . . . . 17
7425, 73cnf 17032 . . . . . . . . . . . . . . . 16
751, 3txuni 17343 . . . . . . . . . . . . . . . . . . . 20
766, 75syl5eq 2360 . . . . . . . . . . . . . . . . . . 19
77763adant3 975 . . . . . . . . . . . . . . . . . 18
7877adantr 451 . . . . . . . . . . . . . . . . 17
79 feq3 5414 . . . . . . . . . . . . . . . . 17
8078, 79syl 15 . . . . . . . . . . . . . . . 16
8174, 80syl5ibr 212 . . . . . . . . . . . . . . 15
8281anim1d 547 . . . . . . . . . . . . . 14
8382, 56syl6ibr 218 . . . . . . . . . . . . 13
84 simpl 443 . . . . . . . . . . . . . 14
8584a1i 10 . . . . . . . . . . . . 13
8683, 85jcad 519 . . . . . . . . . . . 12
8786eximdv 1613 . . . . . . . . . . 11
8872, 87syl5 28 . . . . . . . . . 10
8969, 88mpd 14 . . . . . . . . 9
90 eupick 2239 . . . . . . . . 9
9138, 89, 90syl2anc 642 . . . . . . . 8
9291imp 418 . . . . . . 7
9366, 92eqeltrrd 2391 . . . . . 6
9493ex 423 . . . . 5
9594exlimdv 1627 . . . 4
9640, 95mpd 14 . . 3
9796ex 423 . 2
9822, 97impbid 183 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 176   wa 358   w3a 934  wex 1532   wceq 1633   wcel 1701  weu 2176  wmo 2177  wreu 2579  cvv 2822  cuni 3864   cxp 4724   cres 4728   ccom 4730  wf 5288  cfv 5292  (class class class)co 5900  c1st 6162  c2nd 6163  ctop 16687  TopOnctopon 16688   ccn 17010   ctx 17311 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-13 1703  ax-14 1705  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297  ax-rep 4168  ax-sep 4178  ax-nul 4186  ax-pow 4225  ax-pr 4251  ax-un 4549 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-eu 2180  df-mo 2181  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-ne 2481  df-ral 2582  df-rex 2583  df-reu 2584  df-rab 2586  df-v 2824  df-sbc 3026  df-csb 3116  df-dif 3189  df-un 3191  df-in 3193  df-ss 3200  df-nul 3490  df-if 3600  df-pw 3661  df-sn 3680  df-pr 3681  df-op 3683  df-uni 3865  df-iun 3944  df-br 4061  df-opab 4115  df-mpt 4116  df-id 4346  df-xp 4732  df-rel 4733  df-cnv 4734  df-co 4735  df-dm 4736  df-rn 4737  df-res 4738  df-ima 4739  df-iota 5256  df-fun 5294  df-fn 5295  df-f 5296  df-f1 5297  df-fo 5298  df-f1o 5299  df-fv 5300  df-ov 5903  df-oprab 5904  df-mpt2 5905  df-1st 6164  df-2nd 6165  df-map 6817  df-topgen 13393  df-top 16692  df-bases 16694  df-topon 16695  df-cn 17013  df-tx 17313
 Copyright terms: Public domain W3C validator