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

Metamath Proof Explorer

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 ‘ 𝐵 ) ↔ ∃ 𝑥 ( 𝑥 ⊆ 𝐵 ∧ 𝐴 = ∪ 𝑥 ) ) )