This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem tgval3

Description: Alternate expression for the topology generated by a basis. Lemma 2.1 of Munkres p. 80. See also tgval and tgval2 . (Contributed by NM, 17-Jul-2006) (Revised by Mario Carneiro, 30-Aug-2015)

		Ref	Expression
	Assertion	tgval3	⊢ ( 𝐵 ∈ 𝑉 → ( topGen ‘ 𝐵 ) = { 𝑥 ∣ ∃ 𝑦 ( 𝑦 ⊆ 𝐵 ∧ 𝑥 = ∪ 𝑦 ) } )

Proof

Step	Hyp	Ref	Expression
1		eltg3	⊢ ( 𝐵 ∈ 𝑉 → ( 𝑥 ∈ ( topGen ‘ 𝐵 ) ↔ ∃ 𝑦 ( 𝑦 ⊆ 𝐵 ∧ 𝑥 = ∪ 𝑦 ) ) )
2	1	eqabdv	⊢ ( 𝐵 ∈ 𝑉 → ( topGen ‘ 𝐵 ) = { 𝑥 ∣ ∃ 𝑦 ( 𝑦 ⊆ 𝐵 ∧ 𝑥 = ∪ 𝑦 ) } )