Step |
Hyp |
Ref |
Expression |
1 |
|
cnextfval.1 |
|- X = U. J |
2 |
|
cnextfval.2 |
|- B = U. K |
3 |
|
cnextval |
|- ( ( J e. Top /\ K e. Top ) -> ( J CnExt K ) = ( f e. ( U. K ^pm U. J ) |-> U_ x e. ( ( cls ` J ) ` dom f ) ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t dom f ) ) ` f ) ) ) ) |
4 |
3
|
adantr |
|- ( ( ( J e. Top /\ K e. Top ) /\ ( F : A --> B /\ A C_ X ) ) -> ( J CnExt K ) = ( f e. ( U. K ^pm U. J ) |-> U_ x e. ( ( cls ` J ) ` dom f ) ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t dom f ) ) ` f ) ) ) ) |
5 |
|
simpr |
|- ( ( ( ( J e. Top /\ K e. Top ) /\ ( F : A --> B /\ A C_ X ) ) /\ f = F ) -> f = F ) |
6 |
5
|
dmeqd |
|- ( ( ( ( J e. Top /\ K e. Top ) /\ ( F : A --> B /\ A C_ X ) ) /\ f = F ) -> dom f = dom F ) |
7 |
|
simplrl |
|- ( ( ( ( J e. Top /\ K e. Top ) /\ ( F : A --> B /\ A C_ X ) ) /\ f = F ) -> F : A --> B ) |
8 |
7
|
fdmd |
|- ( ( ( ( J e. Top /\ K e. Top ) /\ ( F : A --> B /\ A C_ X ) ) /\ f = F ) -> dom F = A ) |
9 |
6 8
|
eqtrd |
|- ( ( ( ( J e. Top /\ K e. Top ) /\ ( F : A --> B /\ A C_ X ) ) /\ f = F ) -> dom f = A ) |
10 |
9
|
fveq2d |
|- ( ( ( ( J e. Top /\ K e. Top ) /\ ( F : A --> B /\ A C_ X ) ) /\ f = F ) -> ( ( cls ` J ) ` dom f ) = ( ( cls ` J ) ` A ) ) |
11 |
9
|
oveq2d |
|- ( ( ( ( J e. Top /\ K e. Top ) /\ ( F : A --> B /\ A C_ X ) ) /\ f = F ) -> ( ( ( nei ` J ) ` { x } ) |`t dom f ) = ( ( ( nei ` J ) ` { x } ) |`t A ) ) |
12 |
11
|
oveq2d |
|- ( ( ( ( J e. Top /\ K e. Top ) /\ ( F : A --> B /\ A C_ X ) ) /\ f = F ) -> ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t dom f ) ) = ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ) |
13 |
12 5
|
fveq12d |
|- ( ( ( ( J e. Top /\ K e. Top ) /\ ( F : A --> B /\ A C_ X ) ) /\ f = F ) -> ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t dom f ) ) ` f ) = ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) |
14 |
13
|
xpeq2d |
|- ( ( ( ( J e. Top /\ K e. Top ) /\ ( F : A --> B /\ A C_ X ) ) /\ f = F ) -> ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t dom f ) ) ` f ) ) = ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) ) |
15 |
10 14
|
iuneq12d |
|- ( ( ( ( J e. Top /\ K e. Top ) /\ ( F : A --> B /\ A C_ X ) ) /\ f = F ) -> U_ x e. ( ( cls ` J ) ` dom f ) ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t dom f ) ) ` f ) ) = U_ x e. ( ( cls ` J ) ` A ) ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) ) |
16 |
|
uniexg |
|- ( K e. Top -> U. K e. _V ) |
17 |
16
|
ad2antlr |
|- ( ( ( J e. Top /\ K e. Top ) /\ ( F : A --> B /\ A C_ X ) ) -> U. K e. _V ) |
18 |
|
uniexg |
|- ( J e. Top -> U. J e. _V ) |
19 |
18
|
ad2antrr |
|- ( ( ( J e. Top /\ K e. Top ) /\ ( F : A --> B /\ A C_ X ) ) -> U. J e. _V ) |
20 |
|
eqid |
|- A = A |
21 |
20 2
|
feq23i |
|- ( F : A --> B <-> F : A --> U. K ) |
22 |
21
|
biimpi |
|- ( F : A --> B -> F : A --> U. K ) |
23 |
22
|
ad2antrl |
|- ( ( ( J e. Top /\ K e. Top ) /\ ( F : A --> B /\ A C_ X ) ) -> F : A --> U. K ) |
24 |
1
|
sseq2i |
|- ( A C_ X <-> A C_ U. J ) |
25 |
24
|
biimpi |
|- ( A C_ X -> A C_ U. J ) |
26 |
25
|
ad2antll |
|- ( ( ( J e. Top /\ K e. Top ) /\ ( F : A --> B /\ A C_ X ) ) -> A C_ U. J ) |
27 |
|
elpm2r |
|- ( ( ( U. K e. _V /\ U. J e. _V ) /\ ( F : A --> U. K /\ A C_ U. J ) ) -> F e. ( U. K ^pm U. J ) ) |
28 |
17 19 23 26 27
|
syl22anc |
|- ( ( ( J e. Top /\ K e. Top ) /\ ( F : A --> B /\ A C_ X ) ) -> F e. ( U. K ^pm U. J ) ) |
29 |
|
fvex |
|- ( ( cls ` J ) ` A ) e. _V |
30 |
|
snex |
|- { x } e. _V |
31 |
|
fvex |
|- ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) e. _V |
32 |
30 31
|
xpex |
|- ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) e. _V |
33 |
29 32
|
iunex |
|- U_ x e. ( ( cls ` J ) ` A ) ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) e. _V |
34 |
33
|
a1i |
|- ( ( ( J e. Top /\ K e. Top ) /\ ( F : A --> B /\ A C_ X ) ) -> U_ x e. ( ( cls ` J ) ` A ) ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) e. _V ) |
35 |
4 15 28 34
|
fvmptd |
|- ( ( ( J e. Top /\ K e. Top ) /\ ( F : A --> B /\ A C_ X ) ) -> ( ( J CnExt K ) ` F ) = U_ x e. ( ( cls ` J ) ` A ) ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) ) |