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
|
syl6bi |
|- ( 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
|
syl5bi |
|- ( ( 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 ) |