Theorem eltg4i

Description: An open set in a topology generated by a basis is the union of all basic open sets contained in it. (Contributed by Stefan O'Rear, 22-Feb-2015)

	Ref	Expression
Assertion	eltg4i	⊢ ( 𝐴 ∈ ( topGen ‘ 𝐵 ) → 𝐴 = ∪ ( 𝐵 ∩ 𝒫 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		elfvdm	⊢ ( 𝐴 ∈ ( topGen ‘ 𝐵 ) → 𝐵 ∈ dom topGen )
2		eltg	⊢ ( 𝐵 ∈ dom topGen → ( 𝐴 ∈ ( topGen ‘ 𝐵 ) ↔ 𝐴 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝐴 ) ) )
3	1 2	syl	⊢ ( 𝐴 ∈ ( topGen ‘ 𝐵 ) → ( 𝐴 ∈ ( topGen ‘ 𝐵 ) ↔ 𝐴 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝐴 ) ) )
4	3	ibi	⊢ ( 𝐴 ∈ ( topGen ‘ 𝐵 ) → 𝐴 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝐴 ) )
5		inss2	⊢ ( 𝐵 ∩ 𝒫 𝐴 ) ⊆ 𝒫 𝐴
6	5	unissi	⊢ ∪ ( 𝐵 ∩ 𝒫 𝐴 ) ⊆ ∪ 𝒫 𝐴
7		unipw	⊢ ∪ 𝒫 𝐴 = 𝐴
8	6 7	sseqtri	⊢ ∪ ( 𝐵 ∩ 𝒫 𝐴 ) ⊆ 𝐴
9	8	a1i	⊢ ( 𝐴 ∈ ( topGen ‘ 𝐵 ) → ∪ ( 𝐵 ∩ 𝒫 𝐴 ) ⊆ 𝐴 )
10	4 9	eqssd	⊢ ( 𝐴 ∈ ( topGen ‘ 𝐵 ) → 𝐴 = ∪ ( 𝐵 ∩ 𝒫 𝐴 ) )