Step |
Hyp |
Ref |
Expression |
1 |
|
cnextf.1 |
|- C = U. J |
2 |
|
cnextf.2 |
|- B = U. K |
3 |
|
cnextf.3 |
|- ( ph -> J e. Top ) |
4 |
|
cnextf.4 |
|- ( ph -> K e. Haus ) |
5 |
|
cnextf.5 |
|- ( ph -> F : A --> B ) |
6 |
|
cnextf.a |
|- ( ph -> A C_ C ) |
7 |
|
cnextf.6 |
|- ( ph -> ( ( cls ` J ) ` A ) = C ) |
8 |
|
cnextf.7 |
|- ( ( ph /\ x e. C ) -> ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) =/= (/) ) |
9 |
1 2
|
cnextfun |
|- ( ( ( J e. Top /\ K e. Haus ) /\ ( F : A --> B /\ A C_ C ) ) -> Fun ( ( J CnExt K ) ` F ) ) |
10 |
3 4 5 6 9
|
syl22anc |
|- ( ph -> Fun ( ( J CnExt K ) ` F ) ) |
11 |
|
dfdm3 |
|- dom ( ( J CnExt K ) ` F ) = { x | E. y <. x , y >. e. ( ( J CnExt K ) ` F ) } |
12 |
|
simpl |
|- ( ( ph /\ x e. C ) -> ph ) |
13 |
7
|
eleq2d |
|- ( ph -> ( x e. ( ( cls ` J ) ` A ) <-> x e. C ) ) |
14 |
13
|
biimpar |
|- ( ( ph /\ x e. C ) -> x e. ( ( cls ` J ) ` A ) ) |
15 |
|
n0 |
|- ( ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) =/= (/) <-> E. y y e. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) |
16 |
8 15
|
sylib |
|- ( ( ph /\ x e. C ) -> E. y y e. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) |
17 |
|
haustop |
|- ( K e. Haus -> K e. Top ) |
18 |
4 17
|
syl |
|- ( ph -> K e. Top ) |
19 |
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 ) ) ) |
20 |
3 18 5 6 19
|
syl22anc |
|- ( ph -> ( ( J CnExt K ) ` F ) = U_ x e. ( ( cls ` J ) ` A ) ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) ) |
21 |
20
|
eleq2d |
|- ( ph -> ( <. 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 ) ) ) ) |
22 |
|
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 ) ) ) |
23 |
21 22
|
bitrdi |
|- ( ph -> ( <. x , y >. e. ( ( J CnExt K ) ` F ) <-> ( x e. ( ( cls ` J ) ` A ) /\ y e. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) ) ) |
24 |
23
|
exbidv |
|- ( ph -> ( E. y <. x , y >. e. ( ( J CnExt K ) ` F ) <-> E. y ( x e. ( ( cls ` J ) ` A ) /\ y e. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) ) ) |
25 |
|
19.42v |
|- ( 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 ) ) ) |
26 |
24 25
|
bitrdi |
|- ( ph -> ( E. y <. x , y >. e. ( ( J CnExt K ) ` F ) <-> ( x e. ( ( cls ` J ) ` A ) /\ E. y y e. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) ) ) |
27 |
26
|
biimpar |
|- ( ( ph /\ ( x e. ( ( cls ` J ) ` A ) /\ E. y y e. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) ) -> E. y <. x , y >. e. ( ( J CnExt K ) ` F ) ) |
28 |
12 14 16 27
|
syl12anc |
|- ( ( ph /\ x e. C ) -> E. y <. x , y >. e. ( ( J CnExt K ) ` F ) ) |
29 |
26
|
simprbda |
|- ( ( ph /\ E. y <. x , y >. e. ( ( J CnExt K ) ` F ) ) -> x e. ( ( cls ` J ) ` A ) ) |
30 |
13
|
adantr |
|- ( ( ph /\ E. y <. x , y >. e. ( ( J CnExt K ) ` F ) ) -> ( x e. ( ( cls ` J ) ` A ) <-> x e. C ) ) |
31 |
29 30
|
mpbid |
|- ( ( ph /\ E. y <. x , y >. e. ( ( J CnExt K ) ` F ) ) -> x e. C ) |
32 |
28 31
|
impbida |
|- ( ph -> ( x e. C <-> E. y <. x , y >. e. ( ( J CnExt K ) ` F ) ) ) |
33 |
32
|
abbi2dv |
|- ( ph -> C = { x | E. y <. x , y >. e. ( ( J CnExt K ) ` F ) } ) |
34 |
11 33
|
eqtr4id |
|- ( ph -> dom ( ( J CnExt K ) ` F ) = C ) |
35 |
|
df-fn |
|- ( ( ( J CnExt K ) ` F ) Fn C <-> ( Fun ( ( J CnExt K ) ` F ) /\ dom ( ( J CnExt K ) ` F ) = C ) ) |
36 |
10 34 35
|
sylanbrc |
|- ( ph -> ( ( J CnExt K ) ` F ) Fn C ) |
37 |
20
|
rneqd |
|- ( ph -> ran ( ( J CnExt K ) ` F ) = ran U_ x e. ( ( cls ` J ) ` A ) ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) ) |
38 |
|
rniun |
|- ran U_ x e. ( ( cls ` J ) ` A ) ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) = U_ x e. ( ( cls ` J ) ` A ) ran ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) |
39 |
|
vex |
|- x e. _V |
40 |
39
|
snnz |
|- { x } =/= (/) |
41 |
|
rnxp |
|- ( { x } =/= (/) -> ran ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) = ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) |
42 |
40 41
|
ax-mp |
|- ran ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) = ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) |
43 |
13
|
biimpa |
|- ( ( ph /\ x e. ( ( cls ` J ) ` A ) ) -> x e. C ) |
44 |
2
|
toptopon |
|- ( K e. Top <-> K e. ( TopOn ` B ) ) |
45 |
18 44
|
sylib |
|- ( ph -> K e. ( TopOn ` B ) ) |
46 |
45
|
adantr |
|- ( ( ph /\ x e. C ) -> K e. ( TopOn ` B ) ) |
47 |
1
|
toptopon |
|- ( J e. Top <-> J e. ( TopOn ` C ) ) |
48 |
3 47
|
sylib |
|- ( ph -> J e. ( TopOn ` C ) ) |
49 |
48
|
adantr |
|- ( ( ph /\ x e. C ) -> J e. ( TopOn ` C ) ) |
50 |
6
|
adantr |
|- ( ( ph /\ x e. C ) -> A C_ C ) |
51 |
|
simpr |
|- ( ( ph /\ x e. C ) -> x e. C ) |
52 |
|
trnei |
|- ( ( J e. ( TopOn ` C ) /\ A C_ C /\ x e. C ) -> ( x e. ( ( cls ` J ) ` A ) <-> ( ( ( nei ` J ) ` { x } ) |`t A ) e. ( Fil ` A ) ) ) |
53 |
52
|
biimpa |
|- ( ( ( J e. ( TopOn ` C ) /\ A C_ C /\ x e. C ) /\ x e. ( ( cls ` J ) ` A ) ) -> ( ( ( nei ` J ) ` { x } ) |`t A ) e. ( Fil ` A ) ) |
54 |
49 50 51 14 53
|
syl31anc |
|- ( ( ph /\ x e. C ) -> ( ( ( nei ` J ) ` { x } ) |`t A ) e. ( Fil ` A ) ) |
55 |
5
|
adantr |
|- ( ( ph /\ x e. C ) -> F : A --> B ) |
56 |
|
flfelbas |
|- ( ( ( K e. ( TopOn ` B ) /\ ( ( ( nei ` J ) ` { x } ) |`t A ) e. ( Fil ` A ) /\ F : A --> B ) /\ y e. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) -> y e. B ) |
57 |
56
|
ex |
|- ( ( K e. ( TopOn ` B ) /\ ( ( ( nei ` J ) ` { x } ) |`t A ) e. ( Fil ` A ) /\ F : A --> B ) -> ( y e. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) -> y e. B ) ) |
58 |
57
|
ssrdv |
|- ( ( K e. ( TopOn ` B ) /\ ( ( ( nei ` J ) ` { x } ) |`t A ) e. ( Fil ` A ) /\ F : A --> B ) -> ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) C_ B ) |
59 |
46 54 55 58
|
syl3anc |
|- ( ( ph /\ x e. C ) -> ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) C_ B ) |
60 |
43 59
|
syldan |
|- ( ( ph /\ x e. ( ( cls ` J ) ` A ) ) -> ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) C_ B ) |
61 |
42 60
|
eqsstrid |
|- ( ( ph /\ x e. ( ( cls ` J ) ` A ) ) -> ran ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) C_ B ) |
62 |
61
|
ralrimiva |
|- ( ph -> A. x e. ( ( cls ` J ) ` A ) ran ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) C_ B ) |
63 |
|
iunss |
|- ( U_ x e. ( ( cls ` J ) ` A ) ran ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) C_ B <-> A. x e. ( ( cls ` J ) ` A ) ran ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) C_ B ) |
64 |
62 63
|
sylibr |
|- ( ph -> U_ x e. ( ( cls ` J ) ` A ) ran ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) C_ B ) |
65 |
38 64
|
eqsstrid |
|- ( ph -> ran U_ x e. ( ( cls ` J ) ` A ) ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) C_ B ) |
66 |
37 65
|
eqsstrd |
|- ( ph -> ran ( ( J CnExt K ) ` F ) C_ B ) |
67 |
|
df-f |
|- ( ( ( J CnExt K ) ` F ) : C --> B <-> ( ( ( J CnExt K ) ` F ) Fn C /\ ran ( ( J CnExt K ) ` F ) C_ B ) ) |
68 |
36 66 67
|
sylanbrc |
|- ( ph -> ( ( J CnExt K ) ` F ) : C --> B ) |