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=1stZ
txcn.6 Q=2ndZ
Assertion txcn RTopSTopF:WZFUCnR×tSPFUCnRQFUCnS

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=1stZ
6 txcn.6 Q=2ndZ
7 1 toptopon RTopRTopOnX
8 2 toptopon STopSTopOnY
9 3 reseq2i 1stZ=1stX×Y
10 5 9 eqtri P=1stX×Y
11 tx1cn RTopOnXSTopOnY1stX×YR×tSCnR
12 10 11 eqeltrid RTopOnXSTopOnYPR×tSCnR
13 3 reseq2i 2ndZ=2ndX×Y
14 6 13 eqtri Q=2ndX×Y
15 tx2cn RTopOnXSTopOnY2ndX×YR×tSCnS
16 14 15 eqeltrid RTopOnXSTopOnYQR×tSCnS
17 cnco FUCnR×tSPR×tSCnRPFUCnR
18 cnco FUCnR×tSQR×tSCnSQFUCnS
19 17 18 anim12dan FUCnR×tSPR×tSCnRQR×tSCnSPFUCnRQFUCnS
20 19 expcom PR×tSCnRQR×tSCnSFUCnR×tSPFUCnRQFUCnS
21 12 16 20 syl2anc RTopOnXSTopOnYFUCnR×tSPFUCnRQFUCnS
22 7 8 21 syl2anb RTopSTopFUCnR×tSPFUCnRQFUCnS
23 22 3adant3 RTopSTopF:WZFUCnR×tSPFUCnRQFUCnS
24 cntop1 PFUCnRUTop
25 24 ad2antrl RTopSTopF:WZPFUCnRQFUCnSUTop
26 4 topopn UTopWU
27 25 26 syl RTopSTopF:WZPFUCnRQFUCnSWU
28 4 1 cnf PFUCnRPF:WX
29 28 ad2antrl RTopSTopF:WZPFUCnRQFUCnSPF:WX
30 4 2 cnf QFUCnSQF:WY
31 30 ad2antll RTopSTopF:WZPFUCnRQFUCnSQF:WY
32 10 14 upxp WUPF:WXQF:WY∃!hh:WX×YPF=PhQF=Qh
33 feq3 Z=X×Yh:WZh:WX×Y
34 3 33 ax-mp h:WZh:WX×Y
35 34 3anbi1i h:WZPF=PhQF=Qhh:WX×YPF=PhQF=Qh
36 35 eubii ∃!hh:WZPF=PhQF=Qh∃!hh:WX×YPF=PhQF=Qh
37 32 36 sylibr WUPF:WXQF:WY∃!hh:WZPF=PhQF=Qh
38 27 29 31 37 syl3anc RTopSTopF:WZPFUCnRQFUCnS∃!hh:WZPF=PhQF=Qh
39 euex ∃!hh:WZPF=PhQF=Qhhh:WZPF=PhQF=Qh
40 38 39 syl RTopSTopF:WZPFUCnRQFUCnShh:WZPF=PhQF=Qh
41 simpll3 RTopSTopF:WZPFUCnRQFUCnSh:WZPF=PhQF=QhF:WZ
42 27 adantr RTopSTopF:WZPFUCnRQFUCnSh:WZPF=PhQF=QhWU
43 41 42 fexd RTopSTopF:WZPFUCnRQFUCnSh:WZPF=PhQF=QhFV
44 eumo ∃!hh:WZPF=PhQF=Qh*hh:WZPF=PhQF=Qh
45 38 44 syl RTopSTopF:WZPFUCnRQFUCnS*hh:WZPF=PhQF=Qh
46 45 adantr RTopSTopF:WZPFUCnRQFUCnSh:WZPF=PhQF=Qh*hh:WZPF=PhQF=Qh
47 simpr RTopSTopF:WZPFUCnRQFUCnSh:WZPF=PhQF=Qhh:WZPF=PhQF=Qh
48 3anass h:WZPF=PhQF=Qhh:WZPF=PhQF=Qh
49 coeq2 F=hPF=Ph
50 coeq2 F=hQF=Qh
51 49 50 jca F=hPF=PhQF=Qh
52 51 eqcoms h=FPF=PhQF=Qh
53 52 biantrud h=Fh:WZh:WZPF=PhQF=Qh
54 feq1 h=Fh:WZF:WZ
55 53 54 bitr3d h=Fh:WZPF=PhQF=QhF:WZ
56 48 55 syl5bb h=Fh:WZPF=PhQF=QhF:WZ
57 56 moi2 FV*hh:WZPF=PhQF=Qhh:WZPF=PhQF=QhF:WZh=F
58 43 46 47 41 57 syl22anc RTopSTopF:WZPFUCnRQFUCnSh:WZPF=PhQF=Qhh=F
59 eqid R×tS=R×tS
60 59 1 2 3 5 6 uptx PFUCnRQFUCnS∃!hUCnR×tSPF=PhQF=Qh
61 60 adantl RTopSTopF:WZPFUCnRQFUCnS∃!hUCnR×tSPF=PhQF=Qh
62 df-reu ∃!hUCnR×tSPF=PhQF=Qh∃!hhUCnR×tSPF=PhQF=Qh
63 euex ∃!hhUCnR×tSPF=PhQF=QhhhUCnR×tSPF=PhQF=Qh
64 62 63 sylbi ∃!hUCnR×tSPF=PhQF=QhhhUCnR×tSPF=PhQF=Qh
65 eqid R×tS=R×tS
66 4 65 cnf hUCnR×tSh:WR×tS
67 1 2 txuni RTopSTopX×Y=R×tS
68 3 67 eqtrid RTopSTopZ=R×tS
69 68 3adant3 RTopSTopF:WZZ=R×tS
70 69 adantr RTopSTopF:WZPFUCnRQFUCnSZ=R×tS
71 70 feq3d RTopSTopF:WZPFUCnRQFUCnSh:WZh:WR×tS
72 66 71 syl5ibr RTopSTopF:WZPFUCnRQFUCnShUCnR×tSh:WZ
73 72 anim1d RTopSTopF:WZPFUCnRQFUCnShUCnR×tSPF=PhQF=Qhh:WZPF=PhQF=Qh
74 73 48 syl6ibr RTopSTopF:WZPFUCnRQFUCnShUCnR×tSPF=PhQF=Qhh:WZPF=PhQF=Qh
75 simpl hUCnR×tSPF=PhQF=QhhUCnR×tS
76 74 75 jca2 RTopSTopF:WZPFUCnRQFUCnShUCnR×tSPF=PhQF=Qhh:WZPF=PhQF=QhhUCnR×tS
77 76 eximdv RTopSTopF:WZPFUCnRQFUCnShhUCnR×tSPF=PhQF=Qhhh:WZPF=PhQF=QhhUCnR×tS
78 64 77 syl5 RTopSTopF:WZPFUCnRQFUCnS∃!hUCnR×tSPF=PhQF=Qhhh:WZPF=PhQF=QhhUCnR×tS
79 61 78 mpd RTopSTopF:WZPFUCnRQFUCnShh:WZPF=PhQF=QhhUCnR×tS
80 eupick ∃!hh:WZPF=PhQF=Qhhh:WZPF=PhQF=QhhUCnR×tSh:WZPF=PhQF=QhhUCnR×tS
81 38 79 80 syl2anc RTopSTopF:WZPFUCnRQFUCnSh:WZPF=PhQF=QhhUCnR×tS
82 81 imp RTopSTopF:WZPFUCnRQFUCnSh:WZPF=PhQF=QhhUCnR×tS
83 58 82 eqeltrrd RTopSTopF:WZPFUCnRQFUCnSh:WZPF=PhQF=QhFUCnR×tS
84 40 83 exlimddv RTopSTopF:WZPFUCnRQFUCnSFUCnR×tS
85 84 ex RTopSTopF:WZPFUCnRQFUCnSFUCnR×tS
86 23 85 impbid RTopSTopF:WZFUCnR×tSPFUCnRQFUCnS