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

Metamath Proof Explorer

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