Step |
Hyp |
Ref |
Expression |
1 |
|
cnextfrel.1 |
|- C = U. J |
2 |
|
cnextfrel.2 |
|- B = U. K |
3 |
|
haustop |
|- ( K e. Haus -> K e. Top ) |
4 |
1 2
|
cnextrel |
|- ( ( ( J e. Top /\ K e. Top ) /\ ( F : A --> B /\ A C_ C ) ) -> Rel ( ( J CnExt K ) ` F ) ) |
5 |
3 4
|
sylanl2 |
|- ( ( ( J e. Top /\ K e. Haus ) /\ ( F : A --> B /\ A C_ C ) ) -> Rel ( ( J CnExt K ) ` F ) ) |
6 |
|
simpllr |
|- ( ( ( ( J e. Top /\ K e. Haus ) /\ ( F : A --> B /\ A C_ C ) ) /\ x e. ( ( cls ` J ) ` A ) ) -> K e. Haus ) |
7 |
1
|
toptopon |
|- ( J e. Top <-> J e. ( TopOn ` C ) ) |
8 |
7
|
biimpi |
|- ( J e. Top -> J e. ( TopOn ` C ) ) |
9 |
8
|
ad3antrrr |
|- ( ( ( ( J e. Top /\ K e. Haus ) /\ ( F : A --> B /\ A C_ C ) ) /\ x e. ( ( cls ` J ) ` A ) ) -> J e. ( TopOn ` C ) ) |
10 |
|
simplrr |
|- ( ( ( ( J e. Top /\ K e. Haus ) /\ ( F : A --> B /\ A C_ C ) ) /\ x e. ( ( cls ` J ) ` A ) ) -> A C_ C ) |
11 |
9 7
|
sylibr |
|- ( ( ( ( J e. Top /\ K e. Haus ) /\ ( F : A --> B /\ A C_ C ) ) /\ x e. ( ( cls ` J ) ` A ) ) -> J e. Top ) |
12 |
1
|
clsss3 |
|- ( ( J e. Top /\ A C_ C ) -> ( ( cls ` J ) ` A ) C_ C ) |
13 |
11 10 12
|
syl2anc |
|- ( ( ( ( J e. Top /\ K e. Haus ) /\ ( F : A --> B /\ A C_ C ) ) /\ x e. ( ( cls ` J ) ` A ) ) -> ( ( cls ` J ) ` A ) C_ C ) |
14 |
|
simpr |
|- ( ( ( ( J e. Top /\ K e. Haus ) /\ ( F : A --> B /\ A C_ C ) ) /\ x e. ( ( cls ` J ) ` A ) ) -> x e. ( ( cls ` J ) ` A ) ) |
15 |
13 14
|
sseldd |
|- ( ( ( ( J e. Top /\ K e. Haus ) /\ ( F : A --> B /\ A C_ C ) ) /\ x e. ( ( cls ` J ) ` A ) ) -> x e. C ) |
16 |
|
trnei |
|- ( ( J e. ( TopOn ` C ) /\ A C_ C /\ x e. C ) -> ( x e. ( ( cls ` J ) ` A ) <-> ( ( ( nei ` J ) ` { x } ) |`t A ) e. ( Fil ` A ) ) ) |
17 |
16
|
biimpa |
|- ( ( ( J e. ( TopOn ` C ) /\ A C_ C /\ x e. C ) /\ x e. ( ( cls ` J ) ` A ) ) -> ( ( ( nei ` J ) ` { x } ) |`t A ) e. ( Fil ` A ) ) |
18 |
9 10 15 14 17
|
syl31anc |
|- ( ( ( ( J e. Top /\ K e. Haus ) /\ ( F : A --> B /\ A C_ C ) ) /\ x e. ( ( cls ` J ) ` A ) ) -> ( ( ( nei ` J ) ` { x } ) |`t A ) e. ( Fil ` A ) ) |
19 |
|
simplrl |
|- ( ( ( ( J e. Top /\ K e. Haus ) /\ ( F : A --> B /\ A C_ C ) ) /\ x e. ( ( cls ` J ) ` A ) ) -> F : A --> B ) |
20 |
2
|
hausflf |
|- ( ( K e. Haus /\ ( ( ( nei ` J ) ` { x } ) |`t A ) e. ( Fil ` A ) /\ F : A --> B ) -> E* y y e. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) |
21 |
6 18 19 20
|
syl3anc |
|- ( ( ( ( J e. Top /\ K e. Haus ) /\ ( F : A --> B /\ A C_ C ) ) /\ x e. ( ( cls ` J ) ` A ) ) -> E* y y e. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) |
22 |
21
|
ex |
|- ( ( ( J e. Top /\ K e. Haus ) /\ ( F : A --> B /\ A C_ C ) ) -> ( x e. ( ( cls ` J ) ` A ) -> E* y y e. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) ) |
23 |
22
|
alrimiv |
|- ( ( ( J e. Top /\ K e. Haus ) /\ ( F : A --> B /\ A C_ C ) ) -> A. x ( x e. ( ( cls ` J ) ` A ) -> E* y y e. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) ) |
24 |
|
moanimv |
|- ( E* y ( x e. ( ( cls ` J ) ` A ) /\ y e. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) <-> ( x e. ( ( cls ` J ) ` A ) -> E* y y e. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) ) |
25 |
24
|
albii |
|- ( A. x E* y ( x e. ( ( cls ` J ) ` A ) /\ y e. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) <-> A. x ( x e. ( ( cls ` J ) ` A ) -> E* y y e. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) ) |
26 |
23 25
|
sylibr |
|- ( ( ( J e. Top /\ K e. Haus ) /\ ( F : A --> B /\ A C_ C ) ) -> A. x E* y ( x e. ( ( cls ` J ) ` A ) /\ y e. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) ) |
27 |
|
df-br |
|- ( x ( ( J CnExt K ) ` F ) y <-> <. x , y >. e. ( ( J CnExt K ) ` F ) ) |
28 |
27
|
a1i |
|- ( ( ( J e. Top /\ K e. Haus ) /\ ( F : A --> B /\ A C_ C ) ) -> ( x ( ( J CnExt K ) ` F ) y <-> <. x , y >. e. ( ( J CnExt K ) ` F ) ) ) |
29 |
1 2
|
cnextfval |
|- ( ( ( J e. Top /\ K e. Top ) /\ ( F : A --> B /\ A C_ C ) ) -> ( ( J CnExt K ) ` F ) = U_ x e. ( ( cls ` J ) ` A ) ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) ) |
30 |
3 29
|
sylanl2 |
|- ( ( ( J e. Top /\ K e. Haus ) /\ ( F : A --> B /\ A C_ C ) ) -> ( ( J CnExt K ) ` F ) = U_ x e. ( ( cls ` J ) ` A ) ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) ) |
31 |
30
|
eleq2d |
|- ( ( ( J e. Top /\ K e. Haus ) /\ ( F : A --> B /\ A C_ C ) ) -> ( <. x , y >. e. ( ( J CnExt K ) ` F ) <-> <. x , y >. e. U_ x e. ( ( cls ` J ) ` A ) ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) ) ) |
32 |
|
opeliunxp |
|- ( <. x , y >. e. U_ x e. ( ( cls ` J ) ` A ) ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) <-> ( x e. ( ( cls ` J ) ` A ) /\ y e. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) ) |
33 |
32
|
a1i |
|- ( ( ( J e. Top /\ K e. Haus ) /\ ( F : A --> B /\ A C_ C ) ) -> ( <. x , y >. e. U_ x e. ( ( cls ` J ) ` A ) ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) <-> ( x e. ( ( cls ` J ) ` A ) /\ y e. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) ) ) |
34 |
28 31 33
|
3bitrd |
|- ( ( ( J e. Top /\ K e. Haus ) /\ ( F : A --> B /\ A C_ C ) ) -> ( x ( ( J CnExt K ) ` F ) y <-> ( x e. ( ( cls ` J ) ` A ) /\ y e. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) ) ) |
35 |
34
|
mobidv |
|- ( ( ( J e. Top /\ K e. Haus ) /\ ( F : A --> B /\ A C_ C ) ) -> ( E* y x ( ( J CnExt K ) ` F ) y <-> E* y ( x e. ( ( cls ` J ) ` A ) /\ y e. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) ) ) |
36 |
35
|
albidv |
|- ( ( ( J e. Top /\ K e. Haus ) /\ ( F : A --> B /\ A C_ C ) ) -> ( A. x E* y x ( ( J CnExt K ) ` F ) y <-> A. x E* y ( x e. ( ( cls ` J ) ` A ) /\ y e. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) ) ) |
37 |
26 36
|
mpbird |
|- ( ( ( J e. Top /\ K e. Haus ) /\ ( F : A --> B /\ A C_ C ) ) -> A. x E* y x ( ( J CnExt K ) ` F ) y ) |
38 |
|
dffun6 |
|- ( Fun ( ( J CnExt K ) ` F ) <-> ( Rel ( ( J CnExt K ) ` F ) /\ A. x E* y x ( ( J CnExt K ) ` F ) y ) ) |
39 |
5 37 38
|
sylanbrc |
|- ( ( ( J e. Top /\ K e. Haus ) /\ ( F : A --> B /\ A C_ C ) ) -> Fun ( ( J CnExt K ) ` F ) ) |