Theorem toponcom

Description: If K is a topology on the base set of topology J , then J is a topology on the base of K . (Contributed by Mario Carneiro, 22-Aug-2015)

	Ref	Expression
Assertion	toponcom	|- ( ( J e. Top /\ K e. ( TopOn ` U. J ) ) -> J e. ( TopOn ` U. K ) )

Proof

Step	Hyp	Ref	Expression
1		toponuni	|- ( K e. ( TopOn ` U. J ) -> U. J = U. K )
2	1	eqcomd	|- ( K e. ( TopOn ` U. J ) -> U. K = U. J )
3	2	anim2i	|- ( ( J e. Top /\ K e. ( TopOn ` U. J ) ) -> ( J e. Top /\ U. K = U. J ) )
4		istopon	|- ( J e. ( TopOn ` U. K ) <-> ( J e. Top /\ U. K = U. J ) )
5	3 4	sylibr	|- ( ( J e. Top /\ K e. ( TopOn ` U. J ) ) -> J e. ( TopOn ` U. K ) )