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 ‘ 𝐶 ) )