Theorem tgval2

Description: Definition of a topology generated by a basis in Munkres p. 78. Later we show (in tgcl ) that ( topGenB ) is indeed a topology (on U. B , see unitg ). See also tgval and tgval3 . (Contributed by NM, 15-Jul-2006) (Revised by Mario Carneiro, 10-Jan-2015)

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

Proof

Step	Hyp	Ref	Expression
1		tgval	|- ( B e. V -> ( topGen ` B ) = { x | x C_ U. ( B i^i ~P x ) } )
2		inss1	|- ( B i^i ~P x ) C_ B
3	2	unissi	|- U. ( B i^i ~P x ) C_ U. B
4	3	sseli	|- ( y e. U. ( B i^i ~P x ) -> y e. U. B )
5	4	pm4.71ri	|- ( y e. U. ( B i^i ~P x ) <-> ( y e. U. B /\ y e. U. ( B i^i ~P x ) ) )
6	5	ralbii	|- ( A. y e. x y e. U. ( B i^i ~P x ) <-> A. y e. x ( y e. U. B /\ y e. U. ( B i^i ~P x ) ) )
7		r19.26	|- ( A. y e. x ( y e. U. B /\ y e. U. ( B i^i ~P x ) ) <-> ( A. y e. x y e. U. B /\ A. y e. x y e. U. ( B i^i ~P x ) ) )
8	6 7	bitri	|- ( A. y e. x y e. U. ( B i^i ~P x ) <-> ( A. y e. x y e. U. B /\ A. y e. x y e. U. ( B i^i ~P x ) ) )
9		dfss3	|- ( x C_ U. ( B i^i ~P x ) <-> A. y e. x y e. U. ( B i^i ~P x ) )
10		dfss3	|- ( x C_ U. B <-> A. y e. x y e. U. B )
11		elin	|- ( z e. ( B i^i ~P x ) <-> ( z e. B /\ z e. ~P x ) )
12	11	anbi2i	|- ( ( y e. z /\ z e. ( B i^i ~P x ) ) <-> ( y e. z /\ ( z e. B /\ z e. ~P x ) ) )
13		an12	|- ( ( y e. z /\ ( z e. B /\ z e. ~P x ) ) <-> ( z e. B /\ ( y e. z /\ z e. ~P x ) ) )
14	12 13	bitri	|- ( ( y e. z /\ z e. ( B i^i ~P x ) ) <-> ( z e. B /\ ( y e. z /\ z e. ~P x ) ) )
15	14	exbii	|- ( E. z ( y e. z /\ z e. ( B i^i ~P x ) ) <-> E. z ( z e. B /\ ( y e. z /\ z e. ~P x ) ) )
16		eluni	|- ( y e. U. ( B i^i ~P x ) <-> E. z ( y e. z /\ z e. ( B i^i ~P x ) ) )
17		df-rex	|- ( E. z e. B ( y e. z /\ z e. ~P x ) <-> E. z ( z e. B /\ ( y e. z /\ z e. ~P x ) ) )
18	15 16 17	3bitr4i	|- ( y e. U. ( B i^i ~P x ) <-> E. z e. B ( y e. z /\ z e. ~P x ) )
19		velpw	|- ( z e. ~P x <-> z C_ x )
20	19	anbi2i	|- ( ( y e. z /\ z e. ~P x ) <-> ( y e. z /\ z C_ x ) )
21	20	rexbii	|- ( E. z e. B ( y e. z /\ z e. ~P x ) <-> E. z e. B ( y e. z /\ z C_ x ) )
22	18 21	bitr2i	|- ( E. z e. B ( y e. z /\ z C_ x ) <-> y e. U. ( B i^i ~P x ) )
23	22	ralbii	|- ( A. y e. x E. z e. B ( y e. z /\ z C_ x ) <-> A. y e. x y e. U. ( B i^i ~P x ) )
24	10 23	anbi12i	|- ( ( x C_ U. B /\ A. y e. x E. z e. B ( y e. z /\ z C_ x ) ) <-> ( A. y e. x y e. U. B /\ A. y e. x y e. U. ( B i^i ~P x ) ) )
25	8 9 24	3bitr4i	|- ( x C_ U. ( B i^i ~P x ) <-> ( x C_ U. B /\ A. y e. x E. z e. B ( y e. z /\ z C_ x ) ) )
26	25	abbii	|- { x | x C_ U. ( B i^i ~P x ) } = { x | ( x C_ U. B /\ A. y e. x E. z e. B ( y e. z /\ z C_ x ) ) }
27	1 26	eqtrdi	|- ( B e. V -> ( topGen ` B ) = { x | ( x C_ U. B /\ A. y e. x E. z e. B ( y e. z /\ z C_ x ) ) } )