Theorem bastop2

Description: A version of bastop1 that doesn't have B C_ J in the antecedent. (Contributed by NM, 3-Feb-2008)

	Ref	Expression
Assertion	bastop2	⊢ ( 𝐽 ∈ Top → ( ( topGen ‘ 𝐵 ) = 𝐽 ↔ ( 𝐵 ⊆ 𝐽 ∧ ∀ 𝑥 ∈ 𝐽 ∃ 𝑦 ( 𝑦 ⊆ 𝐵 ∧ 𝑥 = ∪ 𝑦 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		eleq1	⊢ ( ( topGen ‘ 𝐵 ) = 𝐽 → ( ( topGen ‘ 𝐵 ) ∈ Top ↔ 𝐽 ∈ Top ) )
2	1	biimparc	⊢ ( ( 𝐽 ∈ Top ∧ ( topGen ‘ 𝐵 ) = 𝐽 ) → ( topGen ‘ 𝐵 ) ∈ Top )
3		tgclb	⊢ ( 𝐵 ∈ TopBases ↔ ( topGen ‘ 𝐵 ) ∈ Top )
4	2 3	sylibr	⊢ ( ( 𝐽 ∈ Top ∧ ( topGen ‘ 𝐵 ) = 𝐽 ) → 𝐵 ∈ TopBases )
5		bastg	⊢ ( 𝐵 ∈ TopBases → 𝐵 ⊆ ( topGen ‘ 𝐵 ) )
6	4 5	syl	⊢ ( ( 𝐽 ∈ Top ∧ ( topGen ‘ 𝐵 ) = 𝐽 ) → 𝐵 ⊆ ( topGen ‘ 𝐵 ) )
7		simpr	⊢ ( ( 𝐽 ∈ Top ∧ ( topGen ‘ 𝐵 ) = 𝐽 ) → ( topGen ‘ 𝐵 ) = 𝐽 )
8	6 7	sseqtrd	⊢ ( ( 𝐽 ∈ Top ∧ ( topGen ‘ 𝐵 ) = 𝐽 ) → 𝐵 ⊆ 𝐽 )
9	8	ex	⊢ ( 𝐽 ∈ Top → ( ( topGen ‘ 𝐵 ) = 𝐽 → 𝐵 ⊆ 𝐽 ) )
10	9	pm4.71rd	⊢ ( 𝐽 ∈ Top → ( ( topGen ‘ 𝐵 ) = 𝐽 ↔ ( 𝐵 ⊆ 𝐽 ∧ ( topGen ‘ 𝐵 ) = 𝐽 ) ) )
11		bastop1	⊢ ( ( 𝐽 ∈ Top ∧ 𝐵 ⊆ 𝐽 ) → ( ( topGen ‘ 𝐵 ) = 𝐽 ↔ ∀ 𝑥 ∈ 𝐽 ∃ 𝑦 ( 𝑦 ⊆ 𝐵 ∧ 𝑥 = ∪ 𝑦 ) ) )
12	11	pm5.32da	⊢ ( 𝐽 ∈ Top → ( ( 𝐵 ⊆ 𝐽 ∧ ( topGen ‘ 𝐵 ) = 𝐽 ) ↔ ( 𝐵 ⊆ 𝐽 ∧ ∀ 𝑥 ∈ 𝐽 ∃ 𝑦 ( 𝑦 ⊆ 𝐵 ∧ 𝑥 = ∪ 𝑦 ) ) ) )
13	10 12	bitrd	⊢ ( 𝐽 ∈ Top → ( ( topGen ‘ 𝐵 ) = 𝐽 ↔ ( 𝐵 ⊆ 𝐽 ∧ ∀ 𝑥 ∈ 𝐽 ∃ 𝑦 ( 𝑦 ⊆ 𝐵 ∧ 𝑥 = ∪ 𝑦 ) ) ) )