Home Metamath Proof Explorer < Previous   Next > Related theorems Unicode version

Theorem uptx 11061
 Description: Universal property of the binary topological product. (Contributed by Jeff Madsen, 2-Sep-2009.)
Hypotheses
Ref Expression
uptx.1
uptx.2
uptx.3
uptx.4
uptx.5
uptx.6
Assertion
Ref Expression
uptx Top Top Top Cn Cn Cn
Distinct variable groups:   ,   ,   ,   ,   ,   ,   ,   ,   ,   ,   ,

Proof of Theorem uptx
StepHypRef Expression
1 uniexg 3934 . . . . . 6 Top
2 opabex2g 4637 . . . . . 6
31, 2syl 13 . . . . 5 Top
433ad2ant3 1143 . . . 4 Top Top Top
54adantr 447 . . 3 Top Top Top Cn Cn
6 uptx.1 . . . . . . . . . 10
76txtop 9792 . . . . . . . . 9 Top Top Top
8 eqid 2141 . . . . . . . . . 10
9 eqid 2141 . . . . . . . . . 10
108, 9iscn 9900 . . . . . . . . 9 Top Top Cn
117, 10sylan2 600 . . . . . . . 8 Top Top Top Cn
1211ancoms 416 . . . . . . 7 Top Top Top Cn
13123impa 1312 . . . . . 6 Top Top Top Cn
1413adantr 447 . . . . 5 Top Top Top Cn Cn Cn
15 uptx.2 . . . . . . . . . . . . 13
168, 15cnf 9904 . . . . . . . . . . . 12 Top Top Cn
17163expia 1319 . . . . . . . . . . 11 Top Top Cn
1817ancoms 416 . . . . . . . . . 10 Top Top Cn
19183adant2 1139 . . . . . . . . 9 Top Top Top Cn
20 uptx.3 . . . . . . . . . . . . 13
218, 20cnf 9904 . . . . . . . . . . . 12 Top Top Cn
22213expia 1319 . . . . . . . . . . 11 Top Top Cn
2322ancoms 416 . . . . . . . . . 10 Top Top Cn
24233adant1 1138 . . . . . . . . 9 Top Top Top Cn
2519, 24anim12d 533 . . . . . . . 8 Top Top Top Cn Cn
2625imp 393 . . . . . . 7 Top Top Top Cn Cn
27 ffvelrn 4877 . . . . . . . . . . 11
28 ffvelrn 4877 . . . . . . . . . . 11
29 opelxpi 4173 . . . . . . . . . . 11
3027, 28, 29syl2an 603 . . . . . . . . . 10
3130anandirs 890 . . . . . . . . 9
3231r19.21aiva 2426 . . . . . . . 8
33 eqid 2141 . . . . . . . . 9
3433fopab2 4888 . . . . . . . 8
3532, 34sylib 242 . . . . . . 7
3626, 35syl 13 . . . . . 6 Top Top Top Cn Cn
376, 15, 20txuni 9794 . . . . . . . . 9 Top Top
38373adant3 1140 . . . . . . . 8 Top Top Top
3938adantr 447 . . . . . . 7 Top Top Top Cn Cn
40 feq3 4649 . . . . . . 7
4139, 40syl 13 . . . . . 6 Top Top Top Cn Cn
4236, 41mpbird 318 . . . . 5 Top Top Top Cn Cn
43 txval 9790 . . . . . . . . . . . 12 Top Top topGen
446, 43syl5eq 2185 . . . . . . . . . . 11 Top Top topGen
4544eleq2d 2211 . . . . . . . . . 10 Top Top topGen
46 txbas 9791 . . . . . . . . . . 11 Top Top TopBases
47 eltg3 9747 . . . . . . . . . . 11 TopBases topGen
4846, 47syl 13 . . . . . . . . . 10 Top Top topGen
4945, 48bitrd 284 . . . . . . . . 9 Top Top
50493adant3 1140 . . . . . . . 8 Top Top Top
5150adantr 447 . . . . . . 7 Top Top Top Cn Cn
52 imaiun 4935 . . . . . . . . . . 11
53 simpll3 1161 . . . . . . . . . . . 12 Top Top Top Cn Cn Top
54 ssel2 2847 . . . . . . . . . . . . . . . 16
55 visset 2541 . . . . . . . . . . . . . . . . 17
56 eqeq1 2147 . . . . . . . . . . . . . . . . . 18
57562rexbidv 2391 . . . . . . . . . . . . . . . . 17
5855, 57elab 2644 . . . . . . . . . . . . . . . 16
5954, 58sylib 242 . . . . . . . . . . . . . . 15
60 fveq2 4765 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
61 fveq2 4765 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
6260, 61opeq12d 3353 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
63 opex 3690 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
6462, 33, 63fvopab4 4829 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
6564eleq1d 2210 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
66 fvex 4778 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
6766opelxp 4170 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
6865, 67syl6bb 729 . . . . . . . . . . . . . . . . . . . . . . . . . 26
6968adantl 448 . . . . . . . . . . . . . . . . . . . . . . . . 25
7069pm5.32da 840 . . . . . . . . . . . . . . . . . . . . . . . 24
71 anandi 887 . . . . . . . . . . . . . . . . . . . . . . . 24
7270, 71syl6bb 729 . . . . . . . . . . . . . . . . . . . . . . 23
73 ffn 4659 . . . . . . . . . . . . . . . . . . . . . . . . 25
74 elpreima 4869 . . . . . . . . . . . . . . . . . . . . . . . . 25
7535, 73, 743syl 41 . . . . . . . . . . . . . . . . . . . . . . . 24
7675adantr 447 . . . . . . . . . . . . . . . . . . . . . . 23
77 elin 2999 . . . . . . . . . . . . . . . . . . . . . . . . 25
78 ffn 4659 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
79 elpreima 4869 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
8078, 79syl 13 . . . . . . . . . . . . . . . . . . . . . . . . . 26
81 ffn 4659 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
82 elpreima 4869 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
8381, 82syl 13 . . . . . . . . . . . . . . . . . . . . . . . . . 26
8480, 83bi2anan9 950 . . . . . . . . . . . . . . . . . . . . . . . . 25
8577, 84syl5bb 721 . . . . . . . . . . . . . . . . . . . . . . . 24
8685adantr 447 . . . . . . . . . . . . . . . . . . . . . . 23
8772, 76, 863bitr4d 741 . . . . . . . . . . . . . . . . . . . . . 22
8887eqrdv 2139 . . . . . . . . . . . . . . . . . . . . 21
8926, 88sylan 597 . . . . . . . . . . . . . . . . . . . 20 Top Top Top Cn Cn
90 simpll3 1161 . . . . . . . . . . . . . . . . . . . . 21 Top Top Top Cn Cn Top
91 cnima 9910 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Top Top Cn
9291ex 398 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 Top Top Cn
93923expa 1317 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Top Top Cn
9493ancom1s 856 . . . . . . . . . . . . . . . . . . . . . . . . 25 Top Top Cn
95943adantl2 1278 . . . . . . . . . . . . . . . . . . . . . . . 24 Top Top Top Cn
9695imp 393 . . . . . . . . . . . . . . . . . . . . . . 23 Top Top Top Cn
9796adantlrr 789 . . . . . . . . . . . . . . . . . . . . . 22 Top Top Top Cn Cn
9897adantrr 781 . . . . . . . . . . . . . . . . . . . . 21 Top Top Top Cn Cn
99 cnima 9910 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Top Top Cn
10099ex 398 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 Top Top Cn
1011003expa 1317 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Top Top Cn
102101ancom1s 856 . . . . . . . . . . . . . . . . . . . . . . . . 25 Top Top Cn
1031023adantl1 1276 . . . . . . . . . . . . . . . . . . . . . . . 24 Top Top Top Cn
104103imp 393 . . . . . . . . . . . . . . . . . . . . . . 23 Top Top Top Cn
105104adantlrl 787 . . . . . . . . . . . . . . . . . . . . . 22 Top Top Top Cn Cn
106105adantrl 779 . . . . . . . . . . . . . . . . . . . . 21 Top Top Top Cn Cn
107 inopn 9704 . . . . . . . . . . . . . . . . . . . . 21 Top
10890, 98, 106, 107syl111anc 1349 . . . . . . . . . . . . . . . . . . . 20 Top Top Top Cn Cn
10989, 108eqeltrd 2218 . . . . . . . . . . . . . . . . . . 19 Top Top Top Cn Cn
110109ex 398 . . . . . . . . . . . . . . . . . 18 Top Top Top Cn Cn
111 imaeq2 4380 . . . . . . . . . . . . . . . . . . . 20
112111eleq1d 2210 . . . . . . . . . . . . . . . . . . 19
113112biimprcd 234 . . . . . . . . . . . . . . . . . 18
114110, 113syl6 42 . . . . . . . . . . . . . . . . 17 Top Top Top Cn Cn
115114r19.23advv 2466 . . . . . . . . . . . . . . . 16 Top Top Top Cn Cn
116115imp 393 . . . . . . . . . . . . . . 15 Top Top Top Cn Cn
11759, 116sylan2 600 . . . . . . . . . . . . . 14 Top Top Top Cn Cn
118117anassrs 632 . . . . . . . . . . . . 13 Top Top Top Cn Cn
119118r19.21aiva 2426 . . . . . . . . . . . 12 Top Top Top Cn Cn
120 iunopn 9703 . . . . . . . . . . . 12 Top
12153, 119, 120syl11anc 659 . . . . . . . . . . 11 Top Top Top Cn Cn
12252, 121syl5eqel 2222 . . . . . . . . . 10 Top Top Top Cn Cn
123 imaeq2 4380 . . . . . . . . . . 11
124123eleq1d 2210 . . . . . . . . . 10
125122, 124syl5ibrcom 258 . . . . . . . . 9 Top Top Top Cn Cn
126125expimpd 576 . . . . . . . 8 Top Top Top Cn Cn
12712619.23adv 1860 . . . . . . 7 Top Top Top Cn Cn
12851, 127sylbid 246 . . . . . 6 Top Top Top Cn Cn
129128r19.21aiv 2425 . . . . 5 Top Top Top Cn Cn
13014, 42, 129mpbir2and 1036 . . . 4 Top Top Top Cn Cn Cn
13178adantr 447 . . . . . . . 8
132 fo1st 5138 . . . . . . . . . . . 12
133 fofn 4707 . . . . . . . . . . . 12
134132, 133ax-mp 7 . . . . . . . . . . 11
135 ssv 2864 . . . . . . . . . . 11
136 fnssres 4625 . . . . . . . . . . 11
137134, 135, 136mp2an 681 . . . . . . . . . 10
138137a1i 8 . . . . . . . . 9
13935, 73syl 13 . . . . . . . . 9
140 frn 4665 . . . . . . . . . 10
14135, 140syl 13 . . . . . . . . 9
142 fnco 4620 . . . . . . . . 9
143138, 139, 141, 142syl111anc 1349 . . . . . . . 8
144 eqfnfv 4853 . . . . . . . 8
145131, 143, 144syl11anc 659 . . . . . . 7
146 eqidd 2142 . . . . . . 7
147 fnfun 4610 . . . . . . . . . . . 12
148137, 147ax-mp 7 . . . . . . . . . . 11
149148a1i 8 . . . . . . . . . 10
15035adantr 447 . . . . . . . . . . 11
151 ffun 4661 . . . . . . . . . . 11
152150, 151syl 13 . . . . . . . . . 10
153 fdm 4663 . . . . . . . . . . . . 13
15435, 153syl 13 . . . . . . . . . . . 12
155154eleq2d 2211 . . . . . . . . . . 11
156155biimpar 616 . . . . . . . . . 10
157 fvco 4822 . . . . . . . . . 10
158149, 152, 156, 157syl111anc 1349 . . . . . . . . 9
15964adantl 448 . . . . . . . . . . 11
160159fveq2d 4769 . . . . . . . . . 10
161 ffvelrn 4877 . . . . . . . . . . . . 13
162 ffvelrn 4877 . . . . . . . . . . . . 13
163 opelxpi 4173 . . . . . . . . . . . . 13
164161, 162, 163syl2an 603 . . . . . . . . . . . 12
165164anandirs 890 . . . . . . . . . . 11
166 fvres 4780 . . . . . . . . . . 11
167165, 166syl 13 . . . . . . . . . 10
168 fvex 4778 . . . . . . . . . . . 12
169168op1st 5132 . . . . . . . . . . 11
170169a1i 8 . . . . . . . . . 10
171160, 167, 1703eqtrd 2177 . . . . . . . . 9
172158, 171eqtr2d 2174 . . . . . . . 8
173172r19.21aiva 2426 . . . . . . 7
174145, 146, 173mpbir2and 1036 . . . . . 6
175 uptx.5 . . . . . . . 8
176 uptx.4 . . . . . . . . 9
177176reseq2i 4340 . . . . . . . 8
178175, 177eqtri 2161 . . . . . . 7
179178coeq1i 4252 . . . . . 6
180174, 179syl6eqr 2195 . . . . 5
18126, 180syl 13 . . . 4 Top Top Top Cn Cn
18281adantl 448 . . . . . . . 8
183 fo2nd 5139 . . . . . . . . . . . 12
184 fofn 4707 . . . . . . . . . . . 12
185183, 184ax-mp 7 . . . . . . . . . . 11
186 fnssres 4625 . . . . . . . . . . 11
187185, 135, 186mp2an 681 . . . . . . . . . 10
188187a1i 8 . . . . . . . . 9
189 fnco 4620 . . . . . . . . 9
190188, 139, 141, 189syl111anc 1349 . . . . . . . 8
191 eqfnfv 4853 . . . . . . . 8
192182, 190, 191syl11anc 659 . . . . . . 7
193 fnfun 4610 . . . . . . . . . . . 12
194187, 193ax-mp 7 . . . . . . . . . . 11
195194a1i 8 . . . . . . . . . 10
196 fvco 4822 . . . . . . . . . 10
197195, 152, 156, 196syl111anc 1349 . . . . . . . . 9
198159fveq2d 4769 . . . . . . . . . 10
199 fvres 4780 . . . . . . . . . . 11
200165, 199syl 13 . . . . . . . . . 10
201168, 66op2nd 5133 . . . . . . . . . . 11
202201a1i 8 . . . . . . . . . 10
203198, 200, 2023eqtrd 2177 . . . . . . . . 9
204197, 203eqtr2d 2174 . . . . . . . 8
205204r19.21aiva 2426 . . . . . . 7
206192, 146, 205mpbir2and 1036 . . . . . 6
207 uptx.6 . . . . . . . 8
208176reseq2i 4340 . . . . . . . 8
209207, 208eqtri 2161 . . . . . . 7
210209coeq1i 4252 . . . . . 6
211206, 210syl6eqr 2195 . . . . 5
21226, 211syl 13 . . . 4 Top Top Top Cn Cn
213130, 181, 212jca32 499 . . 3 Top Top Top Cn Cn Cn
214 eleq1 2204 . . . . 5 Cn Cn
215 coeq2 4251 . . . . . . 7
216215eqeq2d 2152 . . . . . 6
217 coeq2 4251 . . . . . . 7
218217eqeq2d 2152 . . . . . 6
219216, 218anbi12d 763 . . . . 5
220214, 219anbi12d 763 . . . 4 Cn Cn
221220cla4egv 2605 . . 3 Cn Cn
2225, 213, 221sylc 44 . 2 Top Top Top Cn Cn Cn
22325imdistani 770 . . 3 Top Top Top Cn Cn Top Top Top
2248, 9cnf 9904 . . . . . . . . . . . . 13 Top Top Cn
2252243expia 1319 . . . . . . . . . . . 12 Top Top Cn
2267, 225sylan2 600 . . . . . . . . . . 11 Top Top Top Cn
227226ancoms 416 . . . . . . . . . 10 Top Top Top Cn
2282273impa 1312 . . . . . . . . 9 Top Top Top Cn
229 feq3 4649 . . . . . . . . . 10
23038, 229syl 13 . . . . . . . . 9 Top Top Top
231228, 230sylibd 245 . . . . . . . 8 Top Top Top Cn
232231adantr 447 . . . . . . 7 Top Top Top Cn
233232anim1d 534 . . . . . 6 Top Top Top Cn
234 3anass 1106 . . . . . 6
235233, 234syl6ibr 262 . . . . 5 Top Top Top Cn
23623519.21aiv 1933 . . . 4 Top Top Top Cn
237178, 209upxp 11060 . . . . . . . 8
238 eumo 2072 . . . . . . . 8
239237, 238syl 13 . . . . . . 7
2402393expb 1318 . . . . . 6
2411, 240sylan 597 . . . . 5 Top
2422413ad2antl3 1290 . . . 4 Top Top Top
243 immo 2078 . . . 4 Cn Cn
244236, 242, 243sylc 44 . . 3 Top Top Top Cn
245223, 244syl 13 . 2 Top Top Top Cn Cn Cn
246 df-reu 2361 . . 3 Cn Cn
247 eu5 2070 . . 3 Cn Cn Cn
248246, 247bitri 279 . 2 Cn Cn Cn
249222, 245, 248sylanbrc 664 1 Top Top Top Cn Cn Cn
 Colors of variables: wff set class Syntax hints:   wi 3   wb 219   wa 337   w3a 1102  wal 1584   wceq 1586   wcel 1588  wex 1615  weu 2037  wmo 2038  cab 2128  wral 2355  wrex 2356  wreu 2357  cvv 2538   cin 2826   wss 2827  cop 3240  cuni 3366  ciun 3436  copab 3565   cxp 4117  ccnv 4118   cdm 4119   crn 4120   cres 4121  cima 4122   ccom 4123   wfun 4125   wfn 4126  wf 4127  wfo 4129  cfv 4131  (class class class)co 4981  c1st 5124  c2nd 5125  Topctop 9686  TopBasesctb 9690  topGenctg 9691   ctx 9788   Cn ccn 9894 This theorem is referenced by:  txcn 11062 This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1592  ax-gen 1593  ax-8 1594  ax-9 1595  ax-10 1596  ax-11 1597  ax-12 1598  ax-13 1599  ax-14 1600  ax-17 1605  ax-4 1608  ax-5o 1610  ax-6o 1613  ax-9o 1763  ax-10o 1781  ax-16 1854  ax-11o 1864  ax-ext 2123  ax-rep 3596  ax-sep 3606  ax-nul 3613  ax-pow 3649  ax-pr 3687  ax-un 3929 This theorem depends on definitions:  df-bi 220  df-or 338  df-an 339  df-3an 1104  df-ex 1616  df-sb 1816  df-eu 2041  df-mo 2042  df-clab 2129  df-cleq 2134  df-clel 2137  df-ne 2268  df-ral 2359  df-rex 2360  df-reu 2361  df-rab 2362  df-v 2540  df-sbc 2700  df-csb 2774  df-dif 2830  df-un 2832  df-in 2834  df-ss 2836  df-nul 3083  df-pw 3229  df-sn 3242  df-pr 3243  df-op 3246  df-uni 3367  df-iun 3438  df-br 3508  df-opab 3566  df-id 3747  df-xp 4133  df-rel 4134  df-cnv 4135  df-co 4136  df-dm 4137  df-rn 4138  df-res 4139  df-ima 4140  df-fun 4141  df-fn 4142  df-f 4143  df-fo 4145  df-fv 4147  df-opr 4983  df-oprab 4984  df-1st 5126  df-2nd 5127  df-map 5544  df-top 9692  df-bases 9694  df-topgen 9695  df-tx 9789  df-cn 9896