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

Metamath Proof Explorer

Theorem tgss2

Description: A criterion for determining whether one topology is finer than another, based on a comparison of their bases. Lemma 2.2 of Munkres p. 80. (Contributed by NM, 20-Jul-2006) (Proof shortened by Mario Carneiro, 2-Sep-2015)

Ref Expression
Assertion tgss2 
|- ( ( B e. V /\ U. B = U. C ) -> ( ( topGen ` B ) C_ ( topGen ` C ) <-> A. x e. U. B A. y e. B ( x e. y -> E. z e. C ( x e. z /\ z C_ y ) ) ) )

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( B e. V /\ U. B = U. C ) -> U. B = U. C )
2 uniexg 
 |-  ( B e. V -> U. B e. _V )
3 2 adantr 
 |-  ( ( B e. V /\ U. B = U. C ) -> U. B e. _V )
4 1 3 eqeltrrd 
 |-  ( ( B e. V /\ U. B = U. C ) -> U. C e. _V )
5 uniexb 
 |-  ( C e. _V <-> U. C e. _V )
6 4 5 sylibr 
 |-  ( ( B e. V /\ U. B = U. C ) -> C e. _V )
7 tgss3 
 |-  ( ( B e. V /\ C e. _V ) -> ( ( topGen ` B ) C_ ( topGen ` C ) <-> B C_ ( topGen ` C ) ) )
8 6 7 syldan 
 |-  ( ( B e. V /\ U. B = U. C ) -> ( ( topGen ` B ) C_ ( topGen ` C ) <-> B C_ ( topGen ` C ) ) )
9 eltg2b 
 |-  ( C e. _V -> ( y e. ( topGen ` C ) <-> A. x e. y E. z e. C ( x e. z /\ z C_ y ) ) )
10 6 9 syl 
 |-  ( ( B e. V /\ U. B = U. C ) -> ( y e. ( topGen ` C ) <-> A. x e. y E. z e. C ( x e. z /\ z C_ y ) ) )
11 elunii 
 |-  ( ( x e. y /\ y e. B ) -> x e. U. B )
12 11 ancoms 
 |-  ( ( y e. B /\ x e. y ) -> x e. U. B )
13 biimt 
 |-  ( x e. U. B -> ( E. z e. C ( x e. z /\ z C_ y ) <-> ( x e. U. B -> E. z e. C ( x e. z /\ z C_ y ) ) ) )
14 12 13 syl 
 |-  ( ( y e. B /\ x e. y ) -> ( E. z e. C ( x e. z /\ z C_ y ) <-> ( x e. U. B -> E. z e. C ( x e. z /\ z C_ y ) ) ) )
15 14 ralbidva 
 |-  ( y e. B -> ( A. x e. y E. z e. C ( x e. z /\ z C_ y ) <-> A. x e. y ( x e. U. B -> E. z e. C ( x e. z /\ z C_ y ) ) ) )
16 10 15 sylan9bb 
 |-  ( ( ( B e. V /\ U. B = U. C ) /\ y e. B ) -> ( y e. ( topGen ` C ) <-> A. x e. y ( x e. U. B -> E. z e. C ( x e. z /\ z C_ y ) ) ) )
17 ralcom3 
 |-  ( A. x e. y ( x e. U. B -> E. z e. C ( x e. z /\ z C_ y ) ) <-> A. x e. U. B ( x e. y -> E. z e. C ( x e. z /\ z C_ y ) ) )
18 16 17 bitrdi 
 |-  ( ( ( B e. V /\ U. B = U. C ) /\ y e. B ) -> ( y e. ( topGen ` C ) <-> A. x e. U. B ( x e. y -> E. z e. C ( x e. z /\ z C_ y ) ) ) )
19 18 ralbidva 
 |-  ( ( B e. V /\ U. B = U. C ) -> ( A. y e. B y e. ( topGen ` C ) <-> A. y e. B A. x e. U. B ( x e. y -> E. z e. C ( x e. z /\ z C_ y ) ) ) )
20 dfss3 
 |-  ( B C_ ( topGen ` C ) <-> A. y e. B y e. ( topGen ` C ) )
21 ralcom 
 |-  ( A. x e. U. B A. y e. B ( x e. y -> E. z e. C ( x e. z /\ z C_ y ) ) <-> A. y e. B A. x e. U. B ( x e. y -> E. z e. C ( x e. z /\ z C_ y ) ) )
22 19 20 21 3bitr4g 
 |-  ( ( B e. V /\ U. B = U. C ) -> ( B C_ ( topGen ` C ) <-> A. x e. U. B A. y e. B ( x e. y -> E. z e. C ( x e. z /\ z C_ y ) ) ) )
23 8 22 bitrd 
 |-  ( ( B e. V /\ U. B = U. C ) -> ( ( topGen ` B ) C_ ( topGen ` C ) <-> A. x e. U. B A. y e. B ( x e. y -> E. z e. C ( x e. z /\ z C_ y ) ) ) )