Step |
Hyp |
Ref |
Expression |
1 |
|
elcls3.1 |
|- ( ph -> J = ( topGen ` B ) ) |
2 |
|
elcls3.2 |
|- ( ph -> X = U. J ) |
3 |
|
elcls3.3 |
|- ( ph -> B e. TopBases ) |
4 |
|
elcls3.4 |
|- ( ph -> S C_ X ) |
5 |
|
elcls3.5 |
|- ( ph -> P e. X ) |
6 |
|
tgcl |
|- ( B e. TopBases -> ( topGen ` B ) e. Top ) |
7 |
3 6
|
syl |
|- ( ph -> ( topGen ` B ) e. Top ) |
8 |
1 7
|
eqeltrd |
|- ( ph -> J e. Top ) |
9 |
4 2
|
sseqtrd |
|- ( ph -> S C_ U. J ) |
10 |
5 2
|
eleqtrd |
|- ( ph -> P e. U. J ) |
11 |
|
eqid |
|- U. J = U. J |
12 |
11
|
elcls |
|- ( ( J e. Top /\ S C_ U. J /\ P e. U. J ) -> ( P e. ( ( cls ` J ) ` S ) <-> A. y e. J ( P e. y -> ( y i^i S ) =/= (/) ) ) ) |
13 |
8 9 10 12
|
syl3anc |
|- ( ph -> ( P e. ( ( cls ` J ) ` S ) <-> A. y e. J ( P e. y -> ( y i^i S ) =/= (/) ) ) ) |
14 |
|
bastg |
|- ( B e. TopBases -> B C_ ( topGen ` B ) ) |
15 |
3 14
|
syl |
|- ( ph -> B C_ ( topGen ` B ) ) |
16 |
15 1
|
sseqtrrd |
|- ( ph -> B C_ J ) |
17 |
16
|
sseld |
|- ( ph -> ( y e. B -> y e. J ) ) |
18 |
17
|
imim1d |
|- ( ph -> ( ( y e. J -> ( P e. y -> ( y i^i S ) =/= (/) ) ) -> ( y e. B -> ( P e. y -> ( y i^i S ) =/= (/) ) ) ) ) |
19 |
18
|
ralimdv2 |
|- ( ph -> ( A. y e. J ( P e. y -> ( y i^i S ) =/= (/) ) -> A. y e. B ( P e. y -> ( y i^i S ) =/= (/) ) ) ) |
20 |
|
eleq2w |
|- ( y = x -> ( P e. y <-> P e. x ) ) |
21 |
|
ineq1 |
|- ( y = x -> ( y i^i S ) = ( x i^i S ) ) |
22 |
21
|
neeq1d |
|- ( y = x -> ( ( y i^i S ) =/= (/) <-> ( x i^i S ) =/= (/) ) ) |
23 |
20 22
|
imbi12d |
|- ( y = x -> ( ( P e. y -> ( y i^i S ) =/= (/) ) <-> ( P e. x -> ( x i^i S ) =/= (/) ) ) ) |
24 |
23
|
cbvralvw |
|- ( A. y e. B ( P e. y -> ( y i^i S ) =/= (/) ) <-> A. x e. B ( P e. x -> ( x i^i S ) =/= (/) ) ) |
25 |
19 24
|
syl6ib |
|- ( ph -> ( A. y e. J ( P e. y -> ( y i^i S ) =/= (/) ) -> A. x e. B ( P e. x -> ( x i^i S ) =/= (/) ) ) ) |
26 |
|
simprl |
|- ( ( ( ph /\ A. x e. B ( P e. x -> ( x i^i S ) =/= (/) ) ) /\ ( y e. J /\ P e. y ) ) -> y e. J ) |
27 |
1
|
ad2antrr |
|- ( ( ( ph /\ A. x e. B ( P e. x -> ( x i^i S ) =/= (/) ) ) /\ ( y e. J /\ P e. y ) ) -> J = ( topGen ` B ) ) |
28 |
26 27
|
eleqtrd |
|- ( ( ( ph /\ A. x e. B ( P e. x -> ( x i^i S ) =/= (/) ) ) /\ ( y e. J /\ P e. y ) ) -> y e. ( topGen ` B ) ) |
29 |
|
simprr |
|- ( ( ( ph /\ A. x e. B ( P e. x -> ( x i^i S ) =/= (/) ) ) /\ ( y e. J /\ P e. y ) ) -> P e. y ) |
30 |
|
tg2 |
|- ( ( y e. ( topGen ` B ) /\ P e. y ) -> E. z e. B ( P e. z /\ z C_ y ) ) |
31 |
28 29 30
|
syl2anc |
|- ( ( ( ph /\ A. x e. B ( P e. x -> ( x i^i S ) =/= (/) ) ) /\ ( y e. J /\ P e. y ) ) -> E. z e. B ( P e. z /\ z C_ y ) ) |
32 |
|
eleq2w |
|- ( x = z -> ( P e. x <-> P e. z ) ) |
33 |
|
ineq1 |
|- ( x = z -> ( x i^i S ) = ( z i^i S ) ) |
34 |
33
|
neeq1d |
|- ( x = z -> ( ( x i^i S ) =/= (/) <-> ( z i^i S ) =/= (/) ) ) |
35 |
32 34
|
imbi12d |
|- ( x = z -> ( ( P e. x -> ( x i^i S ) =/= (/) ) <-> ( P e. z -> ( z i^i S ) =/= (/) ) ) ) |
36 |
35
|
rspccva |
|- ( ( A. x e. B ( P e. x -> ( x i^i S ) =/= (/) ) /\ z e. B ) -> ( P e. z -> ( z i^i S ) =/= (/) ) ) |
37 |
36
|
imp |
|- ( ( ( A. x e. B ( P e. x -> ( x i^i S ) =/= (/) ) /\ z e. B ) /\ P e. z ) -> ( z i^i S ) =/= (/) ) |
38 |
|
ssdisj |
|- ( ( z C_ y /\ ( y i^i S ) = (/) ) -> ( z i^i S ) = (/) ) |
39 |
38
|
ex |
|- ( z C_ y -> ( ( y i^i S ) = (/) -> ( z i^i S ) = (/) ) ) |
40 |
39
|
necon3d |
|- ( z C_ y -> ( ( z i^i S ) =/= (/) -> ( y i^i S ) =/= (/) ) ) |
41 |
37 40
|
syl5com |
|- ( ( ( A. x e. B ( P e. x -> ( x i^i S ) =/= (/) ) /\ z e. B ) /\ P e. z ) -> ( z C_ y -> ( y i^i S ) =/= (/) ) ) |
42 |
41
|
exp31 |
|- ( A. x e. B ( P e. x -> ( x i^i S ) =/= (/) ) -> ( z e. B -> ( P e. z -> ( z C_ y -> ( y i^i S ) =/= (/) ) ) ) ) |
43 |
42
|
imp4a |
|- ( A. x e. B ( P e. x -> ( x i^i S ) =/= (/) ) -> ( z e. B -> ( ( P e. z /\ z C_ y ) -> ( y i^i S ) =/= (/) ) ) ) |
44 |
43
|
rexlimdv |
|- ( A. x e. B ( P e. x -> ( x i^i S ) =/= (/) ) -> ( E. z e. B ( P e. z /\ z C_ y ) -> ( y i^i S ) =/= (/) ) ) |
45 |
44
|
ad2antlr |
|- ( ( ( ph /\ A. x e. B ( P e. x -> ( x i^i S ) =/= (/) ) ) /\ ( y e. J /\ P e. y ) ) -> ( E. z e. B ( P e. z /\ z C_ y ) -> ( y i^i S ) =/= (/) ) ) |
46 |
31 45
|
mpd |
|- ( ( ( ph /\ A. x e. B ( P e. x -> ( x i^i S ) =/= (/) ) ) /\ ( y e. J /\ P e. y ) ) -> ( y i^i S ) =/= (/) ) |
47 |
46
|
exp43 |
|- ( ph -> ( A. x e. B ( P e. x -> ( x i^i S ) =/= (/) ) -> ( y e. J -> ( P e. y -> ( y i^i S ) =/= (/) ) ) ) ) |
48 |
47
|
ralrimdv |
|- ( ph -> ( A. x e. B ( P e. x -> ( x i^i S ) =/= (/) ) -> A. y e. J ( P e. y -> ( y i^i S ) =/= (/) ) ) ) |
49 |
25 48
|
impbid |
|- ( ph -> ( A. y e. J ( P e. y -> ( y i^i S ) =/= (/) ) <-> A. x e. B ( P e. x -> ( x i^i S ) =/= (/) ) ) ) |
50 |
13 49
|
bitrd |
|- ( ph -> ( P e. ( ( cls ` J ) ` S ) <-> A. x e. B ( P e. x -> ( x i^i S ) =/= (/) ) ) ) |