Mathbox for Frédéric Liné < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-prtop Unicode version

Definition df-prtop 25648
 Description: The product topology of a family of topologies is the coarsest topology over the product of the underlying sets that makes the projections continuous. (Bourbaki TG I.14 ex. 3) Experimental. (Contributed by FL, 4-Dec-2011.)
Assertion
Ref Expression
df-prtop
Distinct variable group:   ,,,,

Detailed syntax breakdown of Definition df-prtop
StepHypRef Expression
1 ctopx 25647 . 2
2 vf . . . . . . 7
32cv 1631 . . . . . 6
43cdm 4705 . . . . 5
5 ctop 16647 . . . . 5
64, 5, 3wf 5267 . . . 4
7 vy . . . . . 6
87cv 1631 . . . . 5
9 vt . . . . . . . . . . 11
109cv 1631 . . . . . . . . . 10
1110cuni 3843 . . . . . . . . 9
12 vx . . . . . . . . . 10
1312cv 1631 . . . . . . . . . . . 12
1413, 3cfv 5271 . . . . . . . . . . 11
1514cuni 3843 . . . . . . . . . 10
1612, 4, 15cixp 6833 . . . . . . . . 9
1711, 16wceq 1632 . . . . . . . 8
18 vi . . . . . . . . . . . 12
1918cv 1631 . . . . . . . . . . 11
20 cpro 25253 . . . . . . . . . . 11
2116, 19, 20co 5874 . . . . . . . . . 10
2219, 3cfv 5271 . . . . . . . . . . 11
23 ccn 16970 . . . . . . . . . . 11
2410, 22, 23co 5874 . . . . . . . . . 10
2521, 24wcel 1696 . . . . . . . . 9
2625, 18, 4wral 2556 . . . . . . . 8
2717, 26wa 358 . . . . . . 7
2827, 9, 5crab 2560 . . . . . 6
2928cint 3878 . . . . 5
308, 29wceq 1632 . . . 4
316, 30wa 358 . . 3
3231, 2, 7copab 4092 . 2
331, 32wceq 1632 1
 Colors of variables: wff set class This definition is referenced by:  istopx  25650
 Copyright terms: Public domain W3C validator