Theorem tgtop

Description: A topology is its own basis. (Contributed by NM, 18-Jul-2006)

	Ref	Expression
Assertion	tgtop	⊢ ( 𝐽 ∈ Top → ( topGen ‘ 𝐽 ) = 𝐽 )

Proof

Step	Hyp	Ref	Expression
1		eltg3	⊢ ( 𝐽 ∈ Top → ( 𝑥 ∈ ( topGen ‘ 𝐽 ) ↔ ∃ 𝑦 ( 𝑦 ⊆ 𝐽 ∧ 𝑥 = ∪ 𝑦 ) ) )
2		simpr	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ 𝑥 = ∪ 𝑦 ) → 𝑥 = ∪ 𝑦 )
3		uniopn	⊢ ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) → ∪ 𝑦 ∈ 𝐽 )
4	3	adantr	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ 𝑥 = ∪ 𝑦 ) → ∪ 𝑦 ∈ 𝐽 )
5	2 4	eqeltrd	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ 𝑥 = ∪ 𝑦 ) → 𝑥 ∈ 𝐽 )
6	5	expl	⊢ ( 𝐽 ∈ Top → ( ( 𝑦 ⊆ 𝐽 ∧ 𝑥 = ∪ 𝑦 ) → 𝑥 ∈ 𝐽 ) )
7	6	exlimdv	⊢ ( 𝐽 ∈ Top → ( ∃ 𝑦 ( 𝑦 ⊆ 𝐽 ∧ 𝑥 = ∪ 𝑦 ) → 𝑥 ∈ 𝐽 ) )
8	1 7	sylbid	⊢ ( 𝐽 ∈ Top → ( 𝑥 ∈ ( topGen ‘ 𝐽 ) → 𝑥 ∈ 𝐽 ) )
9	8	ssrdv	⊢ ( 𝐽 ∈ Top → ( topGen ‘ 𝐽 ) ⊆ 𝐽 )
10		bastg	⊢ ( 𝐽 ∈ Top → 𝐽 ⊆ ( topGen ‘ 𝐽 ) )
11	9 10	eqssd	⊢ ( 𝐽 ∈ Top → ( topGen ‘ 𝐽 ) = 𝐽 )