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 ( ( 𝐽 ∈ Top ∧ 𝐵𝐽 ) → ( ( topGen ‘ 𝐵 ) = 𝐽 ↔ ∀ 𝑥𝐽𝑦 ( 𝑦𝐵𝑥 = 𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 tgss ( ( 𝐽 ∈ Top ∧ 𝐵𝐽 ) → ( topGen ‘ 𝐵 ) ⊆ ( topGen ‘ 𝐽 ) )
2 tgtop ( 𝐽 ∈ Top → ( topGen ‘ 𝐽 ) = 𝐽 )
3 2 adantr ( ( 𝐽 ∈ Top ∧ 𝐵𝐽 ) → ( topGen ‘ 𝐽 ) = 𝐽 )
4 1 3 sseqtrd ( ( 𝐽 ∈ Top ∧ 𝐵𝐽 ) → ( topGen ‘ 𝐵 ) ⊆ 𝐽 )
5 eqss ( ( topGen ‘ 𝐵 ) = 𝐽 ↔ ( ( topGen ‘ 𝐵 ) ⊆ 𝐽𝐽 ⊆ ( topGen ‘ 𝐵 ) ) )
6 5 baib ( ( topGen ‘ 𝐵 ) ⊆ 𝐽 → ( ( topGen ‘ 𝐵 ) = 𝐽𝐽 ⊆ ( topGen ‘ 𝐵 ) ) )
7 4 6 syl ( ( 𝐽 ∈ Top ∧ 𝐵𝐽 ) → ( ( topGen ‘ 𝐵 ) = 𝐽𝐽 ⊆ ( topGen ‘ 𝐵 ) ) )
8 dfss3 ( 𝐽 ⊆ ( topGen ‘ 𝐵 ) ↔ ∀ 𝑥𝐽 𝑥 ∈ ( topGen ‘ 𝐵 ) )
9 7 8 bitrdi ( ( 𝐽 ∈ Top ∧ 𝐵𝐽 ) → ( ( topGen ‘ 𝐵 ) = 𝐽 ↔ ∀ 𝑥𝐽 𝑥 ∈ ( topGen ‘ 𝐵 ) ) )
10 ssexg ( ( 𝐵𝐽𝐽 ∈ Top ) → 𝐵 ∈ V )
11 10 ancoms ( ( 𝐽 ∈ Top ∧ 𝐵𝐽 ) → 𝐵 ∈ V )
12 eltg3 ( 𝐵 ∈ V → ( 𝑥 ∈ ( topGen ‘ 𝐵 ) ↔ ∃ 𝑦 ( 𝑦𝐵𝑥 = 𝑦 ) ) )
13 11 12 syl ( ( 𝐽 ∈ Top ∧ 𝐵𝐽 ) → ( 𝑥 ∈ ( topGen ‘ 𝐵 ) ↔ ∃ 𝑦 ( 𝑦𝐵𝑥 = 𝑦 ) ) )
14 13 ralbidv ( ( 𝐽 ∈ Top ∧ 𝐵𝐽 ) → ( ∀ 𝑥𝐽 𝑥 ∈ ( topGen ‘ 𝐵 ) ↔ ∀ 𝑥𝐽𝑦 ( 𝑦𝐵𝑥 = 𝑦 ) ) )
15 9 14 bitrd ( ( 𝐽 ∈ Top ∧ 𝐵𝐽 ) → ( ( topGen ‘ 𝐵 ) = 𝐽 ↔ ∀ 𝑥𝐽𝑦 ( 𝑦𝐵𝑥 = 𝑦 ) ) )