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 |
|
cnextcn.8 |
|- ( ph -> K e. Reg ) |
10 |
|
simpll |
|- ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ) -> ph ) |
11 |
|
simpll |
|- ( ( ( ph /\ x e. C ) /\ ( w e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) /\ d e. ( ( nei ` J ) ` { x } ) /\ ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) C_ w ) ) -> ph ) |
12 |
|
simpr3 |
|- ( ( ( ph /\ x e. C ) /\ ( w e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) /\ d e. ( ( nei ` J ) ` { x } ) /\ ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) C_ w ) ) -> ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) C_ w ) |
13 |
3
|
ad2antrr |
|- ( ( ( ph /\ x e. C ) /\ ( w e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) /\ d e. ( ( nei ` J ) ` { x } ) /\ ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) C_ w ) ) -> J e. Top ) |
14 |
|
simpr2 |
|- ( ( ( ph /\ x e. C ) /\ ( w e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) /\ d e. ( ( nei ` J ) ` { x } ) /\ ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) C_ w ) ) -> d e. ( ( nei ` J ) ` { x } ) ) |
15 |
|
neii2 |
|- ( ( J e. Top /\ d e. ( ( nei ` J ) ` { x } ) ) -> E. v e. J ( { x } C_ v /\ v C_ d ) ) |
16 |
13 14 15
|
syl2anc |
|- ( ( ( ph /\ x e. C ) /\ ( w e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) /\ d e. ( ( nei ` J ) ` { x } ) /\ ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) C_ w ) ) -> E. v e. J ( { x } C_ v /\ v C_ d ) ) |
17 |
|
vex |
|- x e. _V |
18 |
17
|
snss |
|- ( x e. v <-> { x } C_ v ) |
19 |
18
|
biimpri |
|- ( { x } C_ v -> x e. v ) |
20 |
19
|
anim1i |
|- ( ( { x } C_ v /\ v C_ d ) -> ( x e. v /\ v C_ d ) ) |
21 |
20
|
anim2i |
|- ( ( v e. J /\ ( { x } C_ v /\ v C_ d ) ) -> ( v e. J /\ ( x e. v /\ v C_ d ) ) ) |
22 |
21
|
anim2i |
|- ( ( ph /\ ( v e. J /\ ( { x } C_ v /\ v C_ d ) ) ) -> ( ph /\ ( v e. J /\ ( x e. v /\ v C_ d ) ) ) ) |
23 |
22
|
ex |
|- ( ph -> ( ( v e. J /\ ( { x } C_ v /\ v C_ d ) ) -> ( ph /\ ( v e. J /\ ( x e. v /\ v C_ d ) ) ) ) ) |
24 |
|
3anass |
|- ( ( ph /\ v e. J /\ x e. v ) <-> ( ph /\ ( v e. J /\ x e. v ) ) ) |
25 |
24
|
anbi1i |
|- ( ( ( ph /\ v e. J /\ x e. v ) /\ v C_ d ) <-> ( ( ph /\ ( v e. J /\ x e. v ) ) /\ v C_ d ) ) |
26 |
|
anass |
|- ( ( ( ph /\ ( v e. J /\ x e. v ) ) /\ v C_ d ) <-> ( ph /\ ( ( v e. J /\ x e. v ) /\ v C_ d ) ) ) |
27 |
|
anass |
|- ( ( ( v e. J /\ x e. v ) /\ v C_ d ) <-> ( v e. J /\ ( x e. v /\ v C_ d ) ) ) |
28 |
27
|
anbi2i |
|- ( ( ph /\ ( ( v e. J /\ x e. v ) /\ v C_ d ) ) <-> ( ph /\ ( v e. J /\ ( x e. v /\ v C_ d ) ) ) ) |
29 |
25 26 28
|
3bitri |
|- ( ( ( ph /\ v e. J /\ x e. v ) /\ v C_ d ) <-> ( ph /\ ( v e. J /\ ( x e. v /\ v C_ d ) ) ) ) |
30 |
|
opnneip |
|- ( ( J e. Top /\ v e. J /\ x e. v ) -> v e. ( ( nei ` J ) ` { x } ) ) |
31 |
3 30
|
syl3an1 |
|- ( ( ph /\ v e. J /\ x e. v ) -> v e. ( ( nei ` J ) ` { x } ) ) |
32 |
31
|
adantr |
|- ( ( ( ph /\ v e. J /\ x e. v ) /\ v C_ d ) -> v e. ( ( nei ` J ) ` { x } ) ) |
33 |
|
simpr2 |
|- ( ( v C_ d /\ ( ph /\ v e. J /\ x e. v ) ) -> v e. J ) |
34 |
33
|
ex |
|- ( v C_ d -> ( ( ph /\ v e. J /\ x e. v ) -> v e. J ) ) |
35 |
34
|
imdistanri |
|- ( ( ( ph /\ v e. J /\ x e. v ) /\ v C_ d ) -> ( v e. J /\ v C_ d ) ) |
36 |
32 35
|
jca |
|- ( ( ( ph /\ v e. J /\ x e. v ) /\ v C_ d ) -> ( v e. ( ( nei ` J ) ` { x } ) /\ ( v e. J /\ v C_ d ) ) ) |
37 |
29 36
|
sylbir |
|- ( ( ph /\ ( v e. J /\ ( x e. v /\ v C_ d ) ) ) -> ( v e. ( ( nei ` J ) ` { x } ) /\ ( v e. J /\ v C_ d ) ) ) |
38 |
23 37
|
syl6 |
|- ( ph -> ( ( v e. J /\ ( { x } C_ v /\ v C_ d ) ) -> ( v e. ( ( nei ` J ) ` { x } ) /\ ( v e. J /\ v C_ d ) ) ) ) |
39 |
38
|
adantr |
|- ( ( ph /\ ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) C_ w ) -> ( ( v e. J /\ ( { x } C_ v /\ v C_ d ) ) -> ( v e. ( ( nei ` J ) ` { x } ) /\ ( v e. J /\ v C_ d ) ) ) ) |
40 |
|
haustop |
|- ( K e. Haus -> K e. Top ) |
41 |
4 40
|
syl |
|- ( ph -> K e. Top ) |
42 |
|
imassrn |
|- ( F " ( d i^i A ) ) C_ ran F |
43 |
5
|
frnd |
|- ( ph -> ran F C_ B ) |
44 |
42 43
|
sstrid |
|- ( ph -> ( F " ( d i^i A ) ) C_ B ) |
45 |
|
ssrin |
|- ( v C_ d -> ( v i^i A ) C_ ( d i^i A ) ) |
46 |
|
imass2 |
|- ( ( v i^i A ) C_ ( d i^i A ) -> ( F " ( v i^i A ) ) C_ ( F " ( d i^i A ) ) ) |
47 |
45 46
|
syl |
|- ( v C_ d -> ( F " ( v i^i A ) ) C_ ( F " ( d i^i A ) ) ) |
48 |
2
|
clsss |
|- ( ( K e. Top /\ ( F " ( d i^i A ) ) C_ B /\ ( F " ( v i^i A ) ) C_ ( F " ( d i^i A ) ) ) -> ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) C_ ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) ) |
49 |
41 44 47 48
|
syl2an3an |
|- ( ( ph /\ v C_ d ) -> ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) C_ ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) ) |
50 |
|
sstr |
|- ( ( ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) C_ ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) /\ ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) C_ w ) -> ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) C_ w ) |
51 |
49 50
|
sylan |
|- ( ( ( ph /\ v C_ d ) /\ ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) C_ w ) -> ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) C_ w ) |
52 |
51
|
an32s |
|- ( ( ( ph /\ ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) C_ w ) /\ v C_ d ) -> ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) C_ w ) |
53 |
52
|
ex |
|- ( ( ph /\ ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) C_ w ) -> ( v C_ d -> ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) C_ w ) ) |
54 |
53
|
anim2d |
|- ( ( ph /\ ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) C_ w ) -> ( ( v e. J /\ v C_ d ) -> ( v e. J /\ ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) C_ w ) ) ) |
55 |
54
|
anim2d |
|- ( ( ph /\ ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) C_ w ) -> ( ( v e. ( ( nei ` J ) ` { x } ) /\ ( v e. J /\ v C_ d ) ) -> ( v e. ( ( nei ` J ) ` { x } ) /\ ( v e. J /\ ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) C_ w ) ) ) ) |
56 |
39 55
|
syld |
|- ( ( ph /\ ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) C_ w ) -> ( ( v e. J /\ ( { x } C_ v /\ v C_ d ) ) -> ( v e. ( ( nei ` J ) ` { x } ) /\ ( v e. J /\ ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) C_ w ) ) ) ) |
57 |
56
|
reximdv2 |
|- ( ( ph /\ ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) C_ w ) -> ( E. v e. J ( { x } C_ v /\ v C_ d ) -> E. v e. ( ( nei ` J ) ` { x } ) ( v e. J /\ ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) C_ w ) ) ) |
58 |
57
|
imp |
|- ( ( ( ph /\ ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) C_ w ) /\ E. v e. J ( { x } C_ v /\ v C_ d ) ) -> E. v e. ( ( nei ` J ) ` { x } ) ( v e. J /\ ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) C_ w ) ) |
59 |
11 12 16 58
|
syl21anc |
|- ( ( ( ph /\ x e. C ) /\ ( w e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) /\ d e. ( ( nei ` J ) ` { x } ) /\ ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) C_ w ) ) -> E. v e. ( ( nei ` J ) ` { x } ) ( v e. J /\ ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) C_ w ) ) |
60 |
59
|
3anassrs |
|- ( ( ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ) /\ d e. ( ( nei ` J ) ` { x } ) ) /\ ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) C_ w ) -> E. v e. ( ( nei ` J ) ` { x } ) ( v e. J /\ ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) C_ w ) ) |
61 |
|
simpr |
|- ( ( ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ) /\ u e. ( ( ( nei ` J ) ` { x } ) |`t A ) ) /\ ( ( cls ` K ) ` ( F " u ) ) C_ w ) -> ( ( cls ` K ) ` ( F " u ) ) C_ w ) |
62 |
|
simp-4l |
|- ( ( ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ) /\ u e. ( ( ( nei ` J ) ` { x } ) |`t A ) ) /\ ( ( cls ` K ) ` ( F " u ) ) C_ w ) -> ph ) |
63 |
|
simplr |
|- ( ( ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ) /\ u e. ( ( ( nei ` J ) ` { x } ) |`t A ) ) /\ ( ( cls ` K ) ` ( F " u ) ) C_ w ) -> u e. ( ( ( nei ` J ) ` { x } ) |`t A ) ) |
64 |
|
imaeq2 |
|- ( u = ( d i^i A ) -> ( F " u ) = ( F " ( d i^i A ) ) ) |
65 |
64
|
fveq2d |
|- ( u = ( d i^i A ) -> ( ( cls ` K ) ` ( F " u ) ) = ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) ) |
66 |
65
|
sseq1d |
|- ( u = ( d i^i A ) -> ( ( ( cls ` K ) ` ( F " u ) ) C_ w <-> ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) C_ w ) ) |
67 |
66
|
biimpcd |
|- ( ( ( cls ` K ) ` ( F " u ) ) C_ w -> ( u = ( d i^i A ) -> ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) C_ w ) ) |
68 |
67
|
reximdv |
|- ( ( ( cls ` K ) ` ( F " u ) ) C_ w -> ( E. d e. ( ( nei ` J ) ` { x } ) u = ( d i^i A ) -> E. d e. ( ( nei ` J ) ` { x } ) ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) C_ w ) ) |
69 |
|
fvexd |
|- ( ph -> ( ( nei ` J ) ` { x } ) e. _V ) |
70 |
1
|
toptopon |
|- ( J e. Top <-> J e. ( TopOn ` C ) ) |
71 |
3 70
|
sylib |
|- ( ph -> J e. ( TopOn ` C ) ) |
72 |
71
|
elfvexd |
|- ( ph -> C e. _V ) |
73 |
72 6
|
ssexd |
|- ( ph -> A e. _V ) |
74 |
|
elrest |
|- ( ( ( ( nei ` J ) ` { x } ) e. _V /\ A e. _V ) -> ( u e. ( ( ( nei ` J ) ` { x } ) |`t A ) <-> E. d e. ( ( nei ` J ) ` { x } ) u = ( d i^i A ) ) ) |
75 |
69 73 74
|
syl2anc |
|- ( ph -> ( u e. ( ( ( nei ` J ) ` { x } ) |`t A ) <-> E. d e. ( ( nei ` J ) ` { x } ) u = ( d i^i A ) ) ) |
76 |
75
|
biimpa |
|- ( ( ph /\ u e. ( ( ( nei ` J ) ` { x } ) |`t A ) ) -> E. d e. ( ( nei ` J ) ` { x } ) u = ( d i^i A ) ) |
77 |
68 76
|
impel |
|- ( ( ( ( cls ` K ) ` ( F " u ) ) C_ w /\ ( ph /\ u e. ( ( ( nei ` J ) ` { x } ) |`t A ) ) ) -> E. d e. ( ( nei ` J ) ` { x } ) ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) C_ w ) |
78 |
61 62 63 77
|
syl12anc |
|- ( ( ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ) /\ u e. ( ( ( nei ` J ) ` { x } ) |`t A ) ) /\ ( ( cls ` K ) ` ( F " u ) ) C_ w ) -> E. d e. ( ( nei ` J ) ` { x } ) ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) C_ w ) |
79 |
|
eleq1w |
|- ( x = y -> ( x e. C <-> y e. C ) ) |
80 |
79
|
anbi2d |
|- ( x = y -> ( ( ph /\ x e. C ) <-> ( ph /\ y e. C ) ) ) |
81 |
|
sneq |
|- ( x = y -> { x } = { y } ) |
82 |
81
|
fveq2d |
|- ( x = y -> ( ( nei ` J ) ` { x } ) = ( ( nei ` J ) ` { y } ) ) |
83 |
82
|
oveq1d |
|- ( x = y -> ( ( ( nei ` J ) ` { x } ) |`t A ) = ( ( ( nei ` J ) ` { y } ) |`t A ) ) |
84 |
83
|
oveq2d |
|- ( x = y -> ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) = ( K fLimf ( ( ( nei ` J ) ` { y } ) |`t A ) ) ) |
85 |
84
|
fveq1d |
|- ( x = y -> ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) = ( ( K fLimf ( ( ( nei ` J ) ` { y } ) |`t A ) ) ` F ) ) |
86 |
85
|
neeq1d |
|- ( x = y -> ( ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) =/= (/) <-> ( ( K fLimf ( ( ( nei ` J ) ` { y } ) |`t A ) ) ` F ) =/= (/) ) ) |
87 |
80 86
|
imbi12d |
|- ( x = y -> ( ( ( ph /\ x e. C ) -> ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) =/= (/) ) <-> ( ( ph /\ y e. C ) -> ( ( K fLimf ( ( ( nei ` J ) ` { y } ) |`t A ) ) ` F ) =/= (/) ) ) ) |
88 |
87 8
|
chvarvv |
|- ( ( ph /\ y e. C ) -> ( ( K fLimf ( ( ( nei ` J ) ` { y } ) |`t A ) ) ` F ) =/= (/) ) |
89 |
1 2 3 4 5 6 7 88
|
cnextfvval |
|- ( ( ph /\ x e. C ) -> ( ( ( J CnExt K ) ` F ) ` x ) = U. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) |
90 |
|
fvex |
|- ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) e. _V |
91 |
90
|
uniex |
|- U. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) e. _V |
92 |
91
|
snid |
|- U. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) e. { U. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) } |
93 |
4
|
adantr |
|- ( ( ph /\ x e. C ) -> K e. Haus ) |
94 |
7
|
eleq2d |
|- ( ph -> ( x e. ( ( cls ` J ) ` A ) <-> x e. C ) ) |
95 |
94
|
biimpar |
|- ( ( ph /\ x e. C ) -> x e. ( ( cls ` J ) ` A ) ) |
96 |
71
|
adantr |
|- ( ( ph /\ x e. C ) -> J e. ( TopOn ` C ) ) |
97 |
6
|
adantr |
|- ( ( ph /\ x e. C ) -> A C_ C ) |
98 |
|
simpr |
|- ( ( ph /\ x e. C ) -> x e. C ) |
99 |
|
trnei |
|- ( ( J e. ( TopOn ` C ) /\ A C_ C /\ x e. C ) -> ( x e. ( ( cls ` J ) ` A ) <-> ( ( ( nei ` J ) ` { x } ) |`t A ) e. ( Fil ` A ) ) ) |
100 |
96 97 98 99
|
syl3anc |
|- ( ( ph /\ x e. C ) -> ( x e. ( ( cls ` J ) ` A ) <-> ( ( ( nei ` J ) ` { x } ) |`t A ) e. ( Fil ` A ) ) ) |
101 |
95 100
|
mpbid |
|- ( ( ph /\ x e. C ) -> ( ( ( nei ` J ) ` { x } ) |`t A ) e. ( Fil ` A ) ) |
102 |
5
|
adantr |
|- ( ( ph /\ x e. C ) -> F : A --> B ) |
103 |
2
|
hausflf2 |
|- ( ( ( K e. Haus /\ ( ( ( nei ` J ) ` { x } ) |`t A ) e. ( Fil ` A ) /\ F : A --> B ) /\ ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) =/= (/) ) -> ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ~~ 1o ) |
104 |
93 101 102 8 103
|
syl31anc |
|- ( ( ph /\ x e. C ) -> ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ~~ 1o ) |
105 |
|
en1b |
|- ( ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ~~ 1o <-> ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) = { U. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) } ) |
106 |
104 105
|
sylib |
|- ( ( ph /\ x e. C ) -> ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) = { U. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) } ) |
107 |
92 106
|
eleqtrrid |
|- ( ( ph /\ x e. C ) -> U. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) e. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) |
108 |
89 107
|
eqeltrd |
|- ( ( ph /\ x e. C ) -> ( ( ( J CnExt K ) ` F ) ` x ) e. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) |
109 |
2
|
toptopon |
|- ( K e. Top <-> K e. ( TopOn ` B ) ) |
110 |
41 109
|
sylib |
|- ( ph -> K e. ( TopOn ` B ) ) |
111 |
110
|
adantr |
|- ( ( ph /\ x e. C ) -> K e. ( TopOn ` B ) ) |
112 |
|
flfnei |
|- ( ( K e. ( TopOn ` B ) /\ ( ( ( nei ` J ) ` { x } ) |`t A ) e. ( Fil ` A ) /\ F : A --> B ) -> ( ( ( ( J CnExt K ) ` F ) ` x ) e. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) <-> ( ( ( ( J CnExt K ) ` F ) ` x ) e. B /\ A. b e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) E. u e. ( ( ( nei ` J ) ` { x } ) |`t A ) ( F " u ) C_ b ) ) ) |
113 |
111 101 102 112
|
syl3anc |
|- ( ( ph /\ x e. C ) -> ( ( ( ( J CnExt K ) ` F ) ` x ) e. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) <-> ( ( ( ( J CnExt K ) ` F ) ` x ) e. B /\ A. b e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) E. u e. ( ( ( nei ` J ) ` { x } ) |`t A ) ( F " u ) C_ b ) ) ) |
114 |
108 113
|
mpbid |
|- ( ( ph /\ x e. C ) -> ( ( ( ( J CnExt K ) ` F ) ` x ) e. B /\ A. b e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) E. u e. ( ( ( nei ` J ) ` { x } ) |`t A ) ( F " u ) C_ b ) ) |
115 |
114
|
simprd |
|- ( ( ph /\ x e. C ) -> A. b e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) E. u e. ( ( ( nei ` J ) ` { x } ) |`t A ) ( F " u ) C_ b ) |
116 |
115
|
r19.21bi |
|- ( ( ( ph /\ x e. C ) /\ b e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ) -> E. u e. ( ( ( nei ` J ) ` { x } ) |`t A ) ( F " u ) C_ b ) |
117 |
116
|
ad4ant13 |
|- ( ( ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ) /\ b e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ) /\ ( ( cls ` K ) ` b ) C_ w ) -> E. u e. ( ( ( nei ` J ) ` { x } ) |`t A ) ( F " u ) C_ b ) |
118 |
41
|
ad3antrrr |
|- ( ( ( ( ph /\ x e. C ) /\ b e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ) /\ ( ( cls ` K ) ` b ) C_ w ) -> K e. Top ) |
119 |
|
simplr |
|- ( ( ( ( ph /\ x e. C ) /\ b e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ) /\ ( ( cls ` K ) ` b ) C_ w ) -> b e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ) |
120 |
2
|
neii1 |
|- ( ( K e. Top /\ b e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ) -> b C_ B ) |
121 |
118 119 120
|
syl2anc |
|- ( ( ( ( ph /\ x e. C ) /\ b e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ) /\ ( ( cls ` K ) ` b ) C_ w ) -> b C_ B ) |
122 |
|
simpr |
|- ( ( ( ( ph /\ x e. C ) /\ b e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ) /\ ( ( cls ` K ) ` b ) C_ w ) -> ( ( cls ` K ) ` b ) C_ w ) |
123 |
2
|
clsss |
|- ( ( K e. Top /\ b C_ B /\ ( F " u ) C_ b ) -> ( ( cls ` K ) ` ( F " u ) ) C_ ( ( cls ` K ) ` b ) ) |
124 |
|
sstr |
|- ( ( ( ( cls ` K ) ` ( F " u ) ) C_ ( ( cls ` K ) ` b ) /\ ( ( cls ` K ) ` b ) C_ w ) -> ( ( cls ` K ) ` ( F " u ) ) C_ w ) |
125 |
123 124
|
sylan |
|- ( ( ( K e. Top /\ b C_ B /\ ( F " u ) C_ b ) /\ ( ( cls ` K ) ` b ) C_ w ) -> ( ( cls ` K ) ` ( F " u ) ) C_ w ) |
126 |
125
|
3an1rs |
|- ( ( ( K e. Top /\ b C_ B /\ ( ( cls ` K ) ` b ) C_ w ) /\ ( F " u ) C_ b ) -> ( ( cls ` K ) ` ( F " u ) ) C_ w ) |
127 |
126
|
ex |
|- ( ( K e. Top /\ b C_ B /\ ( ( cls ` K ) ` b ) C_ w ) -> ( ( F " u ) C_ b -> ( ( cls ` K ) ` ( F " u ) ) C_ w ) ) |
128 |
127
|
reximdv |
|- ( ( K e. Top /\ b C_ B /\ ( ( cls ` K ) ` b ) C_ w ) -> ( E. u e. ( ( ( nei ` J ) ` { x } ) |`t A ) ( F " u ) C_ b -> E. u e. ( ( ( nei ` J ) ` { x } ) |`t A ) ( ( cls ` K ) ` ( F " u ) ) C_ w ) ) |
129 |
118 121 122 128
|
syl3anc |
|- ( ( ( ( ph /\ x e. C ) /\ b e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ) /\ ( ( cls ` K ) ` b ) C_ w ) -> ( E. u e. ( ( ( nei ` J ) ` { x } ) |`t A ) ( F " u ) C_ b -> E. u e. ( ( ( nei ` J ) ` { x } ) |`t A ) ( ( cls ` K ) ` ( F " u ) ) C_ w ) ) |
130 |
129
|
adantllr |
|- ( ( ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ) /\ b e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ) /\ ( ( cls ` K ) ` b ) C_ w ) -> ( E. u e. ( ( ( nei ` J ) ` { x } ) |`t A ) ( F " u ) C_ b -> E. u e. ( ( ( nei ` J ) ` { x } ) |`t A ) ( ( cls ` K ) ` ( F " u ) ) C_ w ) ) |
131 |
117 130
|
mpd |
|- ( ( ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ) /\ b e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ) /\ ( ( cls ` K ) ` b ) C_ w ) -> E. u e. ( ( ( nei ` J ) ` { x } ) |`t A ) ( ( cls ` K ) ` ( F " u ) ) C_ w ) |
132 |
41
|
ad2antrr |
|- ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ) -> K e. Top ) |
133 |
9
|
ad2antrr |
|- ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ) -> K e. Reg ) |
134 |
133
|
ad2antrr |
|- ( ( ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ) /\ c e. K ) /\ ( ( ( ( J CnExt K ) ` F ) ` x ) e. c /\ c C_ w ) ) -> K e. Reg ) |
135 |
|
simplr |
|- ( ( ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ) /\ c e. K ) /\ ( ( ( ( J CnExt K ) ` F ) ` x ) e. c /\ c C_ w ) ) -> c e. K ) |
136 |
|
simprl |
|- ( ( ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ) /\ c e. K ) /\ ( ( ( ( J CnExt K ) ` F ) ` x ) e. c /\ c C_ w ) ) -> ( ( ( J CnExt K ) ` F ) ` x ) e. c ) |
137 |
|
regsep |
|- ( ( K e. Reg /\ c e. K /\ ( ( ( J CnExt K ) ` F ) ` x ) e. c ) -> E. b e. K ( ( ( ( J CnExt K ) ` F ) ` x ) e. b /\ ( ( cls ` K ) ` b ) C_ c ) ) |
138 |
134 135 136 137
|
syl3anc |
|- ( ( ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ) /\ c e. K ) /\ ( ( ( ( J CnExt K ) ` F ) ` x ) e. c /\ c C_ w ) ) -> E. b e. K ( ( ( ( J CnExt K ) ` F ) ` x ) e. b /\ ( ( cls ` K ) ` b ) C_ c ) ) |
139 |
|
sstr |
|- ( ( ( ( cls ` K ) ` b ) C_ c /\ c C_ w ) -> ( ( cls ` K ) ` b ) C_ w ) |
140 |
139
|
expcom |
|- ( c C_ w -> ( ( ( cls ` K ) ` b ) C_ c -> ( ( cls ` K ) ` b ) C_ w ) ) |
141 |
140
|
anim2d |
|- ( c C_ w -> ( ( ( ( ( J CnExt K ) ` F ) ` x ) e. b /\ ( ( cls ` K ) ` b ) C_ c ) -> ( ( ( ( J CnExt K ) ` F ) ` x ) e. b /\ ( ( cls ` K ) ` b ) C_ w ) ) ) |
142 |
141
|
reximdv |
|- ( c C_ w -> ( E. b e. K ( ( ( ( J CnExt K ) ` F ) ` x ) e. b /\ ( ( cls ` K ) ` b ) C_ c ) -> E. b e. K ( ( ( ( J CnExt K ) ` F ) ` x ) e. b /\ ( ( cls ` K ) ` b ) C_ w ) ) ) |
143 |
142
|
ad2antll |
|- ( ( ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ) /\ c e. K ) /\ ( ( ( ( J CnExt K ) ` F ) ` x ) e. c /\ c C_ w ) ) -> ( E. b e. K ( ( ( ( J CnExt K ) ` F ) ` x ) e. b /\ ( ( cls ` K ) ` b ) C_ c ) -> E. b e. K ( ( ( ( J CnExt K ) ` F ) ` x ) e. b /\ ( ( cls ` K ) ` b ) C_ w ) ) ) |
144 |
138 143
|
mpd |
|- ( ( ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ) /\ c e. K ) /\ ( ( ( ( J CnExt K ) ` F ) ` x ) e. c /\ c C_ w ) ) -> E. b e. K ( ( ( ( J CnExt K ) ` F ) ` x ) e. b /\ ( ( cls ` K ) ` b ) C_ w ) ) |
145 |
|
simpr |
|- ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ) -> w e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ) |
146 |
|
neii2 |
|- ( ( K e. Top /\ w e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ) -> E. c e. K ( { ( ( ( J CnExt K ) ` F ) ` x ) } C_ c /\ c C_ w ) ) |
147 |
|
fvex |
|- ( ( ( J CnExt K ) ` F ) ` x ) e. _V |
148 |
147
|
snss |
|- ( ( ( ( J CnExt K ) ` F ) ` x ) e. c <-> { ( ( ( J CnExt K ) ` F ) ` x ) } C_ c ) |
149 |
148
|
anbi1i |
|- ( ( ( ( ( J CnExt K ) ` F ) ` x ) e. c /\ c C_ w ) <-> ( { ( ( ( J CnExt K ) ` F ) ` x ) } C_ c /\ c C_ w ) ) |
150 |
149
|
biimpri |
|- ( ( { ( ( ( J CnExt K ) ` F ) ` x ) } C_ c /\ c C_ w ) -> ( ( ( ( J CnExt K ) ` F ) ` x ) e. c /\ c C_ w ) ) |
151 |
150
|
reximi |
|- ( E. c e. K ( { ( ( ( J CnExt K ) ` F ) ` x ) } C_ c /\ c C_ w ) -> E. c e. K ( ( ( ( J CnExt K ) ` F ) ` x ) e. c /\ c C_ w ) ) |
152 |
146 151
|
syl |
|- ( ( K e. Top /\ w e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ) -> E. c e. K ( ( ( ( J CnExt K ) ` F ) ` x ) e. c /\ c C_ w ) ) |
153 |
132 145 152
|
syl2anc |
|- ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ) -> E. c e. K ( ( ( ( J CnExt K ) ` F ) ` x ) e. c /\ c C_ w ) ) |
154 |
144 153
|
r19.29a |
|- ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ) -> E. b e. K ( ( ( ( J CnExt K ) ` F ) ` x ) e. b /\ ( ( cls ` K ) ` b ) C_ w ) ) |
155 |
|
anass |
|- ( ( ( b e. K /\ ( ( ( J CnExt K ) ` F ) ` x ) e. b ) /\ ( ( cls ` K ) ` b ) C_ w ) <-> ( b e. K /\ ( ( ( ( J CnExt K ) ` F ) ` x ) e. b /\ ( ( cls ` K ) ` b ) C_ w ) ) ) |
156 |
|
opnneip |
|- ( ( K e. Top /\ b e. K /\ ( ( ( J CnExt K ) ` F ) ` x ) e. b ) -> b e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ) |
157 |
156
|
3expib |
|- ( K e. Top -> ( ( b e. K /\ ( ( ( J CnExt K ) ` F ) ` x ) e. b ) -> b e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ) ) |
158 |
157
|
anim1d |
|- ( K e. Top -> ( ( ( b e. K /\ ( ( ( J CnExt K ) ` F ) ` x ) e. b ) /\ ( ( cls ` K ) ` b ) C_ w ) -> ( b e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) /\ ( ( cls ` K ) ` b ) C_ w ) ) ) |
159 |
155 158
|
syl5bir |
|- ( K e. Top -> ( ( b e. K /\ ( ( ( ( J CnExt K ) ` F ) ` x ) e. b /\ ( ( cls ` K ) ` b ) C_ w ) ) -> ( b e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) /\ ( ( cls ` K ) ` b ) C_ w ) ) ) |
160 |
159
|
reximdv2 |
|- ( K e. Top -> ( E. b e. K ( ( ( ( J CnExt K ) ` F ) ` x ) e. b /\ ( ( cls ` K ) ` b ) C_ w ) -> E. b e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ( ( cls ` K ) ` b ) C_ w ) ) |
161 |
132 154 160
|
sylc |
|- ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ) -> E. b e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ( ( cls ` K ) ` b ) C_ w ) |
162 |
131 161
|
r19.29a |
|- ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ) -> E. u e. ( ( ( nei ` J ) ` { x } ) |`t A ) ( ( cls ` K ) ` ( F " u ) ) C_ w ) |
163 |
78 162
|
r19.29a |
|- ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ) -> E. d e. ( ( nei ` J ) ` { x } ) ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) C_ w ) |
164 |
60 163
|
r19.29a |
|- ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ) -> E. v e. ( ( nei ` J ) ` { x } ) ( v e. J /\ ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) C_ w ) ) |
165 |
|
simplr |
|- ( ( ( ( ph /\ v e. J ) /\ ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) C_ w ) /\ z e. v ) -> ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) C_ w ) |
166 |
|
simpll |
|- ( ( ( ph /\ v e. J ) /\ z e. v ) -> ph ) |
167 |
3
|
ad2antrr |
|- ( ( ( ph /\ v e. J ) /\ z e. v ) -> J e. Top ) |
168 |
|
simplr |
|- ( ( ( ph /\ v e. J ) /\ z e. v ) -> v e. J ) |
169 |
1
|
eltopss |
|- ( ( J e. Top /\ v e. J ) -> v C_ C ) |
170 |
167 168 169
|
syl2anc |
|- ( ( ( ph /\ v e. J ) /\ z e. v ) -> v C_ C ) |
171 |
|
simpr |
|- ( ( ( ph /\ v e. J ) /\ z e. v ) -> z e. v ) |
172 |
170 171
|
sseldd |
|- ( ( ( ph /\ v e. J ) /\ z e. v ) -> z e. C ) |
173 |
|
fvexd |
|- ( ( ( ph /\ v e. J ) /\ z e. v ) -> ( ( nei ` J ) ` { z } ) e. _V ) |
174 |
73
|
ad2antrr |
|- ( ( ( ph /\ v e. J ) /\ z e. v ) -> A e. _V ) |
175 |
|
opnneip |
|- ( ( J e. Top /\ v e. J /\ z e. v ) -> v e. ( ( nei ` J ) ` { z } ) ) |
176 |
3 175
|
syl3an1 |
|- ( ( ph /\ v e. J /\ z e. v ) -> v e. ( ( nei ` J ) ` { z } ) ) |
177 |
176
|
3expa |
|- ( ( ( ph /\ v e. J ) /\ z e. v ) -> v e. ( ( nei ` J ) ` { z } ) ) |
178 |
|
elrestr |
|- ( ( ( ( nei ` J ) ` { z } ) e. _V /\ A e. _V /\ v e. ( ( nei ` J ) ` { z } ) ) -> ( v i^i A ) e. ( ( ( nei ` J ) ` { z } ) |`t A ) ) |
179 |
173 174 177 178
|
syl3anc |
|- ( ( ( ph /\ v e. J ) /\ z e. v ) -> ( v i^i A ) e. ( ( ( nei ` J ) ` { z } ) |`t A ) ) |
180 |
1 2 3 4 5 6 7 8
|
cnextfvval |
|- ( ( ph /\ z e. C ) -> ( ( ( J CnExt K ) ` F ) ` z ) = U. ( ( K fLimf ( ( ( nei ` J ) ` { z } ) |`t A ) ) ` F ) ) |
181 |
180
|
adantr |
|- ( ( ( ph /\ z e. C ) /\ ( v i^i A ) e. ( ( ( nei ` J ) ` { z } ) |`t A ) ) -> ( ( ( J CnExt K ) ` F ) ` z ) = U. ( ( K fLimf ( ( ( nei ` J ) ` { z } ) |`t A ) ) ` F ) ) |
182 |
4
|
adantr |
|- ( ( ph /\ z e. C ) -> K e. Haus ) |
183 |
7
|
eleq2d |
|- ( ph -> ( z e. ( ( cls ` J ) ` A ) <-> z e. C ) ) |
184 |
183
|
biimpar |
|- ( ( ph /\ z e. C ) -> z e. ( ( cls ` J ) ` A ) ) |
185 |
71
|
adantr |
|- ( ( ph /\ z e. C ) -> J e. ( TopOn ` C ) ) |
186 |
6
|
adantr |
|- ( ( ph /\ z e. C ) -> A C_ C ) |
187 |
|
simpr |
|- ( ( ph /\ z e. C ) -> z e. C ) |
188 |
|
trnei |
|- ( ( J e. ( TopOn ` C ) /\ A C_ C /\ z e. C ) -> ( z e. ( ( cls ` J ) ` A ) <-> ( ( ( nei ` J ) ` { z } ) |`t A ) e. ( Fil ` A ) ) ) |
189 |
185 186 187 188
|
syl3anc |
|- ( ( ph /\ z e. C ) -> ( z e. ( ( cls ` J ) ` A ) <-> ( ( ( nei ` J ) ` { z } ) |`t A ) e. ( Fil ` A ) ) ) |
190 |
184 189
|
mpbid |
|- ( ( ph /\ z e. C ) -> ( ( ( nei ` J ) ` { z } ) |`t A ) e. ( Fil ` A ) ) |
191 |
5
|
adantr |
|- ( ( ph /\ z e. C ) -> F : A --> B ) |
192 |
|
eleq1w |
|- ( x = z -> ( x e. C <-> z e. C ) ) |
193 |
192
|
anbi2d |
|- ( x = z -> ( ( ph /\ x e. C ) <-> ( ph /\ z e. C ) ) ) |
194 |
|
sneq |
|- ( x = z -> { x } = { z } ) |
195 |
194
|
fveq2d |
|- ( x = z -> ( ( nei ` J ) ` { x } ) = ( ( nei ` J ) ` { z } ) ) |
196 |
195
|
oveq1d |
|- ( x = z -> ( ( ( nei ` J ) ` { x } ) |`t A ) = ( ( ( nei ` J ) ` { z } ) |`t A ) ) |
197 |
196
|
oveq2d |
|- ( x = z -> ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) = ( K fLimf ( ( ( nei ` J ) ` { z } ) |`t A ) ) ) |
198 |
197
|
fveq1d |
|- ( x = z -> ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) = ( ( K fLimf ( ( ( nei ` J ) ` { z } ) |`t A ) ) ` F ) ) |
199 |
198
|
neeq1d |
|- ( x = z -> ( ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) =/= (/) <-> ( ( K fLimf ( ( ( nei ` J ) ` { z } ) |`t A ) ) ` F ) =/= (/) ) ) |
200 |
193 199
|
imbi12d |
|- ( x = z -> ( ( ( ph /\ x e. C ) -> ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) =/= (/) ) <-> ( ( ph /\ z e. C ) -> ( ( K fLimf ( ( ( nei ` J ) ` { z } ) |`t A ) ) ` F ) =/= (/) ) ) ) |
201 |
200 8
|
chvarvv |
|- ( ( ph /\ z e. C ) -> ( ( K fLimf ( ( ( nei ` J ) ` { z } ) |`t A ) ) ` F ) =/= (/) ) |
202 |
2
|
hausflf2 |
|- ( ( ( K e. Haus /\ ( ( ( nei ` J ) ` { z } ) |`t A ) e. ( Fil ` A ) /\ F : A --> B ) /\ ( ( K fLimf ( ( ( nei ` J ) ` { z } ) |`t A ) ) ` F ) =/= (/) ) -> ( ( K fLimf ( ( ( nei ` J ) ` { z } ) |`t A ) ) ` F ) ~~ 1o ) |
203 |
182 190 191 201 202
|
syl31anc |
|- ( ( ph /\ z e. C ) -> ( ( K fLimf ( ( ( nei ` J ) ` { z } ) |`t A ) ) ` F ) ~~ 1o ) |
204 |
|
en1b |
|- ( ( ( K fLimf ( ( ( nei ` J ) ` { z } ) |`t A ) ) ` F ) ~~ 1o <-> ( ( K fLimf ( ( ( nei ` J ) ` { z } ) |`t A ) ) ` F ) = { U. ( ( K fLimf ( ( ( nei ` J ) ` { z } ) |`t A ) ) ` F ) } ) |
205 |
203 204
|
sylib |
|- ( ( ph /\ z e. C ) -> ( ( K fLimf ( ( ( nei ` J ) ` { z } ) |`t A ) ) ` F ) = { U. ( ( K fLimf ( ( ( nei ` J ) ` { z } ) |`t A ) ) ` F ) } ) |
206 |
205
|
adantr |
|- ( ( ( ph /\ z e. C ) /\ ( v i^i A ) e. ( ( ( nei ` J ) ` { z } ) |`t A ) ) -> ( ( K fLimf ( ( ( nei ` J ) ` { z } ) |`t A ) ) ` F ) = { U. ( ( K fLimf ( ( ( nei ` J ) ` { z } ) |`t A ) ) ` F ) } ) |
207 |
110
|
adantr |
|- ( ( ph /\ z e. C ) -> K e. ( TopOn ` B ) ) |
208 |
|
flfval |
|- ( ( K e. ( TopOn ` B ) /\ ( ( ( nei ` J ) ` { z } ) |`t A ) e. ( Fil ` A ) /\ F : A --> B ) -> ( ( K fLimf ( ( ( nei ` J ) ` { z } ) |`t A ) ) ` F ) = ( K fLim ( ( B FilMap F ) ` ( ( ( nei ` J ) ` { z } ) |`t A ) ) ) ) |
209 |
207 190 191 208
|
syl3anc |
|- ( ( ph /\ z e. C ) -> ( ( K fLimf ( ( ( nei ` J ) ` { z } ) |`t A ) ) ` F ) = ( K fLim ( ( B FilMap F ) ` ( ( ( nei ` J ) ` { z } ) |`t A ) ) ) ) |
210 |
209
|
adantr |
|- ( ( ( ph /\ z e. C ) /\ ( v i^i A ) e. ( ( ( nei ` J ) ` { z } ) |`t A ) ) -> ( ( K fLimf ( ( ( nei ` J ) ` { z } ) |`t A ) ) ` F ) = ( K fLim ( ( B FilMap F ) ` ( ( ( nei ` J ) ` { z } ) |`t A ) ) ) ) |
211 |
4
|
uniexd |
|- ( ph -> U. K e. _V ) |
212 |
211
|
ad2antrr |
|- ( ( ( ph /\ z e. C ) /\ ( v i^i A ) e. ( ( ( nei ` J ) ` { z } ) |`t A ) ) -> U. K e. _V ) |
213 |
2 212
|
eqeltrid |
|- ( ( ( ph /\ z e. C ) /\ ( v i^i A ) e. ( ( ( nei ` J ) ` { z } ) |`t A ) ) -> B e. _V ) |
214 |
190
|
adantr |
|- ( ( ( ph /\ z e. C ) /\ ( v i^i A ) e. ( ( ( nei ` J ) ` { z } ) |`t A ) ) -> ( ( ( nei ` J ) ` { z } ) |`t A ) e. ( Fil ` A ) ) |
215 |
|
filfbas |
|- ( ( ( ( nei ` J ) ` { z } ) |`t A ) e. ( Fil ` A ) -> ( ( ( nei ` J ) ` { z } ) |`t A ) e. ( fBas ` A ) ) |
216 |
214 215
|
syl |
|- ( ( ( ph /\ z e. C ) /\ ( v i^i A ) e. ( ( ( nei ` J ) ` { z } ) |`t A ) ) -> ( ( ( nei ` J ) ` { z } ) |`t A ) e. ( fBas ` A ) ) |
217 |
5
|
ad2antrr |
|- ( ( ( ph /\ z e. C ) /\ ( v i^i A ) e. ( ( ( nei ` J ) ` { z } ) |`t A ) ) -> F : A --> B ) |
218 |
|
simpr |
|- ( ( ( ph /\ z e. C ) /\ ( v i^i A ) e. ( ( ( nei ` J ) ` { z } ) |`t A ) ) -> ( v i^i A ) e. ( ( ( nei ` J ) ` { z } ) |`t A ) ) |
219 |
|
fgfil |
|- ( ( ( ( nei ` J ) ` { z } ) |`t A ) e. ( Fil ` A ) -> ( A filGen ( ( ( nei ` J ) ` { z } ) |`t A ) ) = ( ( ( nei ` J ) ` { z } ) |`t A ) ) |
220 |
190 219
|
syl |
|- ( ( ph /\ z e. C ) -> ( A filGen ( ( ( nei ` J ) ` { z } ) |`t A ) ) = ( ( ( nei ` J ) ` { z } ) |`t A ) ) |
221 |
220
|
adantr |
|- ( ( ( ph /\ z e. C ) /\ ( v i^i A ) e. ( ( ( nei ` J ) ` { z } ) |`t A ) ) -> ( A filGen ( ( ( nei ` J ) ` { z } ) |`t A ) ) = ( ( ( nei ` J ) ` { z } ) |`t A ) ) |
222 |
218 221
|
eleqtrrd |
|- ( ( ( ph /\ z e. C ) /\ ( v i^i A ) e. ( ( ( nei ` J ) ` { z } ) |`t A ) ) -> ( v i^i A ) e. ( A filGen ( ( ( nei ` J ) ` { z } ) |`t A ) ) ) |
223 |
|
eqid |
|- ( A filGen ( ( ( nei ` J ) ` { z } ) |`t A ) ) = ( A filGen ( ( ( nei ` J ) ` { z } ) |`t A ) ) |
224 |
223
|
imaelfm |
|- ( ( ( B e. _V /\ ( ( ( nei ` J ) ` { z } ) |`t A ) e. ( fBas ` A ) /\ F : A --> B ) /\ ( v i^i A ) e. ( A filGen ( ( ( nei ` J ) ` { z } ) |`t A ) ) ) -> ( F " ( v i^i A ) ) e. ( ( B FilMap F ) ` ( ( ( nei ` J ) ` { z } ) |`t A ) ) ) |
225 |
213 216 217 222 224
|
syl31anc |
|- ( ( ( ph /\ z e. C ) /\ ( v i^i A ) e. ( ( ( nei ` J ) ` { z } ) |`t A ) ) -> ( F " ( v i^i A ) ) e. ( ( B FilMap F ) ` ( ( ( nei ` J ) ` { z } ) |`t A ) ) ) |
226 |
|
flimclsi |
|- ( ( F " ( v i^i A ) ) e. ( ( B FilMap F ) ` ( ( ( nei ` J ) ` { z } ) |`t A ) ) -> ( K fLim ( ( B FilMap F ) ` ( ( ( nei ` J ) ` { z } ) |`t A ) ) ) C_ ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) ) |
227 |
225 226
|
syl |
|- ( ( ( ph /\ z e. C ) /\ ( v i^i A ) e. ( ( ( nei ` J ) ` { z } ) |`t A ) ) -> ( K fLim ( ( B FilMap F ) ` ( ( ( nei ` J ) ` { z } ) |`t A ) ) ) C_ ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) ) |
228 |
210 227
|
eqsstrd |
|- ( ( ( ph /\ z e. C ) /\ ( v i^i A ) e. ( ( ( nei ` J ) ` { z } ) |`t A ) ) -> ( ( K fLimf ( ( ( nei ` J ) ` { z } ) |`t A ) ) ` F ) C_ ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) ) |
229 |
206 228
|
eqsstrrd |
|- ( ( ( ph /\ z e. C ) /\ ( v i^i A ) e. ( ( ( nei ` J ) ` { z } ) |`t A ) ) -> { U. ( ( K fLimf ( ( ( nei ` J ) ` { z } ) |`t A ) ) ` F ) } C_ ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) ) |
230 |
|
fvex |
|- ( ( K fLimf ( ( ( nei ` J ) ` { z } ) |`t A ) ) ` F ) e. _V |
231 |
230
|
uniex |
|- U. ( ( K fLimf ( ( ( nei ` J ) ` { z } ) |`t A ) ) ` F ) e. _V |
232 |
231
|
snss |
|- ( U. ( ( K fLimf ( ( ( nei ` J ) ` { z } ) |`t A ) ) ` F ) e. ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) <-> { U. ( ( K fLimf ( ( ( nei ` J ) ` { z } ) |`t A ) ) ` F ) } C_ ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) ) |
233 |
229 232
|
sylibr |
|- ( ( ( ph /\ z e. C ) /\ ( v i^i A ) e. ( ( ( nei ` J ) ` { z } ) |`t A ) ) -> U. ( ( K fLimf ( ( ( nei ` J ) ` { z } ) |`t A ) ) ` F ) e. ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) ) |
234 |
181 233
|
eqeltrd |
|- ( ( ( ph /\ z e. C ) /\ ( v i^i A ) e. ( ( ( nei ` J ) ` { z } ) |`t A ) ) -> ( ( ( J CnExt K ) ` F ) ` z ) e. ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) ) |
235 |
166 172 179 234
|
syl21anc |
|- ( ( ( ph /\ v e. J ) /\ z e. v ) -> ( ( ( J CnExt K ) ` F ) ` z ) e. ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) ) |
236 |
235
|
adantlr |
|- ( ( ( ( ph /\ v e. J ) /\ ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) C_ w ) /\ z e. v ) -> ( ( ( J CnExt K ) ` F ) ` z ) e. ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) ) |
237 |
165 236
|
sseldd |
|- ( ( ( ( ph /\ v e. J ) /\ ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) C_ w ) /\ z e. v ) -> ( ( ( J CnExt K ) ` F ) ` z ) e. w ) |
238 |
237
|
ralrimiva |
|- ( ( ( ph /\ v e. J ) /\ ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) C_ w ) -> A. z e. v ( ( ( J CnExt K ) ` F ) ` z ) e. w ) |
239 |
238
|
expl |
|- ( ph -> ( ( v e. J /\ ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) C_ w ) -> A. z e. v ( ( ( J CnExt K ) ` F ) ` z ) e. w ) ) |
240 |
239
|
reximdv |
|- ( ph -> ( E. v e. ( ( nei ` J ) ` { x } ) ( v e. J /\ ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) C_ w ) -> E. v e. ( ( nei ` J ) ` { x } ) A. z e. v ( ( ( J CnExt K ) ` F ) ` z ) e. w ) ) |
241 |
240
|
ad2antrr |
|- ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ) -> ( E. v e. ( ( nei ` J ) ` { x } ) ( v e. J /\ ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) C_ w ) -> E. v e. ( ( nei ` J ) ` { x } ) A. z e. v ( ( ( J CnExt K ) ` F ) ` z ) e. w ) ) |
242 |
164 241
|
mpd |
|- ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ) -> E. v e. ( ( nei ` J ) ` { x } ) A. z e. v ( ( ( J CnExt K ) ` F ) ` z ) e. w ) |
243 |
1 2 3 4 5 6 7 8
|
cnextf |
|- ( ph -> ( ( J CnExt K ) ` F ) : C --> B ) |
244 |
243
|
ffund |
|- ( ph -> Fun ( ( J CnExt K ) ` F ) ) |
245 |
244
|
adantr |
|- ( ( ph /\ v e. ( ( nei ` J ) ` { x } ) ) -> Fun ( ( J CnExt K ) ` F ) ) |
246 |
1
|
neii1 |
|- ( ( J e. Top /\ v e. ( ( nei ` J ) ` { x } ) ) -> v C_ C ) |
247 |
3 246
|
sylan |
|- ( ( ph /\ v e. ( ( nei ` J ) ` { x } ) ) -> v C_ C ) |
248 |
243
|
fdmd |
|- ( ph -> dom ( ( J CnExt K ) ` F ) = C ) |
249 |
248
|
adantr |
|- ( ( ph /\ v e. ( ( nei ` J ) ` { x } ) ) -> dom ( ( J CnExt K ) ` F ) = C ) |
250 |
247 249
|
sseqtrrd |
|- ( ( ph /\ v e. ( ( nei ` J ) ` { x } ) ) -> v C_ dom ( ( J CnExt K ) ` F ) ) |
251 |
|
funimass4 |
|- ( ( Fun ( ( J CnExt K ) ` F ) /\ v C_ dom ( ( J CnExt K ) ` F ) ) -> ( ( ( ( J CnExt K ) ` F ) " v ) C_ w <-> A. z e. v ( ( ( J CnExt K ) ` F ) ` z ) e. w ) ) |
252 |
245 250 251
|
syl2anc |
|- ( ( ph /\ v e. ( ( nei ` J ) ` { x } ) ) -> ( ( ( ( J CnExt K ) ` F ) " v ) C_ w <-> A. z e. v ( ( ( J CnExt K ) ` F ) ` z ) e. w ) ) |
253 |
252
|
biimprd |
|- ( ( ph /\ v e. ( ( nei ` J ) ` { x } ) ) -> ( A. z e. v ( ( ( J CnExt K ) ` F ) ` z ) e. w -> ( ( ( J CnExt K ) ` F ) " v ) C_ w ) ) |
254 |
253
|
reximdva |
|- ( ph -> ( E. v e. ( ( nei ` J ) ` { x } ) A. z e. v ( ( ( J CnExt K ) ` F ) ` z ) e. w -> E. v e. ( ( nei ` J ) ` { x } ) ( ( ( J CnExt K ) ` F ) " v ) C_ w ) ) |
255 |
10 242 254
|
sylc |
|- ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ) -> E. v e. ( ( nei ` J ) ` { x } ) ( ( ( J CnExt K ) ` F ) " v ) C_ w ) |
256 |
255
|
ralrimiva |
|- ( ( ph /\ x e. C ) -> A. w e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) E. v e. ( ( nei ` J ) ` { x } ) ( ( ( J CnExt K ) ` F ) " v ) C_ w ) |
257 |
256
|
ralrimiva |
|- ( ph -> A. x e. C A. w e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) E. v e. ( ( nei ` J ) ` { x } ) ( ( ( J CnExt K ) ` F ) " v ) C_ w ) |
258 |
1 2
|
cnnei |
|- ( ( J e. Top /\ K e. Top /\ ( ( J CnExt K ) ` F ) : C --> B ) -> ( ( ( J CnExt K ) ` F ) e. ( J Cn K ) <-> A. x e. C A. w e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) E. v e. ( ( nei ` J ) ` { x } ) ( ( ( J CnExt K ) ` F ) " v ) C_ w ) ) |
259 |
3 41 243 258
|
syl3anc |
|- ( ph -> ( ( ( J CnExt K ) ` F ) e. ( J Cn K ) <-> A. x e. C A. w e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) E. v e. ( ( nei ` J ) ` { x } ) ( ( ( J CnExt K ) ` F ) " v ) C_ w ) ) |
260 |
257 259
|
mpbird |
|- ( ph -> ( ( J CnExt K ) ` F ) e. ( J Cn K ) ) |