Metamath Proof Explorer

Theorem toptopon

Description: Alternative definition of Top in terms of TopOn . (Contributed by Mario Carneiro, 13-Aug-2015)

Ref Expression
Hypothesis toptopon.1 
|- X = U. J
Assertion toptopon 
|- ( J e. Top <-> J e. ( TopOn ` X ) )

Proof

Step Hyp Ref Expression
1 toptopon.1 
 |-  X = U. J
2 istopon 
 |-  ( J e. ( TopOn ` X ) <-> ( J e. Top /\ X = U. J ) )
3 1 2 mpbiran2 
 |-  ( J e. ( TopOn ` X ) <-> J e. Top )
4 3 bicomi 
 |-  ( J e. Top <-> J e. ( TopOn ` X ) )