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

Theorem txcn 20634
 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 19941 . . . 4 TopOn
3 txcn.2 . . . . 5
43toptopon 19941 . . . 4 TopOn
5 txcn.5 . . . . . . 7
6 txcn.3 . . . . . . . 8
76reseq2i 5101 . . . . . . 7
85, 7eqtri 2472 . . . . . 6
9 tx1cn 20617 . . . . . 6 TopOn TopOn
108, 9syl5eqel 2532 . . . . 5 TopOn TopOn
11 txcn.6 . . . . . . 7
126reseq2i 5101 . . . . . . 7
1311, 12eqtri 2472 . . . . . 6
14 tx2cn 20618 . . . . . 6 TopOn TopOn
1513, 14syl5eqel 2532 . . . . 5 TopOn TopOn
16 cnco 20275 . . . . . . 7
17 cnco 20275 . . . . . . 7
1816, 17anim12dan 847 . . . . . 6
1918expcom 437 . . . . 5
2010, 15, 19syl2anc 666 . . . 4 TopOn TopOn
212, 4, 20syl2anb 482 . . 3
22213adant3 1027 . 2
23 cntop1 20249 . . . . . . . 8
2423ad2antrl 733 . . . . . . 7
25 txcn.4 . . . . . . . 8
2625topopn 19929 . . . . . . 7
2724, 26syl 17 . . . . . 6
2825, 1cnf 20255 . . . . . . 7
2928ad2antrl 733 . . . . . 6
3025, 3cnf 20255 . . . . . . 7
3130ad2antll 734 . . . . . 6
328, 13upxp 20631 . . . . . . 7
33 feq3 5710 . . . . . . . . . 10
346, 33ax-mp 5 . . . . . . . . 9
35343anbi1i 1198 . . . . . . . 8
3635eubii 2320 . . . . . . 7
3732, 36sylibr 216 . . . . . 6
3827, 29, 31, 37syl3anc 1267 . . . . 5
39 euex 2322 . . . . 5
4038, 39syl 17 . . . 4
41 simpll3 1048 . . . . . . 7
4227adantr 467 . . . . . . 7
431topopn 19929 . . . . . . . . . 10
443topopn 19929 . . . . . . . . . 10
45 xpexg 6590 . . . . . . . . . . 11
466, 45syl5eqel 2532 . . . . . . . . . 10
4743, 44, 46syl2an 480 . . . . . . . . 9
48473adant3 1027 . . . . . . . 8
4948ad2antrr 731 . . . . . . 7
50 fex2 6745 . . . . . . 7
5141, 42, 49, 50syl3anc 1267 . . . . . 6
52 eumo 2327 . . . . . . . 8
5338, 52syl 17 . . . . . . 7
5453adantr 467 . . . . . 6
55 simpr 463 . . . . . 6
56 3anass 988 . . . . . . . 8
57 coeq2 4992 . . . . . . . . . . . 12
58 coeq2 4992 . . . . . . . . . . . 12
5957, 58jca 535 . . . . . . . . . . 11
6059eqcoms 2458 . . . . . . . . . 10
6160biantrud 510 . . . . . . . . 9
62 feq1 5708 . . . . . . . . 9
6361, 62bitr3d 259 . . . . . . . 8
6456, 63syl5bb 261 . . . . . . 7
6564moi2 3218 . . . . . 6
6651, 54, 55, 41, 65syl22anc 1268 . . . . 5
67 eqid 2450 . . . . . . . . . 10
6867, 1, 3, 6, 5, 11uptx 20633 . . . . . . . . 9
6968adantl 468 . . . . . . . 8
70 df-reu 2743 . . . . . . . . . 10
71 euex 2322 . . . . . . . . . 10
7270, 71sylbi 199 . . . . . . . . 9
73 eqid 2450 . . . . . . . . . . . . . . 15
7425, 73cnf 20255 . . . . . . . . . . . . . 14
751, 3txuni 20600 . . . . . . . . . . . . . . . . . 18
766, 75syl5eq 2496 . . . . . . . . . . . . . . . . 17
77763adant3 1027 . . . . . . . . . . . . . . . 16
7877adantr 467 . . . . . . . . . . . . . . 15
7978feq3d 5714 . . . . . . . . . . . . . 14
8074, 79syl5ibr 225 . . . . . . . . . . . . 13
8180anim1d 567 . . . . . . . . . . . 12
8281, 56syl6ibr 231 . . . . . . . . . . 11
83 simpl 459 . . . . . . . . . . . 12
8483a1i 11 . . . . . . . . . . 11
8582, 84jcad 536 . . . . . . . . . 10
8685eximdv 1763 . . . . . . . . 9
8772, 86syl5 33 . . . . . . . 8
8869, 87mpd 15 . . . . . . 7
89 eupick 2364 . . . . . . 7
9038, 88, 89syl2anc 666 . . . . . 6
9190imp 431 . . . . 5
9266, 91eqeltrrd 2529 . . . 4
9340, 92exlimddv 1780 . . 3
9493ex 436 . 2
9522, 94impbid 194 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 188   wa 371   w3a 984   wceq 1443  wex 1662   wcel 1886  weu 2298  wmo 2299  wreu 2738  cvv 3044  cuni 4197   cxp 4831   cres 4835   ccom 4837  wf 5577  cfv 5581  (class class class)co 6288  c1st 6788  c2nd 6789  ctop 19910  TopOnctopon 19911   ccn 20233   ctx 20568 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-8 1888  ax-9 1895  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-rep 4514  ax-sep 4524  ax-nul 4533  ax-pow 4580  ax-pr 4638  ax-un 6580 This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 986  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-eu 2302  df-mo 2303  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-ral 2741  df-rex 2742  df-reu 2743  df-rab 2745  df-v 3046  df-sbc 3267  df-csb 3363  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-nul 3731  df-if 3881  df-pw 3952  df-sn 3968  df-pr 3970  df-op 3974  df-uni 4198  df-iun 4279  df-br 4402  df-opab 4461  df-mpt 4462  df-id 4748  df-xp 4839  df-rel 4840  df-cnv 4841  df-co 4842  df-dm 4843  df-rn 4844  df-res 4845  df-ima 4846  df-iota 5545  df-fun 5583  df-fn 5584  df-f 5585  df-f1 5586  df-fo 5587  df-f1o 5588  df-fv 5589  df-ov 6291  df-oprab 6292  df-mpt2 6293  df-1st 6790  df-2nd 6791  df-map 7471  df-topgen 15335  df-top 19914  df-bases 19915  df-topon 19916  df-cn 20236  df-tx 20570 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator