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 ⊢ B ∈ V → A ∈ topGen ⁡ B ↔ ∀ x ∈ A ∃ y ∈ B x ∈ y ∧ y ⊆ A

Proof

Step Hyp Ref Expression
1 eltg2 ⊢ B ∈ V → A ∈ topGen ⁡ B ↔ A ⊆ ⋃ B ∧ ∀ x ∈ A ∃ y ∈ B x ∈ y ∧ y ⊆ A
2 simpl ⊢ x ∈ y ∧ y ⊆ A → x ∈ y
3 2 reximi ⊢ ∃ y ∈ B x ∈ y ∧ y ⊆ A → ∃ y ∈ B x ∈ y
4 eluni2 ⊢ x ∈ ⋃ B ↔ ∃ y ∈ B x ∈ y
5 3 4 sylibr ⊢ ∃ y ∈ B x ∈ y ∧ y ⊆ A → x ∈ ⋃ B
6 5 ralimi ⊢ ∀ x ∈ A ∃ y ∈ B x ∈ y ∧ y ⊆ A → ∀ x ∈ A x ∈ ⋃ B
7 dfss3 ⊢ A ⊆ ⋃ B ↔ ∀ x ∈ A x ∈ ⋃ B
8 6 7 sylibr ⊢ ∀ x ∈ A ∃ y ∈ B x ∈ y ∧ y ⊆ A → A ⊆ ⋃ B
9 8 pm4.71ri ⊢ ∀ x ∈ A ∃ y ∈ B x ∈ y ∧ y ⊆ A ↔ A ⊆ ⋃ B ∧ ∀ x ∈ A ∃ y ∈ B x ∈ y ∧ y ⊆ A
10 1 9 bitr4di ⊢ B ∈ V → A ∈ topGen ⁡ B ↔ ∀ x ∈ A ∃ y ∈ B x ∈ y ∧ y ⊆ A