Theorem eltg

Description: Membership in a topology generated by a basis. (Contributed by NM, 16-Jul-2006) (Revised by Mario Carneiro, 10-Jan-2015)

	Ref	Expression
Assertion	eltg	⊢ ( 𝐵 ∈ 𝑉 → ( 𝐴 ∈ ( topGen ‘ 𝐵 ) ↔ 𝐴 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		tgval	⊢ ( 𝐵 ∈ 𝑉 → ( topGen ‘ 𝐵 ) = { 𝑥 ∣ 𝑥 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) } )
2	1	eleq2d	⊢ ( 𝐵 ∈ 𝑉 → ( 𝐴 ∈ ( topGen ‘ 𝐵 ) ↔ 𝐴 ∈ { 𝑥 ∣ 𝑥 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) } ) )
3		elex	⊢ ( 𝐴 ∈ { 𝑥 ∣ 𝑥 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) } → 𝐴 ∈ V )
4	3	adantl	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐴 ∈ { 𝑥 ∣ 𝑥 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) } ) → 𝐴 ∈ V )
5		inex1g	⊢ ( 𝐵 ∈ 𝑉 → ( 𝐵 ∩ 𝒫 𝐴 ) ∈ V )
6	5	uniexd	⊢ ( 𝐵 ∈ 𝑉 → ∪ ( 𝐵 ∩ 𝒫 𝐴 ) ∈ V )
7		ssexg	⊢ ( ( 𝐴 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝐴 ) ∧ ∪ ( 𝐵 ∩ 𝒫 𝐴 ) ∈ V ) → 𝐴 ∈ V )
8	6 7	sylan2	⊢ ( ( 𝐴 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝐴 ) ∧ 𝐵 ∈ 𝑉 ) → 𝐴 ∈ V )
9	8	ancoms	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐴 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝐴 ) ) → 𝐴 ∈ V )
10		id	⊢ ( 𝑥 = 𝐴 → 𝑥 = 𝐴 )
11		pweq	⊢ ( 𝑥 = 𝐴 → 𝒫 𝑥 = 𝒫 𝐴 )
12	11	ineq2d	⊢ ( 𝑥 = 𝐴 → ( 𝐵 ∩ 𝒫 𝑥 ) = ( 𝐵 ∩ 𝒫 𝐴 ) )
13	12	unieqd	⊢ ( 𝑥 = 𝐴 → ∪ ( 𝐵 ∩ 𝒫 𝑥 ) = ∪ ( 𝐵 ∩ 𝒫 𝐴 ) )
14	10 13	sseq12d	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) ↔ 𝐴 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝐴 ) ) )
15	14	elabg	⊢ ( 𝐴 ∈ V → ( 𝐴 ∈ { 𝑥 ∣ 𝑥 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) } ↔ 𝐴 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝐴 ) ) )
16	4 9 15	pm5.21nd	⊢ ( 𝐵 ∈ 𝑉 → ( 𝐴 ∈ { 𝑥 ∣ 𝑥 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) } ↔ 𝐴 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝐴 ) ) )
17	2 16	bitrd	⊢ ( 𝐵 ∈ 𝑉 → ( 𝐴 ∈ ( topGen ‘ 𝐵 ) ↔ 𝐴 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝐴 ) ) )