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

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 ( ( 𝐴 ∈ ( topGen ‘ 𝐵 ) ∧ 𝐶 ∈ 𝐴 ) → ∃ 𝑥 ∈ 𝐵 ( 𝐶 ∈ 𝑥 ∧ 𝑥 ⊆ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 elfvdm ⊢ ( 𝐴 ∈ ( topGen ‘ 𝐵 ) → 𝐵 ∈ dom topGen )
2 eltg2b ⊢ ( 𝐵 ∈ dom topGen → ( 𝐴 ∈ ( topGen ‘ 𝐵 ) ↔ ∀ 𝑦 ∈ 𝐴 ∃ 𝑥 ∈ 𝐵 ( 𝑦 ∈ 𝑥 ∧ 𝑥 ⊆ 𝐴 ) ) )
3 eleq1 ⊢ ( 𝑦 = 𝐶 → ( 𝑦 ∈ 𝑥 ↔ 𝐶 ∈ 𝑥 ) )
4 3 anbi1d ⊢ ( 𝑦 = 𝐶 → ( ( 𝑦 ∈ 𝑥 ∧ 𝑥 ⊆ 𝐴 ) ↔ ( 𝐶 ∈ 𝑥 ∧ 𝑥 ⊆ 𝐴 ) ) )
5 4 rexbidv ⊢ ( 𝑦 = 𝐶 → ( ∃ 𝑥 ∈ 𝐵 ( 𝑦 ∈ 𝑥 ∧ 𝑥 ⊆ 𝐴 ) ↔ ∃ 𝑥 ∈ 𝐵 ( 𝐶 ∈ 𝑥 ∧ 𝑥 ⊆ 𝐴 ) ) )
6 5 rspccv ⊢ ( ∀ 𝑦 ∈ 𝐴 ∃ 𝑥 ∈ 𝐵 ( 𝑦 ∈ 𝑥 ∧ 𝑥 ⊆ 𝐴 ) → ( 𝐶 ∈ 𝐴 → ∃ 𝑥 ∈ 𝐵 ( 𝐶 ∈ 𝑥 ∧ 𝑥 ⊆ 𝐴 ) ) )
7 2 6 biimtrdi ⊢ ( 𝐵 ∈ dom topGen → ( 𝐴 ∈ ( topGen ‘ 𝐵 ) → ( 𝐶 ∈ 𝐴 → ∃ 𝑥 ∈ 𝐵 ( 𝐶 ∈ 𝑥 ∧ 𝑥 ⊆ 𝐴 ) ) ) )
8 1 7 mpcom ⊢ ( 𝐴 ∈ ( topGen ‘ 𝐵 ) → ( 𝐶 ∈ 𝐴 → ∃ 𝑥 ∈ 𝐵 ( 𝐶 ∈ 𝑥 ∧ 𝑥 ⊆ 𝐴 ) ) )
9 8 imp ⊢ ( ( 𝐴 ∈ ( topGen ‘ 𝐵 ) ∧ 𝐶 ∈ 𝐴 ) → ∃ 𝑥 ∈ 𝐵 ( 𝐶 ∈ 𝑥 ∧ 𝑥 ⊆ 𝐴 ) )