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

Definition df-top 16968
 Description: Define the (proper) class of all topologies. See istop2g 16974 for an alternate way to express finite intersection and istps5OLD 16994 for a standard definition in terms of both members of a topological space. (Contributed by NM, 3-Mar-2006.)
Assertion
Ref Expression
df-top
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-top
StepHypRef Expression
1 ctop 16963 . 2
2 vy . . . . . . . 8
32cv 1652 . . . . . . 7
43cuni 4017 . . . . . 6
5 vx . . . . . . 7
65cv 1652 . . . . . 6
74, 6wcel 1726 . . . . 5
86cpw 3801 . . . . 5
97, 2, 8wral 2707 . . . 4
10 vz . . . . . . . . 9
1110cv 1652 . . . . . . . 8
123, 11cin 3321 . . . . . . 7
1312, 6wcel 1726 . . . . . 6
1413, 10, 6wral 2707 . . . . 5
1514, 2, 6wral 2707 . . . 4
169, 15wa 360 . . 3
1716, 5cab 2424 . 2
181, 17wceq 1653 1
 Colors of variables: wff set class This definition is referenced by:  istopg  16973
 Copyright terms: Public domain W3C validator