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

Metamath Proof Explorer

Theorem eltg2b

Description: Membership in a topology generated by a basis. (Contributed by Mario Carneiro, 17-Jun-2014) (Revised by Mario Carneiro, 10-Jan-2015)

Ref Expression
Assertion eltg2b ( 𝐵 ∈ 𝑉 → ( 𝐴 ∈ ( topGen ‘ 𝐵 ) ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 eltg2 ⊢ ( 𝐵 ∈ 𝑉 → ( 𝐴 ∈ ( topGen ‘ 𝐵 ) ↔ ( 𝐴 ⊆ ∪ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝐴 ) ) ) )
2 simpl ⊢ ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝐴 ) → 𝑥 ∈ 𝑦 )
3 2 reximi ⊢ ( ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝐴 ) → ∃ 𝑦 ∈ 𝐵 𝑥 ∈ 𝑦 )
4 eluni2 ⊢ ( 𝑥 ∈ ∪ 𝐵 ↔ ∃ 𝑦 ∈ 𝐵 𝑥 ∈ 𝑦 )
5 3 4 sylibr ⊢ ( ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝐴 ) → 𝑥 ∈ ∪ 𝐵 )
6 5 ralimi ⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝐴 ) → ∀ 𝑥 ∈ 𝐴 𝑥 ∈ ∪ 𝐵 )
7 dfss3 ⊢ ( 𝐴 ⊆ ∪ 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ ∪ 𝐵 )
8 6 7 sylibr ⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝐴 ) → 𝐴 ⊆ ∪ 𝐵 )
9 8 pm4.71ri ⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝐴 ) ↔ ( 𝐴 ⊆ ∪ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝐴 ) ) )
10 1 9 bitr4di ⊢ ( 𝐵 ∈ 𝑉 → ( 𝐴 ∈ ( topGen ‘ 𝐵 ) ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝐴 ) ) )