Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-pt Structured version   Visualization version   Unicode version

Definition df-pt 15421
 Description: Define the product topology on a collection of topologies. For convenience, it is defined on arbitrary collections of sets, expressed as a function from some index set to the subbases of each factor space. (Contributed by Mario Carneiro, 3-Feb-2015.)
Assertion
Ref Expression
df-pt
Distinct variable group:   ,,,,

Detailed syntax breakdown of Definition df-pt
StepHypRef Expression
1 cpt 15415 . 2
2 vf . . 3
3 cvv 3031 . . 3
4 vg . . . . . . . . . 10
54cv 1451 . . . . . . . . 9
62cv 1451 . . . . . . . . . 10
76cdm 4839 . . . . . . . . 9
85, 7wfn 5584 . . . . . . . 8
9 vy . . . . . . . . . . . 12
109cv 1451 . . . . . . . . . . 11
1110, 5cfv 5589 . . . . . . . . . 10
1210, 6cfv 5589 . . . . . . . . . 10
1311, 12wcel 1904 . . . . . . . . 9
1413, 9, 7wral 2756 . . . . . . . 8
1512cuni 4190 . . . . . . . . . . 11
1611, 15wceq 1452 . . . . . . . . . 10
17 vz . . . . . . . . . . . 12
1817cv 1451 . . . . . . . . . . 11
197, 18cdif 3387 . . . . . . . . . 10
2016, 9, 19wral 2756 . . . . . . . . 9
21 cfn 7587 . . . . . . . . 9
2220, 17, 21wrex 2757 . . . . . . . 8
238, 14, 22w3a 1007 . . . . . . 7
24 vx . . . . . . . . 9
2524cv 1451 . . . . . . . 8
269, 7, 11cixp 7540 . . . . . . . 8
2725, 26wceq 1452 . . . . . . 7
2823, 27wa 376 . . . . . 6
2928, 4wex 1671 . . . . 5
3029, 24cab 2457 . . . 4
31 ctg 15414 . . . 4
3230, 31cfv 5589 . . 3
332, 3, 32cmpt 4454 . 2
341, 33wceq 1452 1
 Colors of variables: wff setvar class This definition is referenced by:  ptval  20662
 Copyright terms: Public domain W3C validator