This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ‘ 𝐵 ) = 𝐽 ↔ ∀ 𝑥 ∈ 𝐽 ∃ 𝑦 ( 𝑦 ⊆ 𝐵 ∧ 𝑥 = ∪ 𝑦 ) ) )