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=J
Assertion toptopon JTopJTopOnX

Proof

Step Hyp Ref Expression
1 toptopon.1 X=J
2 istopon JTopOnXJTopX=J
3 1 2 mpbiran2 JTopOnXJTop
4 3 bicomi JTopJTopOnX