Theorem eltg3

Description: Membership in a topology generated by a basis. (Contributed by NM, 15-Jul-2006) (Proof shortened by Mario Carneiro, 30-Aug-2015)

	Ref	Expression
Assertion	eltg3	⊢ ( 𝐵 ∈ 𝑉 → ( 𝐴 ∈ ( topGen ‘ 𝐵 ) ↔ ∃ 𝑥 ( 𝑥 ⊆ 𝐵 ∧ 𝐴 = ∪ 𝑥 ) ) )

Proof

Step	Hyp	Ref	Expression
1		elfvdm	⊢ ( 𝐴 ∈ ( topGen ‘ 𝐵 ) → 𝐵 ∈ dom topGen )
2		inex1g	⊢ ( 𝐵 ∈ dom topGen → ( 𝐵 ∩ 𝒫 𝐴 ) ∈ V )
3	1 2	syl	⊢ ( 𝐴 ∈ ( topGen ‘ 𝐵 ) → ( 𝐵 ∩ 𝒫 𝐴 ) ∈ V )
4		eltg4i	⊢ ( 𝐴 ∈ ( topGen ‘ 𝐵 ) → 𝐴 = ∪ ( 𝐵 ∩ 𝒫 𝐴 ) )
5		inss1	⊢ ( 𝐵 ∩ 𝒫 𝐴 ) ⊆ 𝐵
6		sseq1	⊢ ( 𝑥 = ( 𝐵 ∩ 𝒫 𝐴 ) → ( 𝑥 ⊆ 𝐵 ↔ ( 𝐵 ∩ 𝒫 𝐴 ) ⊆ 𝐵 ) )
7	5 6	mpbiri	⊢ ( 𝑥 = ( 𝐵 ∩ 𝒫 𝐴 ) → 𝑥 ⊆ 𝐵 )
8	7	biantrurd	⊢ ( 𝑥 = ( 𝐵 ∩ 𝒫 𝐴 ) → ( 𝐴 = ∪ 𝑥 ↔ ( 𝑥 ⊆ 𝐵 ∧ 𝐴 = ∪ 𝑥 ) ) )
9		unieq	⊢ ( 𝑥 = ( 𝐵 ∩ 𝒫 𝐴 ) → ∪ 𝑥 = ∪ ( 𝐵 ∩ 𝒫 𝐴 ) )
10	9	eqeq2d	⊢ ( 𝑥 = ( 𝐵 ∩ 𝒫 𝐴 ) → ( 𝐴 = ∪ 𝑥 ↔ 𝐴 = ∪ ( 𝐵 ∩ 𝒫 𝐴 ) ) )
11	8 10	bitr3d	⊢ ( 𝑥 = ( 𝐵 ∩ 𝒫 𝐴 ) → ( ( 𝑥 ⊆ 𝐵 ∧ 𝐴 = ∪ 𝑥 ) ↔ 𝐴 = ∪ ( 𝐵 ∩ 𝒫 𝐴 ) ) )
12	3 4 11	spcedv	⊢ ( 𝐴 ∈ ( topGen ‘ 𝐵 ) → ∃ 𝑥 ( 𝑥 ⊆ 𝐵 ∧ 𝐴 = ∪ 𝑥 ) )
13		eltg3i	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝑥 ⊆ 𝐵 ) → ∪ 𝑥 ∈ ( topGen ‘ 𝐵 ) )
14		eleq1	⊢ ( 𝐴 = ∪ 𝑥 → ( 𝐴 ∈ ( topGen ‘ 𝐵 ) ↔ ∪ 𝑥 ∈ ( topGen ‘ 𝐵 ) ) )
15	13 14	syl5ibrcom	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝑥 ⊆ 𝐵 ) → ( 𝐴 = ∪ 𝑥 → 𝐴 ∈ ( topGen ‘ 𝐵 ) ) )
16	15	expimpd	⊢ ( 𝐵 ∈ 𝑉 → ( ( 𝑥 ⊆ 𝐵 ∧ 𝐴 = ∪ 𝑥 ) → 𝐴 ∈ ( topGen ‘ 𝐵 ) ) )
17	16	exlimdv	⊢ ( 𝐵 ∈ 𝑉 → ( ∃ 𝑥 ( 𝑥 ⊆ 𝐵 ∧ 𝐴 = ∪ 𝑥 ) → 𝐴 ∈ ( topGen ‘ 𝐵 ) ) )
18	12 17	impbid2	⊢ ( 𝐵 ∈ 𝑉 → ( 𝐴 ∈ ( topGen ‘ 𝐵 ) ↔ ∃ 𝑥 ( 𝑥 ⊆ 𝐵 ∧ 𝐴 = ∪ 𝑥 ) ) )