Metamath Proof Explorer


Theorem txcn

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)

Ref Expression
Hypotheses txcn.1 X = R
txcn.2 Y = S
txcn.3 Z = X × Y
txcn.4 W = U
txcn.5 P = 1 st Z
txcn.6 Q = 2 nd Z
Assertion txcn R Top S Top F : W Z F U Cn R × t S P F U Cn R Q F U Cn S

Proof

Step Hyp Ref Expression
1 txcn.1 X = R
2 txcn.2 Y = S
3 txcn.3 Z = X × Y
4 txcn.4 W = U
5 txcn.5 P = 1 st Z
6 txcn.6 Q = 2 nd Z
7 1 toptopon R Top R TopOn X
8 2 toptopon S Top S TopOn Y
9 3 reseq2i 1 st Z = 1 st X × Y
10 5 9 eqtri P = 1 st X × Y
11 tx1cn R TopOn X S TopOn Y 1 st X × Y R × t S Cn R
12 10 11 eqeltrid R TopOn X S TopOn Y P R × t S Cn R
13 3 reseq2i 2 nd Z = 2 nd X × Y
14 6 13 eqtri Q = 2 nd X × Y
15 tx2cn R TopOn X S TopOn Y 2 nd X × Y R × t S Cn S
16 14 15 eqeltrid R TopOn X S TopOn Y Q R × t S Cn S
17 cnco F U Cn R × t S P R × t S Cn R P F U Cn R
18 cnco F U Cn R × t S Q R × t S Cn S Q F U Cn S
19 17 18 anim12dan F U Cn R × t S P R × t S Cn R Q R × t S Cn S P F U Cn R Q F U Cn S
20 19 expcom P R × t S Cn R Q R × t S Cn S F U Cn R × t S P F U Cn R Q F U Cn S
21 12 16 20 syl2anc R TopOn X S TopOn Y F U Cn R × t S P F U Cn R Q F U Cn S
22 7 8 21 syl2anb R Top S Top F U Cn R × t S P F U Cn R Q F U Cn S
23 22 3adant3 R Top S Top F : W Z F U Cn R × t S P F U Cn R Q F U Cn S
24 cntop1 P F U Cn R U Top
25 24 ad2antrl R Top S Top F : W Z P F U Cn R Q F U Cn S U Top
26 4 topopn U Top W U
27 25 26 syl R Top S Top F : W Z P F U Cn R Q F U Cn S W U
28 4 1 cnf P F U Cn R P F : W X
29 28 ad2antrl R Top S Top F : W Z P F U Cn R Q F U Cn S P F : W X
30 4 2 cnf Q F U Cn S Q F : W Y
31 30 ad2antll R Top S Top F : W Z P F U Cn R Q F U Cn S Q F : W Y
32 10 14 upxp W U P F : W X Q F : W Y ∃! h h : W X × Y P F = P h Q F = Q h
33 feq3 Z = X × Y h : W Z h : W X × Y
34 3 33 ax-mp h : W Z h : W X × Y
35 34 3anbi1i h : W Z P F = P h Q F = Q h h : W X × Y P F = P h Q F = Q h
36 35 eubii ∃! h h : W Z P F = P h Q F = Q h ∃! h h : W X × Y P F = P h Q F = Q h
37 32 36 sylibr W U P F : W X Q F : W Y ∃! h h : W Z P F = P h Q F = Q h
38 27 29 31 37 syl3anc R Top S Top F : W Z P F U Cn R Q F U Cn S ∃! h h : W Z P F = P h Q F = Q h
39 euex ∃! h h : W Z P F = P h Q F = Q h h h : W Z P F = P h Q F = Q h
40 38 39 syl R Top S Top F : W Z P F U Cn R Q F U Cn S h h : W Z P F = P h Q F = Q h
41 simpll3 R Top S Top F : W Z P F U Cn R Q F U Cn S h : W Z P F = P h Q F = Q h F : W Z
42 27 adantr R Top S Top F : W Z P F U Cn R Q F U Cn S h : W Z P F = P h Q F = Q h W U
43 41 42 fexd R Top S Top F : W Z P F U Cn R Q F U Cn S h : W Z P F = P h Q F = Q h F V
44 eumo ∃! h h : W Z P F = P h Q F = Q h * h h : W Z P F = P h Q F = Q h
45 38 44 syl R Top S Top F : W Z P F U Cn R Q F U Cn S * h h : W Z P F = P h Q F = Q h
46 45 adantr R Top S Top F : W Z P F U Cn R Q F U Cn S h : W Z P F = P h Q F = Q h * h h : W Z P F = P h Q F = Q h
47 simpr R Top S Top F : W Z P F U Cn R Q F U Cn S h : W Z P F = P h Q F = Q h h : W Z P F = P h Q F = Q h
48 3anass h : W Z P F = P h Q F = Q h h : W Z P F = P h Q F = Q h
49 coeq2 F = h P F = P h
50 coeq2 F = h Q F = Q h
51 49 50 jca F = h P F = P h Q F = Q h
52 51 eqcoms h = F P F = P h Q F = Q h
53 52 biantrud h = F h : W Z h : W Z P F = P h Q F = Q h
54 feq1 h = F h : W Z F : W Z
55 53 54 bitr3d h = F h : W Z P F = P h Q F = Q h F : W Z
56 48 55 syl5bb h = F h : W Z P F = P h Q F = Q h F : W Z
57 56 moi2 F V * h h : W Z P F = P h Q F = Q h h : W Z P F = P h Q F = Q h F : W Z h = F
58 43 46 47 41 57 syl22anc R Top S Top F : W Z P F U Cn R Q F U Cn S h : W Z P F = P h Q F = Q h h = F
59 eqid R × t S = R × t S
60 59 1 2 3 5 6 uptx P F U Cn R Q F U Cn S ∃! h U Cn R × t S P F = P h Q F = Q h
61 60 adantl R Top S Top F : W Z P F U Cn R Q F U Cn S ∃! h U Cn R × t S P F = P h Q F = Q h
62 df-reu ∃! h U Cn R × t S P F = P h Q F = Q h ∃! h h U Cn R × t S P F = P h Q F = Q h
63 euex ∃! h h U Cn R × t S P F = P h Q F = Q h h h U Cn R × t S P F = P h Q F = Q h
64 62 63 sylbi ∃! h U Cn R × t S P F = P h Q F = Q h h h U Cn R × t S P F = P h Q F = Q h
65 eqid R × t S = R × t S
66 4 65 cnf h U Cn R × t S h : W R × t S
67 1 2 txuni R Top S Top X × Y = R × t S
68 3 67 eqtrid R Top S Top Z = R × t S
69 68 3adant3 R Top S Top F : W Z Z = R × t S
70 69 adantr R Top S Top F : W Z P F U Cn R Q F U Cn S Z = R × t S
71 70 feq3d R Top S Top F : W Z P F U Cn R Q F U Cn S h : W Z h : W R × t S
72 66 71 syl5ibr R Top S Top F : W Z P F U Cn R Q F U Cn S h U Cn R × t S h : W Z
73 72 anim1d R Top S Top F : W Z P F U Cn R Q F U Cn S h U Cn R × t S P F = P h Q F = Q h h : W Z P F = P h Q F = Q h
74 73 48 syl6ibr R Top S Top F : W Z P F U Cn R Q F U Cn S h U Cn R × t S P F = P h Q F = Q h h : W Z P F = P h Q F = Q h
75 simpl h U Cn R × t S P F = P h Q F = Q h h U Cn R × t S
76 74 75 jca2 R Top S Top F : W Z P F U Cn R Q F U Cn S h U Cn R × t S P F = P h Q F = Q h h : W Z P F = P h Q F = Q h h U Cn R × t S
77 76 eximdv R Top S Top F : W Z P F U Cn R Q F U Cn S h h U Cn R × t S P F = P h Q F = Q h h h : W Z P F = P h Q F = Q h h U Cn R × t S
78 64 77 syl5 R Top S Top F : W Z P F U Cn R Q F U Cn S ∃! h U Cn R × t S P F = P h Q F = Q h h h : W Z P F = P h Q F = Q h h U Cn R × t S
79 61 78 mpd R Top S Top F : W Z P F U Cn R Q F U Cn S h h : W Z P F = P h Q F = Q h h U Cn R × t S
80 eupick ∃! h h : W Z P F = P h Q F = Q h h h : W Z P F = P h Q F = Q h h U Cn R × t S h : W Z P F = P h Q F = Q h h U Cn R × t S
81 38 79 80 syl2anc R Top S Top F : W Z P F U Cn R Q F U Cn S h : W Z P F = P h Q F = Q h h U Cn R × t S
82 81 imp R Top S Top F : W Z P F U Cn R Q F U Cn S h : W Z P F = P h Q F = Q h h U Cn R × t S
83 58 82 eqeltrrd R Top S Top F : W Z P F U Cn R Q F U Cn S h : W Z P F = P h Q F = Q h F U Cn R × t S
84 40 83 exlimddv R Top S Top F : W Z P F U Cn R Q F U Cn S F U Cn R × t S
85 84 ex R Top S Top F : W Z P F U Cn R Q F U Cn S F U Cn R × t S
86 23 85 impbid R Top S Top F : W Z F U Cn R × t S P F U Cn R Q F U Cn S