Metamath Proof Explorer

Theorem tgclb

Description: The property tgcl can be reversed: if the topology generated by B is actually a topology, then B must be a topological basis. This yields an alternative definition of TopBases . (Contributed by Mario Carneiro, 2-Sep-2015)

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

Proof

Step Hyp Ref Expression
1 tgcl 
 |-  ( B e. TopBases -> ( topGen ` B ) e. Top )
2 0opn 
 |-  ( ( topGen ` B ) e. Top -> (/) e. ( topGen ` B ) )
3 2 elfvexd 
 |-  ( ( topGen ` B ) e. Top -> B e. _V )
4 bastg 
 |-  ( B e. _V -> B C_ ( topGen ` B ) )
5 3 4 syl 
 |-  ( ( topGen ` B ) e. Top -> B C_ ( topGen ` B ) )
6 5 sselda 
 |-  ( ( ( topGen ` B ) e. Top /\ x e. B ) -> x e. ( topGen ` B ) )
7 5 sselda 
 |-  ( ( ( topGen ` B ) e. Top /\ y e. B ) -> y e. ( topGen ` B ) )
8 6 7 anim12dan 
 |-  ( ( ( topGen ` B ) e. Top /\ ( x e. B /\ y e. B ) ) -> ( x e. ( topGen ` B ) /\ y e. ( topGen ` B ) ) )
9 inopn 
 |-  ( ( ( topGen ` B ) e. Top /\ x e. ( topGen ` B ) /\ y e. ( topGen ` B ) ) -> ( x i^i y ) e. ( topGen ` B ) )
10 9 3expb 
 |-  ( ( ( topGen ` B ) e. Top /\ ( x e. ( topGen ` B ) /\ y e. ( topGen ` B ) ) ) -> ( x i^i y ) e. ( topGen ` B ) )
11 8 10 syldan 
 |-  ( ( ( topGen ` B ) e. Top /\ ( x e. B /\ y e. B ) ) -> ( x i^i y ) e. ( topGen ` B ) )
12 tg2 
 |-  ( ( ( x i^i y ) e. ( topGen ` B ) /\ z e. ( x i^i y ) ) -> E. w e. B ( z e. w /\ w C_ ( x i^i y ) ) )
13 12 ralrimiva 
 |-  ( ( x i^i y ) e. ( topGen ` B ) -> A. z e. ( x i^i y ) E. w e. B ( z e. w /\ w C_ ( x i^i y ) ) )
14 11 13 syl 
 |-  ( ( ( topGen ` B ) e. Top /\ ( x e. B /\ y e. B ) ) -> A. z e. ( x i^i y ) E. w e. B ( z e. w /\ w C_ ( x i^i y ) ) )
15 14 ralrimivva 
 |-  ( ( topGen ` B ) e. Top -> A. x e. B A. y e. B A. z e. ( x i^i y ) E. w e. B ( z e. w /\ w C_ ( x i^i y ) ) )
16 isbasis2g 
 |-  ( B e. _V -> ( B e. TopBases <-> A. x e. B A. y e. B A. z e. ( x i^i y ) E. w e. B ( z e. w /\ w C_ ( x i^i y ) ) ) )
17 3 16 syl 
 |-  ( ( topGen ` B ) e. Top -> ( B e. TopBases <-> A. x e. B A. y e. B A. z e. ( x i^i y ) E. w e. B ( z e. w /\ w C_ ( x i^i y ) ) ) )
18 15 17 mpbird 
 |-  ( ( topGen ` B ) e. Top -> B e. TopBases )
19 1 18 impbii 
 |-  ( B e. TopBases <-> ( topGen ` B ) e. Top )