Metamath Proof Explorer

Theorem tg2

Description: Property of a member of a topology generated by a basis. (Contributed by NM, 20-Jul-2006)

Ref Expression
Assertion tg2 ⊢A∈topGen⁡B∧C∈A→∃x∈BC∈x∧x⊆A

Proof

Step Hyp Ref Expression
1 elfvdm ⊢A∈topGen⁡B→B∈dom⁡topGen
2 eltg2b ⊢B∈dom⁡topGen→A∈topGen⁡B↔∀y∈A∃x∈By∈x∧x⊆A
3 eleq1 ⊢y=C→y∈x↔C∈x
4 3 anbi1d ⊢y=C→y∈x∧x⊆A↔C∈x∧x⊆A
5 4 rexbidv ⊢y=C→∃x∈By∈x∧x⊆A↔∃x∈BC∈x∧x⊆A
6 5 rspccv ⊢∀y∈A∃x∈By∈x∧x⊆A→C∈A→∃x∈BC∈x∧x⊆A
7 2 6 syl6bi ⊢B∈dom⁡topGen→A∈topGen⁡B→C∈A→∃x∈BC∈x∧x⊆A
8 1 7 mpcom ⊢A∈topGen⁡B→C∈A→∃x∈BC∈x∧x⊆A
9 8 imp ⊢A∈topGen⁡B∧C∈A→∃x∈BC∈x∧x⊆A