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