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∈Bx∈y∧y⊆A

Proof

Step Hyp Ref Expression
1 tgval2 ⊢B∈V→topGen⁡B=z|z⊆⋃B∧∀x∈z∃y∈Bx∈y∧y⊆z
2 1 eleq2d ⊢B∈V→A∈topGen⁡B↔A∈z|z⊆⋃B∧∀x∈z∃y∈Bx∈y∧y⊆z
3 elex ⊢A∈z|z⊆⋃B∧∀x∈z∃y∈Bx∈y∧y⊆z→A∈V
4 3 adantl ⊢B∈V∧A∈z|z⊆⋃B∧∀x∈z∃y∈Bx∈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∈Bx∈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∈Bx∈y∧y⊆z↔∃y∈Bx∈y∧y⊆A
14 13 raleqbi1dv ⊢z=A→∀x∈z∃y∈Bx∈y∧y⊆z↔∀x∈A∃y∈Bx∈y∧y⊆A
15 10 14 anbi12d ⊢z=A→z⊆⋃B∧∀x∈z∃y∈Bx∈y∧y⊆z↔A⊆⋃B∧∀x∈A∃y∈Bx∈y∧y⊆A
16 15 elabg ⊢A∈V→A∈z|z⊆⋃B∧∀x∈z∃y∈Bx∈y∧y⊆z↔A⊆⋃B∧∀x∈A∃y∈Bx∈y∧y⊆A
17 4 9 16 pm5.21nd ⊢B∈V→A∈z|z⊆⋃B∧∀x∈z∃y∈Bx∈y∧y⊆z↔A⊆⋃B∧∀x∈A∃y∈Bx∈y∧y⊆A
18 2 17 bitrd ⊢B∈V→A∈topGen⁡B↔A⊆⋃B∧∀x∈A∃y∈Bx∈y∧y⊆A