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 ∈ B C ∈ 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 ∈ B y ∈ 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 ∈ B y ∈ x ∧ x ⊆ A ↔ ∃ x ∈ B C ∈ x ∧ x ⊆ A
6 5 rspccv ⊢ ∀ y ∈ A ∃ x ∈ B y ∈ x ∧ x ⊆ A → C ∈ A → ∃ x ∈ B C ∈ x ∧ x ⊆ A
7 2 6 biimtrdi ⊢ B ∈ dom ⁡ topGen → A ∈ topGen ⁡ B → C ∈ A → ∃ x ∈ B C ∈ x ∧ x ⊆ A
8 1 7 mpcom ⊢ A ∈ topGen ⁡ B → C ∈ A → ∃ x ∈ B C ∈ x ∧ x ⊆ A
9 8 imp ⊢ A ∈ topGen ⁡ B ∧ C ∈ A → ∃ x ∈ B C ∈ x ∧ x ⊆ A