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 )