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

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