Metamath Proof Explorer


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