Metamath Proof Explorer

Theorem bastop1

Description: A subset of a topology is a basis for the topology iff every member of the topology is a union of members of the basis. We use the idiom " ( topGenB ) = J " to express " B is a basis for topology J " since we do not have a separate notation for this. Definition 15.35 of Schechter p. 428. (Contributed by NM, 2-Feb-2008) (Proof shortened by Mario Carneiro, 2-Sep-2015)

Ref Expression
Assertion bastop1 ⊢ J ∈ Top ∧ B ⊆ J → topGen ⁡ B = J ↔ ∀ x ∈ J ∃ y y ⊆ B ∧ x = ⋃ y

Proof

Step Hyp Ref Expression
1 tgss ⊢ J ∈ Top ∧ B ⊆ J → topGen ⁡ B ⊆ topGen ⁡ J
2 tgtop ⊢ J ∈ Top → topGen ⁡ J = J
3 2 adantr ⊢ J ∈ Top ∧ B ⊆ J → topGen ⁡ J = J
4 1 3 sseqtrd ⊢ J ∈ Top ∧ B ⊆ J → topGen ⁡ B ⊆ J
5 eqss ⊢ topGen ⁡ B = J ↔ topGen ⁡ B ⊆ J ∧ J ⊆ topGen ⁡ B
6 5 baib ⊢ topGen ⁡ B ⊆ J → topGen ⁡ B = J ↔ J ⊆ topGen ⁡ B
7 4 6 syl ⊢ J ∈ Top ∧ B ⊆ J → topGen ⁡ B = J ↔ J ⊆ topGen ⁡ B
8 dfss3 ⊢ J ⊆ topGen ⁡ B ↔ ∀ x ∈ J x ∈ topGen ⁡ B
9 7 8 bitrdi ⊢ J ∈ Top ∧ B ⊆ J → topGen ⁡ B = J ↔ ∀ x ∈ J x ∈ topGen ⁡ B
10 ssexg ⊢ B ⊆ J ∧ J ∈ Top → B ∈ V
11 10 ancoms ⊢ J ∈ Top ∧ B ⊆ J → B ∈ V
12 eltg3 ⊢ B ∈ V → x ∈ topGen ⁡ B ↔ ∃ y y ⊆ B ∧ x = ⋃ y
13 11 12 syl ⊢ J ∈ Top ∧ B ⊆ J → x ∈ topGen ⁡ B ↔ ∃ y y ⊆ B ∧ x = ⋃ y
14 13 ralbidv ⊢ J ∈ Top ∧ B ⊆ J → ∀ x ∈ J x ∈ topGen ⁡ B ↔ ∀ x ∈ J ∃ y y ⊆ B ∧ x = ⋃ y
15 9 14 bitrd ⊢ J ∈ Top ∧ B ⊆ J → topGen ⁡ B = J ↔ ∀ x ∈ J ∃ y y ⊆ B ∧ x = ⋃ y