Step |
Hyp |
Ref |
Expression |
1 |
|
tgcn.1 |
|- ( ph -> J e. ( TopOn ` X ) ) |
2 |
|
tgcn.3 |
|- ( ph -> K = ( topGen ` B ) ) |
3 |
|
tgcn.4 |
|- ( ph -> K e. ( TopOn ` Y ) ) |
4 |
|
tgcnp.5 |
|- ( ph -> P e. X ) |
5 |
|
iscnp |
|- ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ P e. X ) -> ( F e. ( ( J CnP K ) ` P ) <-> ( F : X --> Y /\ A. y e. K ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) ) ) ) |
6 |
1 3 4 5
|
syl3anc |
|- ( ph -> ( F e. ( ( J CnP K ) ` P ) <-> ( F : X --> Y /\ A. y e. K ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) ) ) ) |
7 |
|
topontop |
|- ( K e. ( TopOn ` Y ) -> K e. Top ) |
8 |
3 7
|
syl |
|- ( ph -> K e. Top ) |
9 |
2 8
|
eqeltrrd |
|- ( ph -> ( topGen ` B ) e. Top ) |
10 |
|
tgclb |
|- ( B e. TopBases <-> ( topGen ` B ) e. Top ) |
11 |
9 10
|
sylibr |
|- ( ph -> B e. TopBases ) |
12 |
|
bastg |
|- ( B e. TopBases -> B C_ ( topGen ` B ) ) |
13 |
11 12
|
syl |
|- ( ph -> B C_ ( topGen ` B ) ) |
14 |
13 2
|
sseqtrrd |
|- ( ph -> B C_ K ) |
15 |
|
ssralv |
|- ( B C_ K -> ( A. y e. K ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) -> A. y e. B ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) ) ) |
16 |
14 15
|
syl |
|- ( ph -> ( A. y e. K ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) -> A. y e. B ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) ) ) |
17 |
16
|
anim2d |
|- ( ph -> ( ( F : X --> Y /\ A. y e. K ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) ) -> ( F : X --> Y /\ A. y e. B ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) ) ) ) |
18 |
6 17
|
sylbid |
|- ( ph -> ( F e. ( ( J CnP K ) ` P ) -> ( F : X --> Y /\ A. y e. B ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) ) ) ) |
19 |
2
|
eleq2d |
|- ( ph -> ( z e. K <-> z e. ( topGen ` B ) ) ) |
20 |
19
|
biimpa |
|- ( ( ph /\ z e. K ) -> z e. ( topGen ` B ) ) |
21 |
|
tg2 |
|- ( ( z e. ( topGen ` B ) /\ ( F ` P ) e. z ) -> E. y e. B ( ( F ` P ) e. y /\ y C_ z ) ) |
22 |
|
r19.29 |
|- ( ( A. y e. B ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) /\ E. y e. B ( ( F ` P ) e. y /\ y C_ z ) ) -> E. y e. B ( ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) /\ ( ( F ` P ) e. y /\ y C_ z ) ) ) |
23 |
|
sstr |
|- ( ( ( F " x ) C_ y /\ y C_ z ) -> ( F " x ) C_ z ) |
24 |
23
|
expcom |
|- ( y C_ z -> ( ( F " x ) C_ y -> ( F " x ) C_ z ) ) |
25 |
24
|
anim2d |
|- ( y C_ z -> ( ( P e. x /\ ( F " x ) C_ y ) -> ( P e. x /\ ( F " x ) C_ z ) ) ) |
26 |
25
|
reximdv |
|- ( y C_ z -> ( E. x e. J ( P e. x /\ ( F " x ) C_ y ) -> E. x e. J ( P e. x /\ ( F " x ) C_ z ) ) ) |
27 |
26
|
com12 |
|- ( E. x e. J ( P e. x /\ ( F " x ) C_ y ) -> ( y C_ z -> E. x e. J ( P e. x /\ ( F " x ) C_ z ) ) ) |
28 |
27
|
imim2i |
|- ( ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) -> ( ( F ` P ) e. y -> ( y C_ z -> E. x e. J ( P e. x /\ ( F " x ) C_ z ) ) ) ) |
29 |
28
|
imp32 |
|- ( ( ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) /\ ( ( F ` P ) e. y /\ y C_ z ) ) -> E. x e. J ( P e. x /\ ( F " x ) C_ z ) ) |
30 |
29
|
rexlimivw |
|- ( E. y e. B ( ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) /\ ( ( F ` P ) e. y /\ y C_ z ) ) -> E. x e. J ( P e. x /\ ( F " x ) C_ z ) ) |
31 |
22 30
|
syl |
|- ( ( A. y e. B ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) /\ E. y e. B ( ( F ` P ) e. y /\ y C_ z ) ) -> E. x e. J ( P e. x /\ ( F " x ) C_ z ) ) |
32 |
31
|
expcom |
|- ( E. y e. B ( ( F ` P ) e. y /\ y C_ z ) -> ( A. y e. B ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) -> E. x e. J ( P e. x /\ ( F " x ) C_ z ) ) ) |
33 |
21 32
|
syl |
|- ( ( z e. ( topGen ` B ) /\ ( F ` P ) e. z ) -> ( A. y e. B ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) -> E. x e. J ( P e. x /\ ( F " x ) C_ z ) ) ) |
34 |
33
|
ex |
|- ( z e. ( topGen ` B ) -> ( ( F ` P ) e. z -> ( A. y e. B ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) -> E. x e. J ( P e. x /\ ( F " x ) C_ z ) ) ) ) |
35 |
34
|
com23 |
|- ( z e. ( topGen ` B ) -> ( A. y e. B ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) -> ( ( F ` P ) e. z -> E. x e. J ( P e. x /\ ( F " x ) C_ z ) ) ) ) |
36 |
20 35
|
syl |
|- ( ( ph /\ z e. K ) -> ( A. y e. B ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) -> ( ( F ` P ) e. z -> E. x e. J ( P e. x /\ ( F " x ) C_ z ) ) ) ) |
37 |
36
|
ralrimdva |
|- ( ph -> ( A. y e. B ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) -> A. z e. K ( ( F ` P ) e. z -> E. x e. J ( P e. x /\ ( F " x ) C_ z ) ) ) ) |
38 |
37
|
anim2d |
|- ( ph -> ( ( F : X --> Y /\ A. y e. B ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) ) -> ( F : X --> Y /\ A. z e. K ( ( F ` P ) e. z -> E. x e. J ( P e. x /\ ( F " x ) C_ z ) ) ) ) ) |
39 |
|
iscnp |
|- ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ P e. X ) -> ( F e. ( ( J CnP K ) ` P ) <-> ( F : X --> Y /\ A. z e. K ( ( F ` P ) e. z -> E. x e. J ( P e. x /\ ( F " x ) C_ z ) ) ) ) ) |
40 |
1 3 4 39
|
syl3anc |
|- ( ph -> ( F e. ( ( J CnP K ) ` P ) <-> ( F : X --> Y /\ A. z e. K ( ( F ` P ) e. z -> E. x e. J ( P e. x /\ ( F " x ) C_ z ) ) ) ) ) |
41 |
38 40
|
sylibrd |
|- ( ph -> ( ( F : X --> Y /\ A. y e. B ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) ) -> F e. ( ( J CnP K ) ` P ) ) ) |
42 |
18 41
|
impbid |
|- ( ph -> ( F e. ( ( J CnP K ) ` P ) <-> ( F : X --> Y /\ A. y e. B ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) ) ) ) |