Metamath Proof Explorer


Theorem tgtop11

Description: The topology generation function is one-to-one when applied to completed topologies. (Contributed by NM, 18-Jul-2006)

Ref Expression
Assertion tgtop11 JTopKToptopGenJ=topGenKJ=K

Proof

Step Hyp Ref Expression
1 tgtop JToptopGenJ=J
2 tgtop KToptopGenK=K
3 1 2 eqeqan12d JTopKToptopGenJ=topGenKJ=K
4 3 biimp3a JTopKToptopGenJ=topGenKJ=K