Metamath Proof Explorer

Theorem tgcl

Description: Show that a basis generates a topology. Remark in Munkres p. 79. (Contributed by NM, 17-Jul-2006)

Ref Expression
Assertion tgcl 
|- ( B e. TopBases -> ( topGen ` B ) e. Top )

Proof

Step Hyp Ref Expression
1 uniss 
 |-  ( u C_ ( topGen ` B ) -> U. u C_ U. ( topGen ` B ) )
2 1 adantl 
 |-  ( ( B e. TopBases /\ u C_ ( topGen ` B ) ) -> U. u C_ U. ( topGen ` B ) )
3 unitg 
 |-  ( B e. TopBases -> U. ( topGen ` B ) = U. B )
4 3 adantr 
 |-  ( ( B e. TopBases /\ u C_ ( topGen ` B ) ) -> U. ( topGen ` B ) = U. B )
5 2 4 sseqtrd 
 |-  ( ( B e. TopBases /\ u C_ ( topGen ` B ) ) -> U. u C_ U. B )
6 eluni2 
 |-  ( x e. U. u <-> E. t e. u x e. t )
7 ssel2 
 |-  ( ( u C_ ( topGen ` B ) /\ t e. u ) -> t e. ( topGen ` B ) )
8 eltg2b 
 |-  ( B e. TopBases -> ( t e. ( topGen ` B ) <-> A. x e. t E. y e. B ( x e. y /\ y C_ t ) ) )
9 rsp 
 |-  ( A. x e. t E. y e. B ( x e. y /\ y C_ t ) -> ( x e. t -> E. y e. B ( x e. y /\ y C_ t ) ) )
10 8 9 biimtrdi 
 |-  ( B e. TopBases -> ( t e. ( topGen ` B ) -> ( x e. t -> E. y e. B ( x e. y /\ y C_ t ) ) ) )
11 10 imp31 
 |-  ( ( ( B e. TopBases /\ t e. ( topGen ` B ) ) /\ x e. t ) -> E. y e. B ( x e. y /\ y C_ t ) )
12 11 an32s 
 |-  ( ( ( B e. TopBases /\ x e. t ) /\ t e. ( topGen ` B ) ) -> E. y e. B ( x e. y /\ y C_ t ) )
13 7 12 sylan2 
 |-  ( ( ( B e. TopBases /\ x e. t ) /\ ( u C_ ( topGen ` B ) /\ t e. u ) ) -> E. y e. B ( x e. y /\ y C_ t ) )
14 13 an42s 
 |-  ( ( ( B e. TopBases /\ u C_ ( topGen ` B ) ) /\ ( t e. u /\ x e. t ) ) -> E. y e. B ( x e. y /\ y C_ t ) )
15 elssuni 
 |-  ( t e. u -> t C_ U. u )
16 sstr2 
 |-  ( y C_ t -> ( t C_ U. u -> y C_ U. u ) )
17 15 16 syl5com 
 |-  ( t e. u -> ( y C_ t -> y C_ U. u ) )
18 17 anim2d 
 |-  ( t e. u -> ( ( x e. y /\ y C_ t ) -> ( x e. y /\ y C_ U. u ) ) )
19 18 reximdv 
 |-  ( t e. u -> ( E. y e. B ( x e. y /\ y C_ t ) -> E. y e. B ( x e. y /\ y C_ U. u ) ) )
20 19 ad2antrl 
 |-  ( ( ( B e. TopBases /\ u C_ ( topGen ` B ) ) /\ ( t e. u /\ x e. t ) ) -> ( E. y e. B ( x e. y /\ y C_ t ) -> E. y e. B ( x e. y /\ y C_ U. u ) ) )
21 14 20 mpd 
 |-  ( ( ( B e. TopBases /\ u C_ ( topGen ` B ) ) /\ ( t e. u /\ x e. t ) ) -> E. y e. B ( x e. y /\ y C_ U. u ) )
22 21 rexlimdvaa 
 |-  ( ( B e. TopBases /\ u C_ ( topGen ` B ) ) -> ( E. t e. u x e. t -> E. y e. B ( x e. y /\ y C_ U. u ) ) )
23 6 22 biimtrid 
 |-  ( ( B e. TopBases /\ u C_ ( topGen ` B ) ) -> ( x e. U. u -> E. y e. B ( x e. y /\ y C_ U. u ) ) )
24 23 ralrimiv 
 |-  ( ( B e. TopBases /\ u C_ ( topGen ` B ) ) -> A. x e. U. u E. y e. B ( x e. y /\ y C_ U. u ) )
25 5 24 jca 
 |-  ( ( B e. TopBases /\ u C_ ( topGen ` B ) ) -> ( U. u C_ U. B /\ A. x e. U. u E. y e. B ( x e. y /\ y C_ U. u ) ) )
26 25 ex 
 |-  ( B e. TopBases -> ( u C_ ( topGen ` B ) -> ( U. u C_ U. B /\ A. x e. U. u E. y e. B ( x e. y /\ y C_ U. u ) ) ) )
27 eltg2 
 |-  ( B e. TopBases -> ( U. u e. ( topGen ` B ) <-> ( U. u C_ U. B /\ A. x e. U. u E. y e. B ( x e. y /\ y C_ U. u ) ) ) )
28 26 27 sylibrd 
 |-  ( B e. TopBases -> ( u C_ ( topGen ` B ) -> U. u e. ( topGen ` B ) ) )
29 28 alrimiv 
 |-  ( B e. TopBases -> A. u ( u C_ ( topGen ` B ) -> U. u e. ( topGen ` B ) ) )
30 inss1 
 |-  ( u i^i v ) C_ u
31 tg1 
 |-  ( u e. ( topGen ` B ) -> u C_ U. B )
32 30 31 sstrid 
 |-  ( u e. ( topGen ` B ) -> ( u i^i v ) C_ U. B )
33 32 ad2antrl 
 |-  ( ( B e. TopBases /\ ( u e. ( topGen ` B ) /\ v e. ( topGen ` B ) ) ) -> ( u i^i v ) C_ U. B )
34 eltg2 
 |-  ( B e. TopBases -> ( u e. ( topGen ` B ) <-> ( u C_ U. B /\ A. x e. u E. z e. B ( x e. z /\ z C_ u ) ) ) )
35 34 simplbda 
 |-  ( ( B e. TopBases /\ u e. ( topGen ` B ) ) -> A. x e. u E. z e. B ( x e. z /\ z C_ u ) )
36 rsp 
 |-  ( A. x e. u E. z e. B ( x e. z /\ z C_ u ) -> ( x e. u -> E. z e. B ( x e. z /\ z C_ u ) ) )
37 35 36 syl 
 |-  ( ( B e. TopBases /\ u e. ( topGen ` B ) ) -> ( x e. u -> E. z e. B ( x e. z /\ z C_ u ) ) )
38 eltg2 
 |-  ( B e. TopBases -> ( v e. ( topGen ` B ) <-> ( v C_ U. B /\ A. x e. v E. w e. B ( x e. w /\ w C_ v ) ) ) )
39 38 simplbda 
 |-  ( ( B e. TopBases /\ v e. ( topGen ` B ) ) -> A. x e. v E. w e. B ( x e. w /\ w C_ v ) )
40 rsp 
 |-  ( A. x e. v E. w e. B ( x e. w /\ w C_ v ) -> ( x e. v -> E. w e. B ( x e. w /\ w C_ v ) ) )
41 39 40 syl 
 |-  ( ( B e. TopBases /\ v e. ( topGen ` B ) ) -> ( x e. v -> E. w e. B ( x e. w /\ w C_ v ) ) )
42 37 41 im2anan9 
 |-  ( ( ( B e. TopBases /\ u e. ( topGen ` B ) ) /\ ( B e. TopBases /\ v e. ( topGen ` B ) ) ) -> ( ( x e. u /\ x e. v ) -> ( E. z e. B ( x e. z /\ z C_ u ) /\ E. w e. B ( x e. w /\ w C_ v ) ) ) )
43 elin 
 |-  ( x e. ( u i^i v ) <-> ( x e. u /\ x e. v ) )
44 reeanv 
 |-  ( E. z e. B E. w e. B ( ( x e. z /\ z C_ u ) /\ ( x e. w /\ w C_ v ) ) <-> ( E. z e. B ( x e. z /\ z C_ u ) /\ E. w e. B ( x e. w /\ w C_ v ) ) )
45 42 43 44 3imtr4g 
 |-  ( ( ( B e. TopBases /\ u e. ( topGen ` B ) ) /\ ( B e. TopBases /\ v e. ( topGen ` B ) ) ) -> ( x e. ( u i^i v ) -> E. z e. B E. w e. B ( ( x e. z /\ z C_ u ) /\ ( x e. w /\ w C_ v ) ) ) )
46 45 anandis 
 |-  ( ( B e. TopBases /\ ( u e. ( topGen ` B ) /\ v e. ( topGen ` B ) ) ) -> ( x e. ( u i^i v ) -> E. z e. B E. w e. B ( ( x e. z /\ z C_ u ) /\ ( x e. w /\ w C_ v ) ) ) )
47 elin 
 |-  ( x e. ( z i^i w ) <-> ( x e. z /\ x e. w ) )
48 47 biimpri 
 |-  ( ( x e. z /\ x e. w ) -> x e. ( z i^i w ) )
49 ss2in 
 |-  ( ( z C_ u /\ w C_ v ) -> ( z i^i w ) C_ ( u i^i v ) )
50 48 49 anim12i 
 |-  ( ( ( x e. z /\ x e. w ) /\ ( z C_ u /\ w C_ v ) ) -> ( x e. ( z i^i w ) /\ ( z i^i w ) C_ ( u i^i v ) ) )
51 50 an4s 
 |-  ( ( ( x e. z /\ z C_ u ) /\ ( x e. w /\ w C_ v ) ) -> ( x e. ( z i^i w ) /\ ( z i^i w ) C_ ( u i^i v ) ) )
52 basis2 
 |-  ( ( ( B e. TopBases /\ z e. B ) /\ ( w e. B /\ x e. ( z i^i w ) ) ) -> E. t e. B ( x e. t /\ t C_ ( z i^i w ) ) )
53 52 adantllr 
 |-  ( ( ( ( B e. TopBases /\ x e. ( u i^i v ) ) /\ z e. B ) /\ ( w e. B /\ x e. ( z i^i w ) ) ) -> E. t e. B ( x e. t /\ t C_ ( z i^i w ) ) )
54 53 adantrrr 
 |-  ( ( ( ( B e. TopBases /\ x e. ( u i^i v ) ) /\ z e. B ) /\ ( w e. B /\ ( x e. ( z i^i w ) /\ ( z i^i w ) C_ ( u i^i v ) ) ) ) -> E. t e. B ( x e. t /\ t C_ ( z i^i w ) ) )
55 sstr2 
 |-  ( t C_ ( z i^i w ) -> ( ( z i^i w ) C_ ( u i^i v ) -> t C_ ( u i^i v ) ) )
56 55 com12 
 |-  ( ( z i^i w ) C_ ( u i^i v ) -> ( t C_ ( z i^i w ) -> t C_ ( u i^i v ) ) )
57 56 anim2d 
 |-  ( ( z i^i w ) C_ ( u i^i v ) -> ( ( x e. t /\ t C_ ( z i^i w ) ) -> ( x e. t /\ t C_ ( u i^i v ) ) ) )
58 57 reximdv 
 |-  ( ( z i^i w ) C_ ( u i^i v ) -> ( E. t e. B ( x e. t /\ t C_ ( z i^i w ) ) -> E. t e. B ( x e. t /\ t C_ ( u i^i v ) ) ) )
59 58 adantl 
 |-  ( ( x e. ( z i^i w ) /\ ( z i^i w ) C_ ( u i^i v ) ) -> ( E. t e. B ( x e. t /\ t C_ ( z i^i w ) ) -> E. t e. B ( x e. t /\ t C_ ( u i^i v ) ) ) )
60 59 ad2antll 
 |-  ( ( ( ( B e. TopBases /\ x e. ( u i^i v ) ) /\ z e. B ) /\ ( w e. B /\ ( x e. ( z i^i w ) /\ ( z i^i w ) C_ ( u i^i v ) ) ) ) -> ( E. t e. B ( x e. t /\ t C_ ( z i^i w ) ) -> E. t e. B ( x e. t /\ t C_ ( u i^i v ) ) ) )
61 54 60 mpd 
 |-  ( ( ( ( B e. TopBases /\ x e. ( u i^i v ) ) /\ z e. B ) /\ ( w e. B /\ ( x e. ( z i^i w ) /\ ( z i^i w ) C_ ( u i^i v ) ) ) ) -> E. t e. B ( x e. t /\ t C_ ( u i^i v ) ) )
62 51 61 sylanr2 
 |-  ( ( ( ( B e. TopBases /\ x e. ( u i^i v ) ) /\ z e. B ) /\ ( w e. B /\ ( ( x e. z /\ z C_ u ) /\ ( x e. w /\ w C_ v ) ) ) ) -> E. t e. B ( x e. t /\ t C_ ( u i^i v ) ) )
63 62 rexlimdvaa 
 |-  ( ( ( B e. TopBases /\ x e. ( u i^i v ) ) /\ z e. B ) -> ( E. w e. B ( ( x e. z /\ z C_ u ) /\ ( x e. w /\ w C_ v ) ) -> E. t e. B ( x e. t /\ t C_ ( u i^i v ) ) ) )
64 63 rexlimdva 
 |-  ( ( B e. TopBases /\ x e. ( u i^i v ) ) -> ( E. z e. B E. w e. B ( ( x e. z /\ z C_ u ) /\ ( x e. w /\ w C_ v ) ) -> E. t e. B ( x e. t /\ t C_ ( u i^i v ) ) ) )
65 64 ex 
 |-  ( B e. TopBases -> ( x e. ( u i^i v ) -> ( E. z e. B E. w e. B ( ( x e. z /\ z C_ u ) /\ ( x e. w /\ w C_ v ) ) -> E. t e. B ( x e. t /\ t C_ ( u i^i v ) ) ) ) )
66 65 a2d 
 |-  ( B e. TopBases -> ( ( x e. ( u i^i v ) -> E. z e. B E. w e. B ( ( x e. z /\ z C_ u ) /\ ( x e. w /\ w C_ v ) ) ) -> ( x e. ( u i^i v ) -> E. t e. B ( x e. t /\ t C_ ( u i^i v ) ) ) ) )
67 66 imp 
 |-  ( ( B e. TopBases /\ ( x e. ( u i^i v ) -> E. z e. B E. w e. B ( ( x e. z /\ z C_ u ) /\ ( x e. w /\ w C_ v ) ) ) ) -> ( x e. ( u i^i v ) -> E. t e. B ( x e. t /\ t C_ ( u i^i v ) ) ) )
68 46 67 syldan 
 |-  ( ( B e. TopBases /\ ( u e. ( topGen ` B ) /\ v e. ( topGen ` B ) ) ) -> ( x e. ( u i^i v ) -> E. t e. B ( x e. t /\ t C_ ( u i^i v ) ) ) )
69 68 ralrimiv 
 |-  ( ( B e. TopBases /\ ( u e. ( topGen ` B ) /\ v e. ( topGen ` B ) ) ) -> A. x e. ( u i^i v ) E. t e. B ( x e. t /\ t C_ ( u i^i v ) ) )
70 33 69 jca 
 |-  ( ( B e. TopBases /\ ( u e. ( topGen ` B ) /\ v e. ( topGen ` B ) ) ) -> ( ( u i^i v ) C_ U. B /\ A. x e. ( u i^i v ) E. t e. B ( x e. t /\ t C_ ( u i^i v ) ) ) )
71 70 ex 
 |-  ( B e. TopBases -> ( ( u e. ( topGen ` B ) /\ v e. ( topGen ` B ) ) -> ( ( u i^i v ) C_ U. B /\ A. x e. ( u i^i v ) E. t e. B ( x e. t /\ t C_ ( u i^i v ) ) ) ) )
72 eltg2 
 |-  ( B e. TopBases -> ( ( u i^i v ) e. ( topGen ` B ) <-> ( ( u i^i v ) C_ U. B /\ A. x e. ( u i^i v ) E. t e. B ( x e. t /\ t C_ ( u i^i v ) ) ) ) )
73 71 72 sylibrd 
 |-  ( B e. TopBases -> ( ( u e. ( topGen ` B ) /\ v e. ( topGen ` B ) ) -> ( u i^i v ) e. ( topGen ` B ) ) )
74 73 ralrimivv 
 |-  ( B e. TopBases -> A. u e. ( topGen ` B ) A. v e. ( topGen ` B ) ( u i^i v ) e. ( topGen ` B ) )
75 fvex 
 |-  ( topGen ` B ) e. _V
76 istopg 
 |-  ( ( topGen ` B ) e. _V -> ( ( topGen ` B ) e. Top <-> ( A. u ( u C_ ( topGen ` B ) -> U. u e. ( topGen ` B ) ) /\ A. u e. ( topGen ` B ) A. v e. ( topGen ` B ) ( u i^i v ) e. ( topGen ` B ) ) ) )
77 75 76 ax-mp 
 |-  ( ( topGen ` B ) e. Top <-> ( A. u ( u C_ ( topGen ` B ) -> U. u e. ( topGen ` B ) ) /\ A. u e. ( topGen ` B ) A. v e. ( topGen ` B ) ( u i^i v ) e. ( topGen ` B ) ) )
78 29 74 77 sylanbrc 
 |-  ( B e. TopBases -> ( topGen ` B ) e. Top )