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