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

Definition df-topon 18486
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 18479 . 2
2 vb . . 3
3 cvv 2967 . . 3
42cv 1368 . . . . 5
5 vj . . . . . . 7
65cv 1368 . . . . . 6
76cuni 4086 . . . . 5
84, 7wceq 1369 . . . 4
9 ctop 18478 . . . 4
108, 5, 9crab 2714 . . 3
112, 3, 10cmpt 4345 . 2
121, 11wceq 1369 1
Colors of variables: wff setvar class
This definition is referenced by:  istopon  18510
  Copyright terms: Public domain W3C validator