Metamath Proof Explorer

Theorem isbasis2g

Description: Express the predicate "the set B is a basis for a topology". (Contributed by NM, 17-Jul-2006)

Ref Expression
Assertion isbasis2g ⊢B∈C→B∈TopBases↔∀x∈B∀y∈B∀z∈x∩y∃w∈Bz∈w∧w⊆x∩y

Proof

Step Hyp Ref Expression
1 isbasisg ⊢B∈C→B∈TopBases↔∀x∈B∀y∈Bx∩y⊆⋃B∩𝒫x∩y
2 dfss3 ⊢x∩y⊆⋃B∩𝒫x∩y↔∀z∈x∩yz∈⋃B∩𝒫x∩y
3 elin ⊢w∈B∩𝒫x∩y↔w∈B∧w∈𝒫x∩y
4 velpw ⊢w∈𝒫x∩y↔w⊆x∩y
5 4 anbi2i ⊢w∈B∧w∈𝒫x∩y↔w∈B∧w⊆x∩y
6 3 5 bitri ⊢w∈B∩𝒫x∩y↔w∈B∧w⊆x∩y
7 6 anbi2i ⊢z∈w∧w∈B∩𝒫x∩y↔z∈w∧w∈B∧w⊆x∩y
8 an12 ⊢z∈w∧w∈B∧w⊆x∩y↔w∈B∧z∈w∧w⊆x∩y
9 7 8 bitri ⊢z∈w∧w∈B∩𝒫x∩y↔w∈B∧z∈w∧w⊆x∩y
10 9 exbii ⊢∃wz∈w∧w∈B∩𝒫x∩y↔∃ww∈B∧z∈w∧w⊆x∩y
11 eluni ⊢z∈⋃B∩𝒫x∩y↔∃wz∈w∧w∈B∩𝒫x∩y
12 df-rex ⊢∃w∈Bz∈w∧w⊆x∩y↔∃ww∈B∧z∈w∧w⊆x∩y
13 10 11 12 3bitr4i ⊢z∈⋃B∩𝒫x∩y↔∃w∈Bz∈w∧w⊆x∩y
14 13 ralbii ⊢∀z∈x∩yz∈⋃B∩𝒫x∩y↔∀z∈x∩y∃w∈Bz∈w∧w⊆x∩y
15 2 14 bitri ⊢x∩y⊆⋃B∩𝒫x∩y↔∀z∈x∩y∃w∈Bz∈w∧w⊆x∩y
16 15 2ralbii ⊢∀x∈B∀y∈Bx∩y⊆⋃B∩𝒫x∩y↔∀x∈B∀y∈B∀z∈x∩y∃w∈Bz∈w∧w⊆x∩y
17 1 16 bitrdi ⊢B∈C→B∈TopBases↔∀x∈B∀y∈B∀z∈x∩y∃w∈Bz∈w∧w⊆x∩y