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

Theorem txcn 12503
 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 12244 . . . 4 TopOn
3 txcn.2 . . . . 5
43toptopon 12244 . . . 4 TopOn
5 txcn.5 . . . . . . 7
6 txcn.3 . . . . . . . 8
76reseq2i 4825 . . . . . . 7
85, 7eqtri 2161 . . . . . 6
9 tx1cn 12497 . . . . . 6 TopOn TopOn
108, 9eqeltrid 2227 . . . . 5 TopOn TopOn
11 txcn.6 . . . . . . 7
126reseq2i 4825 . . . . . . 7
1311, 12eqtri 2161 . . . . . 6
14 tx2cn 12498 . . . . . 6 TopOn TopOn
1513, 14eqeltrid 2227 . . . . 5 TopOn TopOn
16 cnco 12449 . . . . . . 7
17 cnco 12449 . . . . . . 7
1816, 17anim12dan 590 . . . . . 6
1918expcom 115 . . . . 5
2010, 15, 19syl2anc 409 . . . 4 TopOn TopOn
212, 4, 20syl2anb 289 . . 3
23 cntop1 12429 . . . . . . . 8
2423ad2antrl 482 . . . . . . 7
25 txcn.4 . . . . . . . 8
2625topopn 12234 . . . . . . 7
2724, 26syl 14 . . . . . 6
2825, 1cnf 12432 . . . . . . 7
2928ad2antrl 482 . . . . . 6
3025, 3cnf 12432 . . . . . . 7
3130ad2antll 483 . . . . . 6
328, 13upxp 12500 . . . . . . 7
33 feq3 5266 . . . . . . . . . 10
346, 33ax-mp 5 . . . . . . . . 9
35343anbi1i 1173 . . . . . . . 8
3635eubii 2009 . . . . . . 7
3732, 36sylibr 133 . . . . . 6
3827, 29, 31, 37syl3anc 1217 . . . . 5
39 euex 2030 . . . . 5
4038, 39syl 14 . . . 4
41 simpll3 1023 . . . . . . 7
4227adantr 274 . . . . . . 7
431topopn 12234 . . . . . . . . . 10
443topopn 12234 . . . . . . . . . 10
45 xpexg 4662 . . . . . . . . . . 11
466, 45eqeltrid 2227 . . . . . . . . . 10
4743, 44, 46syl2an 287 . . . . . . . . 9
48473adant3 1002 . . . . . . . 8
4948ad2antrr 480 . . . . . . 7
50 fex2 5300 . . . . . . 7
5141, 42, 49, 50syl3anc 1217 . . . . . 6
52 eumo 2032 . . . . . . . 8
5338, 52syl 14 . . . . . . 7
5453adantr 274 . . . . . 6
55 simpr 109 . . . . . 6
56 3anass 967 . . . . . . . 8
57 coeq2 4706 . . . . . . . . . . . 12
58 coeq2 4706 . . . . . . . . . . . 12
5957, 58jca 304 . . . . . . . . . . 11
6059eqcoms 2143 . . . . . . . . . 10
6160biantrud 302 . . . . . . . . 9
62 feq1 5264 . . . . . . . . 9
6361, 62bitr3d 189 . . . . . . . 8
6456, 63syl5bb 191 . . . . . . 7
6564moi2 2870 . . . . . 6
6651, 54, 55, 41, 65syl22anc 1218 . . . . 5
67 eqid 2140 . . . . . . . . . 10
6867, 1, 3, 6, 5, 11uptx 12502 . . . . . . . . 9
6968adantl 275 . . . . . . . 8
70 df-reu 2424 . . . . . . . . . 10
71 euex 2030 . . . . . . . . . 10
7270, 71sylbi 120 . . . . . . . . 9
73 eqid 2140 . . . . . . . . . . . . . . 15
7425, 73cnf 12432 . . . . . . . . . . . . . 14
751, 3txuni 12491 . . . . . . . . . . . . . . . . . 18
766, 75syl5eq 2185 . . . . . . . . . . . . . . . . 17
77763adant3 1002 . . . . . . . . . . . . . . . 16
7877adantr 274 . . . . . . . . . . . . . . 15
7978feq3d 5270 . . . . . . . . . . . . . 14
8074, 79syl5ibr 155 . . . . . . . . . . . . 13
8180anim1d 334 . . . . . . . . . . . 12
8281, 56syl6ibr 161 . . . . . . . . . . 11
83 simpl 108 . . . . . . . . . . 11
8482, 83jca2 306 . . . . . . . . . 10
8584eximdv 1853 . . . . . . . . 9
8672, 85syl5 32 . . . . . . . 8
8769, 86mpd 13 . . . . . . 7
88 eupick 2079 . . . . . . 7
8938, 87, 88syl2anc 409 . . . . . 6
9089imp 123 . . . . 5
9166, 90eqeltrrd 2218 . . . 4
9240, 91exlimddv 1871 . . 3
9392ex 114 . 2
9422, 93impbid 128 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 103   wb 104   w3a 963   wceq 1332  wex 1469   wcel 1481  weu 2000  wmo 2001  wreu 2419  cvv 2690  cuni 3745   cxp 4546   cres 4550   ccom 4552  wf 5128  cfv 5132  (class class class)co 5783  c1st 6045  c2nd 6046  ctop 12223  TopOnctopon 12236   ccn 12413   ctx 12480 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 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-13 1492  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-coll 4052  ax-sep 4055  ax-pow 4107  ax-pr 4140  ax-un 4364  ax-setind 4461 This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-fal 1338  df-nf 1438  df-sb 1737  df-eu 2003  df-mo 2004  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ne 2310  df-ral 2422  df-rex 2423  df-reu 2424  df-rab 2426  df-v 2692  df-sbc 2915  df-csb 3009  df-dif 3079  df-un 3081  df-in 3083  df-ss 3090  df-nul 3370  df-pw 3518  df-sn 3539  df-pr 3540  df-op 3542  df-uni 3746  df-iun 3824  df-br 3939  df-opab 3999  df-mpt 4000  df-id 4224  df-xp 4554  df-rel 4555  df-cnv 4556  df-co 4557  df-dm 4558  df-rn 4559  df-res 4560  df-ima 4561  df-iota 5097  df-fun 5134  df-fn 5135  df-f 5136  df-f1 5137  df-fo 5138  df-f1o 5139  df-fv 5140  df-ov 5786  df-oprab 5787  df-mpo 5788  df-1st 6047  df-2nd 6048  df-map 6553  df-topgen 12200  df-top 12224  df-topon 12237  df-bases 12269  df-cn 12416  df-tx 12481 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator