Metamath Proof Explorer


Theorem uptx

Description: Universal property of the binary topological product. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 22-Aug-2015)

Ref Expression
Hypotheses uptx.1 T=R×tS
uptx.2 X=R
uptx.3 Y=S
uptx.4 Z=X×Y
uptx.5 P=1stZ
uptx.6 Q=2ndZ
Assertion uptx FUCnRGUCnS∃!hUCnTF=PhG=Qh

Proof

Step Hyp Ref Expression
1 uptx.1 T=R×tS
2 uptx.2 X=R
3 uptx.3 Y=S
4 uptx.4 Z=X×Y
5 uptx.5 P=1stZ
6 uptx.6 Q=2ndZ
7 eqid U=U
8 eqid xUFxGx=xUFxGx
9 7 8 txcnmpt FUCnRGUCnSxUFxGxUCnR×tS
10 1 oveq2i UCnT=UCnR×tS
11 9 10 eleqtrrdi FUCnRGUCnSxUFxGxUCnT
12 7 2 cnf FUCnRF:UX
13 7 3 cnf GUCnSG:UY
14 ffn F:UXFFnU
15 14 adantr F:UXG:UYFFnU
16 fo1st 1st:VontoV
17 fofn 1st:VontoV1stFnV
18 16 17 ax-mp 1stFnV
19 ssv X×YV
20 fnssres 1stFnVX×YV1stX×YFnX×Y
21 18 19 20 mp2an 1stX×YFnX×Y
22 ffvelrn F:UXxUFxX
23 ffvelrn G:UYxUGxY
24 opelxpi FxXGxYFxGxX×Y
25 22 23 24 syl2an F:UXxUG:UYxUFxGxX×Y
26 25 anandirs F:UXG:UYxUFxGxX×Y
27 26 fmpttd F:UXG:UYxUFxGx:UX×Y
28 ffn xUFxGx:UX×YxUFxGxFnU
29 27 28 syl F:UXG:UYxUFxGxFnU
30 27 frnd F:UXG:UYranxUFxGxX×Y
31 fnco 1stX×YFnX×YxUFxGxFnUranxUFxGxX×Y1stX×YxUFxGxFnU
32 21 29 30 31 mp3an2i F:UXG:UY1stX×YxUFxGxFnU
33 fvco3 xUFxGx:UX×YzU1stX×YxUFxGxz=1stX×YxUFxGxz
34 27 33 sylan F:UXG:UYzU1stX×YxUFxGxz=1stX×YxUFxGxz
35 fveq2 x=zFx=Fz
36 fveq2 x=zGx=Gz
37 35 36 opeq12d x=zFxGx=FzGz
38 opex FzGzV
39 37 8 38 fvmpt zUxUFxGxz=FzGz
40 39 adantl F:UXG:UYzUxUFxGxz=FzGz
41 40 fveq2d F:UXG:UYzU1stX×YxUFxGxz=1stX×YFzGz
42 ffvelrn F:UXzUFzX
43 ffvelrn G:UYzUGzY
44 opelxpi FzXGzYFzGzX×Y
45 42 43 44 syl2an F:UXzUG:UYzUFzGzX×Y
46 45 anandirs F:UXG:UYzUFzGzX×Y
47 46 fvresd F:UXG:UYzU1stX×YFzGz=1stFzGz
48 fvex FzV
49 fvex GzV
50 48 49 op1st 1stFzGz=Fz
51 47 50 eqtrdi F:UXG:UYzU1stX×YFzGz=Fz
52 34 41 51 3eqtrrd F:UXG:UYzUFz=1stX×YxUFxGxz
53 15 32 52 eqfnfvd F:UXG:UYF=1stX×YxUFxGx
54 4 reseq2i 1stZ=1stX×Y
55 5 54 eqtri P=1stX×Y
56 55 coeq1i PxUFxGx=1stX×YxUFxGx
57 53 56 eqtr4di F:UXG:UYF=PxUFxGx
58 12 13 57 syl2an FUCnRGUCnSF=PxUFxGx
59 ffn G:UYGFnU
60 59 adantl F:UXG:UYGFnU
61 fo2nd 2nd:VontoV
62 fofn 2nd:VontoV2ndFnV
63 61 62 ax-mp 2ndFnV
64 fnssres 2ndFnVX×YV2ndX×YFnX×Y
65 63 19 64 mp2an 2ndX×YFnX×Y
66 fnco 2ndX×YFnX×YxUFxGxFnUranxUFxGxX×Y2ndX×YxUFxGxFnU
67 65 29 30 66 mp3an2i F:UXG:UY2ndX×YxUFxGxFnU
68 fvco3 xUFxGx:UX×YzU2ndX×YxUFxGxz=2ndX×YxUFxGxz
69 27 68 sylan F:UXG:UYzU2ndX×YxUFxGxz=2ndX×YxUFxGxz
70 40 fveq2d F:UXG:UYzU2ndX×YxUFxGxz=2ndX×YFzGz
71 46 fvresd F:UXG:UYzU2ndX×YFzGz=2ndFzGz
72 48 49 op2nd 2ndFzGz=Gz
73 71 72 eqtrdi F:UXG:UYzU2ndX×YFzGz=Gz
74 69 70 73 3eqtrrd F:UXG:UYzUGz=2ndX×YxUFxGxz
75 60 67 74 eqfnfvd F:UXG:UYG=2ndX×YxUFxGx
76 4 reseq2i 2ndZ=2ndX×Y
77 6 76 eqtri Q=2ndX×Y
78 77 coeq1i QxUFxGx=2ndX×YxUFxGx
79 75 78 eqtr4di F:UXG:UYG=QxUFxGx
80 12 13 79 syl2an FUCnRGUCnSG=QxUFxGx
81 11 58 80 jca32 FUCnRGUCnSxUFxGxUCnTF=PxUFxGxG=QxUFxGx
82 eleq1 h=xUFxGxhUCnTxUFxGxUCnT
83 coeq2 h=xUFxGxPh=PxUFxGx
84 83 eqeq2d h=xUFxGxF=PhF=PxUFxGx
85 coeq2 h=xUFxGxQh=QxUFxGx
86 85 eqeq2d h=xUFxGxG=QhG=QxUFxGx
87 84 86 anbi12d h=xUFxGxF=PhG=QhF=PxUFxGxG=QxUFxGx
88 82 87 anbi12d h=xUFxGxhUCnTF=PhG=QhxUFxGxUCnTF=PxUFxGxG=QxUFxGx
89 88 spcegv xUFxGxUCnTxUFxGxUCnTF=PxUFxGxG=QxUFxGxhhUCnTF=PhG=Qh
90 11 81 89 sylc FUCnRGUCnShhUCnTF=PhG=Qh
91 eqid T=T
92 7 91 cnf hUCnTh:UT
93 cntop2 FUCnRRTop
94 cntop2 GUCnSSTop
95 1 unieqi T=R×tS
96 2 3 txuni RTopSTopX×Y=R×tS
97 95 96 eqtr4id RTopSTopT=X×Y
98 93 94 97 syl2an FUCnRGUCnST=X×Y
99 98 feq3d FUCnRGUCnSh:UTh:UX×Y
100 92 99 syl5ib FUCnRGUCnShUCnTh:UX×Y
101 100 anim1d FUCnRGUCnShUCnTF=PhG=Qhh:UX×YF=PhG=Qh
102 3anass h:UX×YF=PhG=Qhh:UX×YF=PhG=Qh
103 101 102 syl6ibr FUCnRGUCnShUCnTF=PhG=Qhh:UX×YF=PhG=Qh
104 103 alrimiv FUCnRGUCnShhUCnTF=PhG=Qhh:UX×YF=PhG=Qh
105 cntop1 FUCnRUTop
106 105 uniexd FUCnRUV
107 55 77 upxp UVF:UXG:UY∃!hh:UX×YF=PhG=Qh
108 106 12 13 107 syl2an3an FUCnRGUCnS∃!hh:UX×YF=PhG=Qh
109 eumo ∃!hh:UX×YF=PhG=Qh*hh:UX×YF=PhG=Qh
110 108 109 syl FUCnRGUCnS*hh:UX×YF=PhG=Qh
111 moim hhUCnTF=PhG=Qhh:UX×YF=PhG=Qh*hh:UX×YF=PhG=Qh*hhUCnTF=PhG=Qh
112 104 110 111 sylc FUCnRGUCnS*hhUCnTF=PhG=Qh
113 df-reu ∃!hUCnTF=PhG=Qh∃!hhUCnTF=PhG=Qh
114 df-eu ∃!hhUCnTF=PhG=QhhhUCnTF=PhG=Qh*hhUCnTF=PhG=Qh
115 113 114 bitri ∃!hUCnTF=PhG=QhhhUCnTF=PhG=Qh*hhUCnTF=PhG=Qh
116 90 112 115 sylanbrc FUCnRGUCnS∃!hUCnTF=PhG=Qh