# 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 ${⊢}\left({B}\subseteq {C}\wedge {C}\subseteq \mathrm{topGen}\left({B}\right)\right)\to \mathrm{topGen}\left({B}\right)=\mathrm{topGen}\left({C}\right)$

### Proof

Step Hyp Ref Expression
1 fvex ${⊢}\mathrm{topGen}\left({B}\right)\in \mathrm{V}$
2 1 ssex ${⊢}{C}\subseteq \mathrm{topGen}\left({B}\right)\to {C}\in \mathrm{V}$
3 simpl ${⊢}\left({B}\subseteq {C}\wedge {C}\subseteq \mathrm{topGen}\left({B}\right)\right)\to {B}\subseteq {C}$
4 tgss ${⊢}\left({C}\in \mathrm{V}\wedge {B}\subseteq {C}\right)\to \mathrm{topGen}\left({B}\right)\subseteq \mathrm{topGen}\left({C}\right)$
5 2 3 4 syl2an2 ${⊢}\left({B}\subseteq {C}\wedge {C}\subseteq \mathrm{topGen}\left({B}\right)\right)\to \mathrm{topGen}\left({B}\right)\subseteq \mathrm{topGen}\left({C}\right)$
6 simpr ${⊢}\left({B}\subseteq {C}\wedge {C}\subseteq \mathrm{topGen}\left({B}\right)\right)\to {C}\subseteq \mathrm{topGen}\left({B}\right)$
7 ssexg ${⊢}\left({B}\subseteq {C}\wedge {C}\in \mathrm{V}\right)\to {B}\in \mathrm{V}$
8 2 7 sylan2 ${⊢}\left({B}\subseteq {C}\wedge {C}\subseteq \mathrm{topGen}\left({B}\right)\right)\to {B}\in \mathrm{V}$
9 tgss3 ${⊢}\left({C}\in \mathrm{V}\wedge {B}\in \mathrm{V}\right)\to \left(\mathrm{topGen}\left({C}\right)\subseteq \mathrm{topGen}\left({B}\right)↔{C}\subseteq \mathrm{topGen}\left({B}\right)\right)$
10 2 8 9 syl2an2 ${⊢}\left({B}\subseteq {C}\wedge {C}\subseteq \mathrm{topGen}\left({B}\right)\right)\to \left(\mathrm{topGen}\left({C}\right)\subseteq \mathrm{topGen}\left({B}\right)↔{C}\subseteq \mathrm{topGen}\left({B}\right)\right)$
11 6 10 mpbird ${⊢}\left({B}\subseteq {C}\wedge {C}\subseteq \mathrm{topGen}\left({B}\right)\right)\to \mathrm{topGen}\left({C}\right)\subseteq \mathrm{topGen}\left({B}\right)$
12 5 11 eqssd ${⊢}\left({B}\subseteq {C}\wedge {C}\subseteq \mathrm{topGen}\left({B}\right)\right)\to \mathrm{topGen}\left({B}\right)=\mathrm{topGen}\left({C}\right)$