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 ⊢ B ⊆ C ∧ C ⊆ topGen ⁡ B → topGen ⁡ B = topGen ⁡ C

Proof

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