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	⊢ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ ( topGen ‘ 𝐽 ) = ( topGen ‘ 𝐾 ) ) → 𝐽 = 𝐾 )

Proof

Step	Hyp	Ref	Expression
1		tgtop	⊢ ( 𝐽 ∈ Top → ( topGen ‘ 𝐽 ) = 𝐽 )
2		tgtop	⊢ ( 𝐾 ∈ Top → ( topGen ‘ 𝐾 ) = 𝐾 )
3	1 2	eqeqan12d	⊢ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) → ( ( topGen ‘ 𝐽 ) = ( topGen ‘ 𝐾 ) ↔ 𝐽 = 𝐾 ) )
4	3	biimp3a	⊢ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ ( topGen ‘ 𝐽 ) = ( topGen ‘ 𝐾 ) ) → 𝐽 = 𝐾 )