Metamath Proof Explorer

Theorem eltg2

Description: Membership in a topology generated by a basis. (Contributed by NM, 15-Jul-2006) (Revised by Mario Carneiro, 10-Jan-2015)

Ref Expression
Assertion eltg2 ⊢ B ∈ V → A ∈ topGen ⁡ B ↔ A ⊆ ⋃ B ∧ ∀ x ∈ A ∃ y ∈ B x ∈ y ∧ y ⊆ A

Proof

Step Hyp Ref Expression
1 tgval2 ⊢ B ∈ V → topGen ⁡ B = z | z ⊆ ⋃ B ∧ ∀ x ∈ z ∃ y ∈ B x ∈ y ∧ y ⊆ z
2 1 eleq2d ⊢ B ∈ V → A ∈ topGen ⁡ B ↔ A ∈ z | z ⊆ ⋃ B ∧ ∀ x ∈ z ∃ y ∈ B x ∈ y ∧ y ⊆ z
3 elex ⊢ A ∈ z | z ⊆ ⋃ B ∧ ∀ x ∈ z ∃ y ∈ B x ∈ y ∧ y ⊆ z → A ∈ V
4 3 adantl ⊢ B ∈ V ∧ A ∈ z | z ⊆ ⋃ B ∧ ∀ x ∈ z ∃ y ∈ B x ∈ y ∧ y ⊆ z → A ∈ V
5 uniexg ⊢ B ∈ V → ⋃ B ∈ V
6 ssexg ⊢ A ⊆ ⋃ B ∧ ⋃ B ∈ V → A ∈ V
7 5 6 sylan2 ⊢ A ⊆ ⋃ B ∧ B ∈ V → A ∈ V
8 7 ancoms ⊢ B ∈ V ∧ A ⊆ ⋃ B → A ∈ V
9 8 adantrr ⊢ B ∈ V ∧ A ⊆ ⋃ B ∧ ∀ x ∈ A ∃ y ∈ B x ∈ y ∧ y ⊆ A → A ∈ V
10 sseq1 ⊢ z = A → z ⊆ ⋃ B ↔ A ⊆ ⋃ B
11 sseq2 ⊢ z = A → y ⊆ z ↔ y ⊆ A
12 11 anbi2d ⊢ z = A → x ∈ y ∧ y ⊆ z ↔ x ∈ y ∧ y ⊆ A
13 12 rexbidv ⊢ z = A → ∃ y ∈ B x ∈ y ∧ y ⊆ z ↔ ∃ y ∈ B x ∈ y ∧ y ⊆ A
14 13 raleqbi1dv ⊢ z = A → ∀ x ∈ z ∃ y ∈ B x ∈ y ∧ y ⊆ z ↔ ∀ x ∈ A ∃ y ∈ B x ∈ y ∧ y ⊆ A
15 10 14 anbi12d ⊢ z = A → z ⊆ ⋃ B ∧ ∀ x ∈ z ∃ y ∈ B x ∈ y ∧ y ⊆ z ↔ A ⊆ ⋃ B ∧ ∀ x ∈ A ∃ y ∈ B x ∈ y ∧ y ⊆ A
16 15 elabg ⊢ A ∈ V → A ∈ z | z ⊆ ⋃ B ∧ ∀ x ∈ z ∃ y ∈ B x ∈ y ∧ y ⊆ z ↔ A ⊆ ⋃ B ∧ ∀ x ∈ A ∃ y ∈ B x ∈ y ∧ y ⊆ A
17 4 9 16 pm5.21nd ⊢ B ∈ V → A ∈ z | z ⊆ ⋃ B ∧ ∀ x ∈ z ∃ y ∈ B x ∈ y ∧ y ⊆ z ↔ A ⊆ ⋃ B ∧ ∀ x ∈ A ∃ y ∈ B x ∈ y ∧ y ⊆ A
18 2 17 bitrd ⊢ B ∈ V → A ∈ topGen ⁡ B ↔ A ⊆ ⋃ B ∧ ∀ x ∈ A ∃ y ∈ B x ∈ y ∧ y ⊆ A