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

Metamath Proof Explorer

Theorem 2basgen

Description: Conditions that determine the equality of two generated topologies. (Contributed by NM, 8-May-2007) (Revised by Mario Carneiro, 2-Sep-2015)

Ref Expression
Assertion 2basgen ( ( 𝐵 ⊆ 𝐶 ∧ 𝐶 ⊆ ( topGen ‘ 𝐵 ) ) → ( topGen ‘ 𝐵 ) = ( topGen ‘ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 fvex ⊢ ( topGen ‘ 𝐵 ) ∈ V
2 1 ssex ⊢ ( 𝐶 ⊆ ( topGen ‘ 𝐵 ) → 𝐶 ∈ V )
3 simpl ⊢ ( ( 𝐵 ⊆ 𝐶 ∧ 𝐶 ⊆ ( topGen ‘ 𝐵 ) ) → 𝐵 ⊆ 𝐶 )
4 tgss ⊢ ( ( 𝐶 ∈ V ∧ 𝐵 ⊆ 𝐶 ) → ( topGen ‘ 𝐵 ) ⊆ ( topGen ‘ 𝐶 ) )
5 2 3 4 syl2an2 ⊢ ( ( 𝐵 ⊆ 𝐶 ∧ 𝐶 ⊆ ( topGen ‘ 𝐵 ) ) → ( topGen ‘ 𝐵 ) ⊆ ( topGen ‘ 𝐶 ) )
6 simpr ⊢ ( ( 𝐵 ⊆ 𝐶 ∧ 𝐶 ⊆ ( topGen ‘ 𝐵 ) ) → 𝐶 ⊆ ( topGen ‘ 𝐵 ) )
7 ssexg ⊢ ( ( 𝐵 ⊆ 𝐶 ∧ 𝐶 ∈ V ) → 𝐵 ∈ V )
8 2 7 sylan2 ⊢ ( ( 𝐵 ⊆ 𝐶 ∧ 𝐶 ⊆ ( topGen ‘ 𝐵 ) ) → 𝐵 ∈ V )
9 tgss3 ⊢ ( ( 𝐶 ∈ V ∧ 𝐵 ∈ V ) → ( ( topGen ‘ 𝐶 ) ⊆ ( topGen ‘ 𝐵 ) ↔ 𝐶 ⊆ ( topGen ‘ 𝐵 ) ) )
10 2 8 9 syl2an2 ⊢ ( ( 𝐵 ⊆ 𝐶 ∧ 𝐶 ⊆ ( topGen ‘ 𝐵 ) ) → ( ( topGen ‘ 𝐶 ) ⊆ ( topGen ‘ 𝐵 ) ↔ 𝐶 ⊆ ( topGen ‘ 𝐵 ) ) )
11 6 10 mpbird ⊢ ( ( 𝐵 ⊆ 𝐶 ∧ 𝐶 ⊆ ( topGen ‘ 𝐵 ) ) → ( topGen ‘ 𝐶 ) ⊆ ( topGen ‘ 𝐵 ) )
12 5 11 eqssd ⊢ ( ( 𝐵 ⊆ 𝐶 ∧ 𝐶 ⊆ ( topGen ‘ 𝐵 ) ) → ( topGen ‘ 𝐵 ) = ( topGen ‘ 𝐶 ) )