Metamath Proof Explorer


Theorem tpsuni

Description: The base set of a topological space. (Contributed by FL, 27-Jun-2014)

Ref Expression
Hypotheses istps.a
|- A = ( Base ` K )
istps.j
|- J = ( TopOpen ` K )
Assertion tpsuni
|- ( K e. TopSp -> A = U. J )

Proof

Step Hyp Ref Expression
1 istps.a
 |-  A = ( Base ` K )
2 istps.j
 |-  J = ( TopOpen ` K )
3 1 2 istps2
 |-  ( K e. TopSp <-> ( J e. Top /\ A = U. J ) )
4 3 simprbi
 |-  ( K e. TopSp -> A = U. J )