Metamath Proof Explorer

Theorem isbasis3g

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

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

Proof

Step Hyp Ref Expression
1 isbasis2g ⊢B∈C→B∈TopBases↔∀x∈B∀y∈B∀z∈x∩y∃w∈Bz∈w∧w⊆x∩y
2 elssuni ⊢x∈B→x⊆⋃B
3 2 rgen ⊢∀x∈Bx⊆⋃B
4 eluni2 ⊢x∈⋃B↔∃y∈Bx∈y
5 4 biimpi ⊢x∈⋃B→∃y∈Bx∈y
6 5 rgen ⊢∀x∈⋃B∃y∈Bx∈y
7 3 6 pm3.2i ⊢∀x∈Bx⊆⋃B∧∀x∈⋃B∃y∈Bx∈y
8 7 biantrur ⊢∀x∈B∀y∈B∀z∈x∩y∃w∈Bz∈w∧w⊆x∩y↔∀x∈Bx⊆⋃B∧∀x∈⋃B∃y∈Bx∈y∧∀x∈B∀y∈B∀z∈x∩y∃w∈Bz∈w∧w⊆x∩y
9 df-3an ⊢∀x∈Bx⊆⋃B∧∀x∈⋃B∃y∈Bx∈y∧∀x∈B∀y∈B∀z∈x∩y∃w∈Bz∈w∧w⊆x∩y↔∀x∈Bx⊆⋃B∧∀x∈⋃B∃y∈Bx∈y∧∀x∈B∀y∈B∀z∈x∩y∃w∈Bz∈w∧w⊆x∩y
10 8 9 bitr4i ⊢∀x∈B∀y∈B∀z∈x∩y∃w∈Bz∈w∧w⊆x∩y↔∀x∈Bx⊆⋃B∧∀x∈⋃B∃y∈Bx∈y∧∀x∈B∀y∈B∀z∈x∩y∃w∈Bz∈w∧w⊆x∩y
11 1 10 bitrdi ⊢B∈C→B∈TopBases↔∀x∈Bx⊆⋃B∧∀x∈⋃B∃y∈Bx∈y∧∀x∈B∀y∈B∀z∈x∩y∃w∈Bz∈w∧w⊆x∩y