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	$⊢ (J \in Top \land K \in Top \land topGen (J) = topGen (K)) \to J = K$

Step	Hyp	Ref	Expression
1		tgtop	$⊢ J \in Top \to topGen (J) = J$
2		tgtop	$⊢ K \in Top \to topGen (K) = K$
3	1 2	eqeqan12d	$⊢ (J \in Top \land K \in Top) \to (topGen (J) = topGen (K) \leftrightarrow J = K)$
4	3	biimp3a	$⊢ (J \in Top \land K \in Top \land topGen (J) = topGen (K)) \to J = K$