Theorem tgval

Description: The topology generated by a basis. See also tgval2 and tgval3 . (Contributed by NM, 16-Jul-2006) (Revised by Mario Carneiro, 10-Jan-2015)

	Ref	Expression
Assertion	tgval	⊢ ( 𝐵 ∈ 𝑉 → ( topGen ‘ 𝐵 ) = { 𝑥 ∣ 𝑥 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) } )

Proof

Step	Hyp	Ref	Expression
1		df-topgen	⊢ topGen = ( 𝑦 ∈ V ↦ { 𝑥 ∣ 𝑥 ⊆ ∪ ( 𝑦 ∩ 𝒫 𝑥 ) } )
2		ineq1	⊢ ( 𝑦 = 𝐵 → ( 𝑦 ∩ 𝒫 𝑥 ) = ( 𝐵 ∩ 𝒫 𝑥 ) )
3	2	unieqd	⊢ ( 𝑦 = 𝐵 → ∪ ( 𝑦 ∩ 𝒫 𝑥 ) = ∪ ( 𝐵 ∩ 𝒫 𝑥 ) )
4	3	sseq2d	⊢ ( 𝑦 = 𝐵 → ( 𝑥 ⊆ ∪ ( 𝑦 ∩ 𝒫 𝑥 ) ↔ 𝑥 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) ) )
5	4	abbidv	⊢ ( 𝑦 = 𝐵 → { 𝑥 ∣ 𝑥 ⊆ ∪ ( 𝑦 ∩ 𝒫 𝑥 ) } = { 𝑥 ∣ 𝑥 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) } )
6		elex	⊢ ( 𝐵 ∈ 𝑉 → 𝐵 ∈ V )
7		uniexg	⊢ ( 𝐵 ∈ 𝑉 → ∪ 𝐵 ∈ V )
8		abssexg	⊢ ( ∪ 𝐵 ∈ V → { 𝑥 ∣ ( 𝑥 ⊆ ∪ 𝐵 ∧ 𝑥 ⊆ ∪ 𝒫 𝑥 ) } ∈ V )
9		uniin	⊢ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) ⊆ ( ∪ 𝐵 ∩ ∪ 𝒫 𝑥 )
10		sstr	⊢ ( ( 𝑥 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) ∧ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) ⊆ ( ∪ 𝐵 ∩ ∪ 𝒫 𝑥 ) ) → 𝑥 ⊆ ( ∪ 𝐵 ∩ ∪ 𝒫 𝑥 ) )
11	9 10	mpan2	⊢ ( 𝑥 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) → 𝑥 ⊆ ( ∪ 𝐵 ∩ ∪ 𝒫 𝑥 ) )
12		ssin	⊢ ( ( 𝑥 ⊆ ∪ 𝐵 ∧ 𝑥 ⊆ ∪ 𝒫 𝑥 ) ↔ 𝑥 ⊆ ( ∪ 𝐵 ∩ ∪ 𝒫 𝑥 ) )
13	11 12	sylibr	⊢ ( 𝑥 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) → ( 𝑥 ⊆ ∪ 𝐵 ∧ 𝑥 ⊆ ∪ 𝒫 𝑥 ) )
14	13	ss2abi	⊢ { 𝑥 ∣ 𝑥 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) } ⊆ { 𝑥 ∣ ( 𝑥 ⊆ ∪ 𝐵 ∧ 𝑥 ⊆ ∪ 𝒫 𝑥 ) }
15		ssexg	⊢ ( ( { 𝑥 ∣ 𝑥 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) } ⊆ { 𝑥 ∣ ( 𝑥 ⊆ ∪ 𝐵 ∧ 𝑥 ⊆ ∪ 𝒫 𝑥 ) } ∧ { 𝑥 ∣ ( 𝑥 ⊆ ∪ 𝐵 ∧ 𝑥 ⊆ ∪ 𝒫 𝑥 ) } ∈ V ) → { 𝑥 ∣ 𝑥 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) } ∈ V )
16	14 15	mpan	⊢ ( { 𝑥 ∣ ( 𝑥 ⊆ ∪ 𝐵 ∧ 𝑥 ⊆ ∪ 𝒫 𝑥 ) } ∈ V → { 𝑥 ∣ 𝑥 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) } ∈ V )
17	7 8 16	3syl	⊢ ( 𝐵 ∈ 𝑉 → { 𝑥 ∣ 𝑥 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) } ∈ V )
18	1 5 6 17	fvmptd3	⊢ ( 𝐵 ∈ 𝑉 → ( topGen ‘ 𝐵 ) = { 𝑥 ∣ 𝑥 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) } )