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