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

Definition df-topon 17017
Description: Define the set of topologies with a given base set. (Contributed by Stefan O'Rear, 31-Jan-2015.)
Assertion
Ref Expression
df-topon
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-topon
StepHypRef Expression
1 ctopon 17010 . 2
2 vb . . 3
3 cvv 2965 . . 3
42cv 1653 . . . . 5
5 vj . . . . . . 7
65cv 1653 . . . . . 6
76cuni 4043 . . . . 5
84, 7wceq 1654 . . . 4
9 ctop 17009 . . . 4
108, 5, 9crab 2716 . . 3
112, 3, 10cmpt 4301 . 2
121, 11wceq 1654 1
Colors of variables: wff set class
This definition is referenced by:  istopon  17041
  Copyright terms: Public domain W3C validator