Users' Mathboxes Mathbox for Frédéric Liné < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  islimrs4 Unicode version

Theorem islimrs4 25685
Description: The limits of  F at point  P relatively to  A is a limit of  F at point  P relatively to  B. (Contributed by FL, 13-Dec-2013.)
Hypotheses
Ref Expression
islimrs.1  |-  L  =  ( ( ( nei `  K ) `  { P } )t  A )
islimrs.2  |-  X  = 
U. J
islimrs.3  |-  Y  = 
U. K
Assertion
Ref Expression
islimrs4  |-  ( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K ) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K
) `  A )
)  /\  F  e.  ( X  ^m  A ) )  ->  ( (
( J  fLimfrs  K ) `
 A ) `  <. P ,  F >. )  =  ( ( ( J  fLimfrs  K ) `  ( A  i^i  N ) ) `  <. P , 
( F  |`  ( A  i^i  N ) )
>. ) )

Proof of Theorem islimrs4
Dummy variables  u  n  v  w  x are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simp11 985 . . 3  |-  ( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K ) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K
) `  A )
)  /\  F  e.  ( X  ^m  A ) )  ->  J  e.  Top )
2 simp12 986 . . 3  |-  ( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K ) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K
) `  A )
)  /\  F  e.  ( X  ^m  A ) )  ->  K  e.  Top )
3 inss1 3402 . . . 4  |-  ( A  i^i  N )  C_  A
43a1i 10 . . 3  |-  ( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K ) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K
) `  A )
)  /\  F  e.  ( X  ^m  A ) )  ->  ( A  i^i  N )  C_  A
)
5 simp2l 981 . . 3  |-  ( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K ) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K
) `  A )
)  /\  F  e.  ( X  ^m  A ) )  ->  A  C_  Y
)
6 incom 3374 . . . . . 6  |-  ( n  i^i  ( A  i^i  N ) )  =  ( ( A  i^i  N
)  i^i  n )
7 inass 3392 . . . . . 6  |-  ( ( A  i^i  N )  i^i  n )  =  ( A  i^i  ( N  i^i  n ) )
8 eqtr 2313 . . . . . . 7  |-  ( ( ( n  i^i  ( A  i^i  N ) )  =  ( ( A  i^i  N )  i^i  n )  /\  (
( A  i^i  N
)  i^i  n )  =  ( A  i^i  ( N  i^i  n
) ) )  -> 
( n  i^i  ( A  i^i  N ) )  =  ( A  i^i  ( N  i^i  n
) ) )
9 innei 16878 . . . . . . . . . . . . 13  |-  ( ( K  e.  Top  /\  N  e.  ( ( nei `  K ) `  { P } )  /\  n  e.  ( ( nei `  K ) `  { P } ) )  ->  ( N  i^i  n )  e.  ( ( nei `  K
) `  { P } ) )
1093expia 1153 . . . . . . . . . . . 12  |-  ( ( K  e.  Top  /\  N  e.  ( ( nei `  K ) `  { P } ) )  ->  ( n  e.  ( ( nei `  K
) `  { P } )  ->  ( N  i^i  n )  e.  ( ( nei `  K
) `  { P } ) ) )
11103adant1 973 . . . . . . . . . . 11  |-  ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K
) `  { P } ) )  -> 
( n  e.  ( ( nei `  K
) `  { P } )  ->  ( N  i^i  n )  e.  ( ( nei `  K
) `  { P } ) ) )
12113ad2ant1 976 . . . . . . . . . 10  |-  ( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K ) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K
) `  A )
)  /\  F  e.  ( X  ^m  A ) )  ->  ( n  e.  ( ( nei `  K
) `  { P } )  ->  ( N  i^i  n )  e.  ( ( nei `  K
) `  { P } ) ) )
1312imp 418 . . . . . . . . 9  |-  ( ( ( ( J  e. 
Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K
) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K ) `  A ) )  /\  F  e.  ( X  ^m  A ) )  /\  n  e.  ( ( nei `  K ) `  { P } ) )  ->  ( N  i^i  n )  e.  ( ( nei `  K
) `  { P } ) )
14 incom 3374 . . . . . . . . . 10  |-  ( A  i^i  ( N  i^i  n ) )  =  ( ( N  i^i  n )  i^i  A
)
152, 5jca 518 . . . . . . . . . . . . 13  |-  ( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K ) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K
) `  A )
)  /\  F  e.  ( X  ^m  A ) )  ->  ( K  e.  Top  /\  A  C_  Y ) )
1615ad2antrl 708 . . . . . . . . . . . 12  |-  ( ( ( N  i^i  n
)  e.  ( ( nei `  K ) `
 { P }
)  /\  ( (
( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K ) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K
) `  A )
)  /\  F  e.  ( X  ^m  A ) )  /\  n  e.  ( ( nei `  K
) `  { P } ) ) )  ->  ( K  e. 
Top  /\  A  C_  Y
) )
17 simpl2r 1009 . . . . . . . . . . . . 13  |-  ( ( ( ( J  e. 
Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K
) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K ) `  A ) )  /\  F  e.  ( X  ^m  A ) )  /\  n  e.  ( ( nei `  K ) `  { P } ) )  ->  P  e.  ( ( cls `  K
) `  A )
)
1817adantl 452 . . . . . . . . . . . 12  |-  ( ( ( N  i^i  n
)  e.  ( ( nei `  K ) `
 { P }
)  /\  ( (
( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K ) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K
) `  A )
)  /\  F  e.  ( X  ^m  A ) )  /\  n  e.  ( ( nei `  K
) `  { P } ) ) )  ->  P  e.  ( ( cls `  K
) `  A )
)
19 simpl 443 . . . . . . . . . . . 12  |-  ( ( ( N  i^i  n
)  e.  ( ( nei `  K ) `
 { P }
)  /\  ( (
( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K ) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K
) `  A )
)  /\  F  e.  ( X  ^m  A ) )  /\  n  e.  ( ( nei `  K
) `  { P } ) ) )  ->  ( N  i^i  n )  e.  ( ( nei `  K
) `  { P } ) )
20 islimrs.3 . . . . . . . . . . . . 13  |-  Y  = 
U. K
2120neindisj 16870 . . . . . . . . . . . 12  |-  ( ( ( K  e.  Top  /\  A  C_  Y )  /\  ( P  e.  ( ( cls `  K
) `  A )  /\  ( N  i^i  n
)  e.  ( ( nei `  K ) `
 { P }
) ) )  -> 
( ( N  i^i  n )  i^i  A
)  =/=  (/) )
2216, 18, 19, 21syl12anc 1180 . . . . . . . . . . 11  |-  ( ( ( N  i^i  n
)  e.  ( ( nei `  K ) `
 { P }
)  /\  ( (
( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K ) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K
) `  A )
)  /\  F  e.  ( X  ^m  A ) )  /\  n  e.  ( ( nei `  K
) `  { P } ) ) )  ->  ( ( N  i^i  n )  i^i 
A )  =/=  (/) )
23 neeq1 2467 . . . . . . . . . . 11  |-  ( ( A  i^i  ( N  i^i  n ) )  =  ( ( N  i^i  n )  i^i 
A )  ->  (
( A  i^i  ( N  i^i  n ) )  =/=  (/)  <->  ( ( N  i^i  n )  i^i 
A )  =/=  (/) ) )
2422, 23syl5ibr 212 . . . . . . . . . 10  |-  ( ( A  i^i  ( N  i^i  n ) )  =  ( ( N  i^i  n )  i^i 
A )  ->  (
( ( N  i^i  n )  e.  ( ( nei `  K
) `  { P } )  /\  (
( ( J  e. 
Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K
) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K ) `  A ) )  /\  F  e.  ( X  ^m  A ) )  /\  n  e.  ( ( nei `  K ) `  { P } ) ) )  ->  ( A  i^i  ( N  i^i  n
) )  =/=  (/) ) )
2514, 24ax-mp 8 . . . . . . . . 9  |-  ( ( ( N  i^i  n
)  e.  ( ( nei `  K ) `
 { P }
)  /\  ( (
( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K ) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K
) `  A )
)  /\  F  e.  ( X  ^m  A ) )  /\  n  e.  ( ( nei `  K
) `  { P } ) ) )  ->  ( A  i^i  ( N  i^i  n
) )  =/=  (/) )
2613, 25mpancom 650 . . . . . . . 8  |-  ( ( ( ( J  e. 
Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K
) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K ) `  A ) )  /\  F  e.  ( X  ^m  A ) )  /\  n  e.  ( ( nei `  K ) `  { P } ) )  ->  ( A  i^i  ( N  i^i  n
) )  =/=  (/) )
27 neeq1 2467 . . . . . . . 8  |-  ( ( n  i^i  ( A  i^i  N ) )  =  ( A  i^i  ( N  i^i  n
) )  ->  (
( n  i^i  ( A  i^i  N ) )  =/=  (/)  <->  ( A  i^i  ( N  i^i  n
) )  =/=  (/) ) )
2826, 27syl5ibr 212 . . . . . . 7  |-  ( ( n  i^i  ( A  i^i  N ) )  =  ( A  i^i  ( N  i^i  n
) )  ->  (
( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K
) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K ) `  A ) )  /\  F  e.  ( X  ^m  A ) )  /\  n  e.  ( ( nei `  K ) `  { P } ) )  ->  ( n  i^i  ( A  i^i  N
) )  =/=  (/) ) )
298, 28syl 15 . . . . . 6  |-  ( ( ( n  i^i  ( A  i^i  N ) )  =  ( ( A  i^i  N )  i^i  n )  /\  (
( A  i^i  N
)  i^i  n )  =  ( A  i^i  ( N  i^i  n
) ) )  -> 
( ( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K
) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K ) `  A ) )  /\  F  e.  ( X  ^m  A ) )  /\  n  e.  ( ( nei `  K ) `  { P } ) )  ->  ( n  i^i  ( A  i^i  N
) )  =/=  (/) ) )
306, 7, 29mp2an 653 . . . . 5  |-  ( ( ( ( J  e. 
Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K
) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K ) `  A ) )  /\  F  e.  ( X  ^m  A ) )  /\  n  e.  ( ( nei `  K ) `  { P } ) )  ->  ( n  i^i  ( A  i^i  N
) )  =/=  (/) )
3130ralrimiva 2639 . . . 4  |-  ( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K ) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K
) `  A )
)  /\  F  e.  ( X  ^m  A ) )  ->  A. n  e.  ( ( nei `  K
) `  { P } ) ( n  i^i  ( A  i^i  N ) )  =/=  (/) )
32 ssinss1 3410 . . . . . . 7  |-  ( A 
C_  Y  ->  ( A  i^i  N )  C_  Y )
3332ad2antrl 708 . . . . . 6  |-  ( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K ) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K
) `  A )
) )  ->  ( A  i^i  N )  C_  Y )
34333adant3 975 . . . . 5  |-  ( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K ) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K
) `  A )
)  /\  F  e.  ( X  ^m  A ) )  ->  ( A  i^i  N )  C_  Y
)
3520clsss3 16812 . . . . . . . . . 10  |-  ( ( K  e.  Top  /\  A  C_  Y )  -> 
( ( cls `  K
) `  A )  C_  Y )
3635sseld 3192 . . . . . . . . 9  |-  ( ( K  e.  Top  /\  A  C_  Y )  -> 
( P  e.  ( ( cls `  K
) `  A )  ->  P  e.  Y ) )
3736ex 423 . . . . . . . 8  |-  ( K  e.  Top  ->  ( A  C_  Y  ->  ( P  e.  ( ( cls `  K ) `  A )  ->  P  e.  Y ) ) )
38373ad2ant2 977 . . . . . . 7  |-  ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K
) `  { P } ) )  -> 
( A  C_  Y  ->  ( P  e.  ( ( cls `  K
) `  A )  ->  P  e.  Y ) ) )
3938imp32 422 . . . . . 6  |-  ( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K ) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K
) `  A )
) )  ->  P  e.  Y )
40393adant3 975 . . . . 5  |-  ( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K ) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K
) `  A )
)  /\  F  e.  ( X  ^m  A ) )  ->  P  e.  Y )
4120neindisj2 16876 . . . . 5  |-  ( ( K  e.  Top  /\  ( A  i^i  N ) 
C_  Y  /\  P  e.  Y )  ->  ( P  e.  ( ( cls `  K ) `  ( A  i^i  N ) )  <->  A. n  e.  ( ( nei `  K
) `  { P } ) ( n  i^i  ( A  i^i  N ) )  =/=  (/) ) )
422, 34, 40, 41syl3anc 1182 . . . 4  |-  ( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K ) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K
) `  A )
)  /\  F  e.  ( X  ^m  A ) )  ->  ( P  e.  ( ( cls `  K
) `  ( A  i^i  N ) )  <->  A. n  e.  ( ( nei `  K
) `  { P } ) ( n  i^i  ( A  i^i  N ) )  =/=  (/) ) )
4331, 42mpbird 223 . . 3  |-  ( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K ) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K
) `  A )
)  /\  F  e.  ( X  ^m  A ) )  ->  P  e.  ( ( cls `  K
) `  ( A  i^i  N ) ) )
44 simp3 957 . . 3  |-  ( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K ) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K
) `  A )
)  /\  F  e.  ( X  ^m  A ) )  ->  F  e.  ( X  ^m  A ) )
45 islimrs.1 . . . 4  |-  L  =  ( ( ( nei `  K ) `  { P } )t  A )
46 islimrs.2 . . . 4  |-  X  = 
U. J
4745, 46, 20islimrs3 25684 . . 3  |-  ( ( ( J  e.  Top  /\  K  e.  Top  /\  ( A  i^i  N ) 
C_  A )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K ) `  ( A  i^i  N ) ) )  /\  F  e.  ( X  ^m  A
) )  ->  (
( ( J  fLimfrs  K ) `  A ) `
 <. P ,  F >. )  C_  ( (
( J  fLimfrs  K ) `
 ( A  i^i  N ) ) `  <. P ,  ( F  |`  ( A  i^i  N ) ) >. ) )
481, 2, 4, 5, 43, 44, 47syl321anc 1204 . 2  |-  ( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K ) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K
) `  A )
)  /\  F  e.  ( X  ^m  A ) )  ->  ( (
( J  fLimfrs  K ) `
 A ) `  <. P ,  F >. ) 
C_  ( ( ( J  fLimfrs  K ) `  ( A  i^i  N ) ) `  <. P , 
( F  |`  ( A  i^i  N ) )
>. ) )
49 ineq1 3376 . . . . . . . . . . . 12  |-  ( v  =  w  ->  (
v  i^i  ( A  i^i  N ) )  =  ( w  i^i  ( A  i^i  N ) ) )
5049eqeq2d 2307 . . . . . . . . . . 11  |-  ( v  =  w  ->  (
( `' ( F  |`  ( A  i^i  N
) ) " u
)  =  ( v  i^i  ( A  i^i  N ) )  <->  ( `' ( F  |`  ( A  i^i  N ) )
" u )  =  ( w  i^i  ( A  i^i  N ) ) ) )
5150cbvrexv 2778 . . . . . . . . . 10  |-  ( E. v  e.  ( ( nei `  K ) `
 { P }
) ( `' ( F  |`  ( A  i^i  N ) ) "
u )  =  ( v  i^i  ( A  i^i  N ) )  <->  E. w  e.  (
( nei `  K
) `  { P } ) ( `' ( F  |`  ( A  i^i  N ) )
" u )  =  ( w  i^i  ( A  i^i  N ) ) )
52 incom 3374 . . . . . . . . . . . . . . 15  |-  ( A  i^i  N )  =  ( N  i^i  A
)
5352ineq2i 3380 . . . . . . . . . . . . . 14  |-  ( w  i^i  ( A  i^i  N ) )  =  ( w  i^i  ( N  i^i  A ) )
54 inass 3392 . . . . . . . . . . . . . 14  |-  ( ( w  i^i  N )  i^i  A )  =  ( w  i^i  ( N  i^i  A ) )
5553, 54eqtr4i 2319 . . . . . . . . . . . . 13  |-  ( w  i^i  ( A  i^i  N ) )  =  ( ( w  i^i  N
)  i^i  A )
56 eqtr 2313 . . . . . . . . . . . . . 14  |-  ( ( ( `' ( F  |`  ( A  i^i  N
) ) " u
)  =  ( w  i^i  ( A  i^i  N ) )  /\  (
w  i^i  ( A  i^i  N ) )  =  ( ( w  i^i 
N )  i^i  A
) )  ->  ( `' ( F  |`  ( A  i^i  N ) ) " u )  =  ( ( w  i^i  N )  i^i 
A ) )
57 cnvresima 5178 . . . . . . . . . . . . . . . 16  |-  ( `' ( F  |`  ( A  i^i  N ) )
" u )  =  ( ( `' F " u )  i^i  ( A  i^i  N ) )
58 inass 3392 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( `' F "
u )  i^i  A
)  i^i  N )  =  ( ( `' F " u )  i^i  ( A  i^i  N ) )
59 eqtr 2313 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( `' F " u )  i^i  ( A  i^i  N ) )  =  ( `' ( F  |`  ( A  i^i  N ) ) "
u )  /\  ( `' ( F  |`  ( A  i^i  N ) ) " u )  =  ( ( w  i^i  N )  i^i 
A ) )  -> 
( ( `' F " u )  i^i  ( A  i^i  N ) )  =  ( ( w  i^i  N )  i^i 
A ) )
60 eqtr 2313 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( `' F " u )  i^i  A )  i^i 
N )  =  ( ( `' F "
u )  i^i  ( A  i^i  N ) )  /\  ( ( `' F " u )  i^i  ( A  i^i  N ) )  =  ( ( w  i^i  N
)  i^i  A )
)  ->  ( (
( `' F "
u )  i^i  A
)  i^i  N )  =  ( ( w  i^i  N )  i^i 
A ) )
61 cnvimass 5049 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( `' F " u ) 
C_  dom  F
62 uniexg 4533 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( J  e.  Top  ->  U. J  e.  _V )
6346, 62syl5eqel 2380 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( J  e.  Top  ->  X  e.  _V )
64 uniexg 4533 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( K  e.  Top  ->  U. K  e.  _V )
6520, 64syl5eqel 2380 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( K  e.  Top  ->  Y  e.  _V )
66 ssexg 4176 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( A  C_  Y  /\  Y  e.  _V )  ->  A  e.  _V )
6766ex 423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( A 
C_  Y  ->  ( Y  e.  _V  ->  A  e.  _V ) )
68 elmapg 6801 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( X  e.  _V  /\  A  e.  _V )  ->  ( F  e.  ( X  ^m  A )  <-> 
F : A --> X ) )
6968biimpd 198 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( X  e.  _V  /\  A  e.  _V )  ->  ( F  e.  ( X  ^m  A )  ->  F : A --> X ) )
7069expcom 424 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( A  e.  _V  ->  ( X  e.  _V  ->  ( F  e.  ( X  ^m  A )  ->  F : A --> X ) ) )
7167, 70syl6 29 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( A 
C_  Y  ->  ( Y  e.  _V  ->  ( X  e.  _V  ->  ( F  e.  ( X  ^m  A )  ->  F : A --> X ) ) ) )
7271com13 74 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( X  e.  _V  ->  ( Y  e.  _V  ->  ( A  C_  Y  ->  ( F  e.  ( X  ^m  A )  ->  F : A --> X ) ) ) )
7372imp 418 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( X  e.  _V  /\  Y  e.  _V )  ->  ( A  C_  Y  ->  ( F  e.  ( X  ^m  A )  ->  F : A --> X ) ) )
7463, 65, 73syl2an 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( J  e.  Top  /\  K  e.  Top )  ->  ( A  C_  Y  ->  ( F  e.  ( X  ^m  A )  ->  F : A --> X ) ) )
75743adant3 975 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K
) `  { P } ) )  -> 
( A  C_  Y  ->  ( F  e.  ( X  ^m  A )  ->  F : A --> X ) ) )
7675adantrd 454 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K
) `  { P } ) )  -> 
( ( A  C_  Y  /\  P  e.  ( ( cls `  K
) `  A )
)  ->  ( F  e.  ( X  ^m  A
)  ->  F : A
--> X ) ) )
77763imp 1145 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K ) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K
) `  A )
)  /\  F  e.  ( X  ^m  A ) )  ->  F : A
--> X )
7877ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K
) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K ) `  A ) )  /\  F  e.  ( X  ^m  A ) )  /\  x  e.  X )  /\  u  e.  (
( nei `  J
) `  { x } ) )  ->  F : A --> X )
79 fdm 5409 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( F : A --> X  ->  dom  F  =  A )
8078, 79syl 15 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K
) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K ) `  A ) )  /\  F  e.  ( X  ^m  A ) )  /\  x  e.  X )  /\  u  e.  (
( nei `  J
) `  { x } ) )  ->  dom  F  =  A )
8161, 80syl5sseq 3239 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K
) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K ) `  A ) )  /\  F  e.  ( X  ^m  A ) )  /\  x  e.  X )  /\  u  e.  (
( nei `  J
) `  { x } ) )  -> 
( `' F "
u )  C_  A
)
82 df-ss 3179 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( `' F " u ) 
C_  A  <->  ( ( `' F " u )  i^i  A )  =  ( `' F "
u ) )
83 ineq1 3376 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( `' F "
u )  i^i  A
)  =  ( `' F " u )  ->  ( ( ( `' F " u )  i^i  A )  i^i 
N )  =  ( ( `' F "
u )  i^i  N
) )
84 eqtr 2313 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( `' F " u )  i^i  N
)  =  ( ( ( `' F "
u )  i^i  A
)  i^i  N )  /\  ( ( ( `' F " u )  i^i  A )  i^i 
N )  =  ( ( w  i^i  N
)  i^i  A )
)  ->  ( ( `' F " u )  i^i  N )  =  ( ( w  i^i 
N )  i^i  A
) )
85 inundif 3545 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( `' F "
u )  i^i  N
)  u.  ( ( `' F " u ) 
\  N ) )  =  ( `' F " u )
86 uneq1 3335 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( `' F "
u )  i^i  N
)  =  ( ( w  i^i  N )  i^i  A )  -> 
( ( ( `' F " u )  i^i  N )  u.  ( ( `' F " u )  \  N
) )  =  ( ( ( w  i^i 
N )  i^i  A
)  u.  ( ( `' F " u ) 
\  N ) ) )
87 eqtr 2313 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( `' F "
u )  =  ( ( ( `' F " u )  i^i  N
)  u.  ( ( `' F " u ) 
\  N ) )  /\  ( ( ( `' F " u )  i^i  N )  u.  ( ( `' F " u )  \  N
) )  =  ( ( ( w  i^i 
N )  i^i  A
)  u.  ( ( `' F " u ) 
\  N ) ) )  ->  ( `' F " u )  =  ( ( ( w  i^i  N )  i^i 
A )  u.  (
( `' F "
u )  \  N
) ) )
88 undir 3431 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( w  i^i  N
)  i^i  A )  u.  ( ( `' F " u )  \  N
) )  =  ( ( ( w  i^i 
N )  u.  (
( `' F "
u )  \  N
) )  i^i  ( A  u.  ( ( `' F " u ) 
\  N ) ) )
89 difss 3316 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( `' F " u ) 
\  N )  C_  ( `' F " u )
90 eqtr 2313 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( `' F "
u )  =  ( ( ( w  i^i 
N )  i^i  A
)  u.  ( ( `' F " u ) 
\  N ) )  /\  ( ( ( w  i^i  N )  i^i  A )  u.  ( ( `' F " u )  \  N
) )  =  ( ( ( w  i^i 
N )  u.  (
( `' F "
u )  \  N
) )  i^i  ( A  u.  ( ( `' F " u ) 
\  N ) ) ) )  ->  ( `' F " u )  =  ( ( ( w  i^i  N )  u.  ( ( `' F " u ) 
\  N ) )  i^i  ( A  u.  ( ( `' F " u )  \  N
) ) ) )
91 sstr 3200 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ( ( `' F " u )  \  N
)  C_  ( `' F " u )  /\  ( `' F " u ) 
C_  A )  -> 
( ( `' F " u )  \  N
)  C_  A )
92 ssequn1 3358 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( ( `' F "
u )  \  N
)  C_  A  <->  ( (
( `' F "
u )  \  N
)  u.  A )  =  A )
93 uncom 3332 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( A  u.  ( ( `' F " u ) 
\  N ) )  =  ( ( ( `' F " u ) 
\  N )  u.  A )
94 eqtr 2313 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( ( ( A  u.  (
( `' F "
u )  \  N
) )  =  ( ( ( `' F " u )  \  N
)  u.  A )  /\  ( ( ( `' F " u ) 
\  N )  u.  A )  =  A )  ->  ( A  u.  ( ( `' F " u )  \  N
) )  =  A )
9594ineq2d 3383 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( ( A  u.  (
( `' F "
u )  \  N
) )  =  ( ( ( `' F " u )  \  N
)  u.  A )  /\  ( ( ( `' F " u ) 
\  N )  u.  A )  =  A )  ->  ( (
( w  i^i  N
)  u.  ( ( `' F " u ) 
\  N ) )  i^i  ( A  u.  ( ( `' F " u )  \  N
) ) )  =  ( ( ( w  i^i  N )  u.  ( ( `' F " u )  \  N
) )  i^i  A
) )
96 eqtr 2313 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( ( ( `' F "
u )  =  ( ( ( w  i^i 
N )  u.  (
( `' F "
u )  \  N
) )  i^i  ( A  u.  ( ( `' F " u ) 
\  N ) ) )  /\  ( ( ( w  i^i  N
)  u.  ( ( `' F " u ) 
\  N ) )  i^i  ( A  u.  ( ( `' F " u )  \  N
) ) )  =  ( ( ( w  i^i  N )  u.  ( ( `' F " u )  \  N
) )  i^i  A
) )  ->  ( `' F " u )  =  ( ( ( w  i^i  N )  u.  ( ( `' F " u ) 
\  N ) )  i^i  A ) )
97 simpl12 1031 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( ( ( ( J  e. 
Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K
) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K ) `  A ) )  /\  F  e.  ( X  ^m  A ) )  /\  x  e.  X )  ->  K  e.  Top )
9897ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( ( ( ( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K
) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K ) `  A ) )  /\  F  e.  ( X  ^m  A ) )  /\  x  e.  X )  /\  u  e.  (
( nei `  J
) `  { x } ) )  /\  w  e.  ( ( nei `  K ) `  { P } ) )  ->  K  e.  Top )
99 simpr 447 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( ( ( ( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K
) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K ) `  A ) )  /\  F  e.  ( X  ^m  A ) )  /\  x  e.  X )  /\  u  e.  (
( nei `  J
) `  { x } ) )  /\  w  e.  ( ( nei `  K ) `  { P } ) )  ->  w  e.  ( ( nei `  K
) `  { P } ) )
100 simpl13 1032 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52  |-  ( ( ( ( J  e. 
Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K
) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K ) `  A ) )  /\  F  e.  ( X  ^m  A ) )  /\  x  e.  X )  ->  N  e.  ( ( nei `  K ) `
 { P }
) )
101100ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( ( ( ( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K
) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K ) `  A ) )  /\  F  e.  ( X  ^m  A ) )  /\  x  e.  X )  /\  u  e.  (
( nei `  J
) `  { x } ) )  /\  w  e.  ( ( nei `  K ) `  { P } ) )  ->  N  e.  ( ( nei `  K
) `  { P } ) )
102 innei 16878 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( ( K  e.  Top  /\  w  e.  ( ( nei `  K ) `  { P } )  /\  N  e.  ( ( nei `  K ) `  { P } ) )  ->  ( w  i^i 
N )  e.  ( ( nei `  K
) `  { P } ) )
10398, 99, 101, 102syl3anc 1182 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( ( ( ( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K
) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K ) `  A ) )  /\  F  e.  ( X  ^m  A ) )  /\  x  e.  X )  /\  u  e.  (
( nei `  J
) `  { x } ) )  /\  w  e.  ( ( nei `  K ) `  { P } ) )  ->  ( w  i^i 
N )  e.  ( ( nei `  K
) `  { P } ) )
10497adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54  |-  ( ( ( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K
) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K ) `  A ) )  /\  F  e.  ( X  ^m  A ) )  /\  x  e.  X )  /\  u  e.  (
( nei `  J
) `  { x } ) )  ->  K  e.  Top )
10520neii1 16859 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54  |-  ( ( K  e.  Top  /\  w  e.  ( ( nei `  K ) `  { P } ) )  ->  w  C_  Y
)
106104, 105sylan 457 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53  |-  ( ( ( ( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K
) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K ) `  A ) )  /\  F  e.  ( X  ^m  A ) )  /\  x  e.  X )  /\  u  e.  (
( nei `  J
) `  { x } ) )  /\  w  e.  ( ( nei `  K ) `  { P } ) )  ->  w  C_  Y
)
107 ssinss1 3410 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53  |-  ( w 
C_  Y  ->  (
w  i^i  N )  C_  Y )
108106, 107syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52  |-  ( ( ( ( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K
) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K ) `  A ) )  /\  F  e.  ( X  ^m  A ) )  /\  x  e.  X )  /\  u  e.  (
( nei `  J
) `  { x } ) )  /\  w  e.  ( ( nei `  K ) `  { P } ) )  ->  ( w  i^i 
N )  C_  Y
)
10981adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54  |-  ( ( ( ( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K
) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K ) `  A ) )  /\  F  e.  ( X  ^m  A ) )  /\  x  e.  X )  /\  u  e.  (
( nei `  J
) `  { x } ) )  /\  w  e.  ( ( nei `  K ) `  { P } ) )  ->  ( `' F " u )  C_  A
)
110 simpl2l 1008 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55  |-  ( ( ( ( J  e. 
Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K
) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K ) `  A ) )  /\  F  e.  ( X  ^m  A ) )  /\  x  e.  X )  ->  A  C_  Y )
111110ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54  |-  ( ( ( ( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K
) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K ) `  A ) )  /\  F  e.  ( X  ^m  A ) )  /\  x  e.  X )  /\  u  e.  (
( nei `  J
) `  { x } ) )  /\  w  e.  ( ( nei `  K ) `  { P } ) )  ->  A  C_  Y
)
112109, 111sstrd 3202 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53  |-  ( ( ( ( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K
) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K ) `  A ) )  /\  F  e.  ( X  ^m  A ) )  /\  x  e.  X )  /\  u  e.  (
( nei `  J
) `  { x } ) )  /\  w  e.  ( ( nei `  K ) `  { P } ) )  ->  ( `' F " u )  C_  Y
)
113 ssdifss 3320 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53  |-  ( ( `' F " u ) 
C_  Y  ->  (
( `' F "
u )  \  N
)  C_  Y )
114112, 113syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52  |-  ( ( ( ( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K
) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K ) `  A ) )  /\  F  e.  ( X  ^m  A ) )  /\  x  e.  X )  /\  u  e.  (
( nei `  J
) `  { x } ) )  /\  w  e.  ( ( nei `  K ) `  { P } ) )  ->  ( ( `' F " u ) 
\  N )  C_  Y )
115108, 114unssd 3364 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( ( ( ( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K
) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K ) `  A ) )  /\  F  e.  ( X  ^m  A ) )  /\  x  e.  X )  /\  u  e.  (
( nei `  J
) `  { x } ) )  /\  w  e.  ( ( nei `  K ) `  { P } ) )  ->  ( ( w  i^i  N )  u.  ( ( `' F " u )  \  N
) )  C_  Y
)
116 ssun1 3351 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( w  i^i  N )  C_  ( ( w  i^i 
N )  u.  (
( `' F "
u )  \  N
) )
117115, 116jctil 523 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( ( ( ( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K
) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K ) `  A ) )  /\  F  e.  ( X  ^m  A ) )  /\  x  e.  X )  /\  u  e.  (
( nei `  J
) `  { x } ) )  /\  w  e.  ( ( nei `  K ) `  { P } ) )  ->  ( ( w  i^i  N )  C_  ( ( w  i^i 
N )  u.  (
( `' F "
u )  \  N
) )  /\  (
( w  i^i  N
)  u.  ( ( `' F " u ) 
\  N ) ) 
C_  Y ) )
11898, 103, 117jca31 520 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( ( ( ( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K
) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K ) `  A ) )  /\  F  e.  ( X  ^m  A ) )  /\  x  e.  X )  /\  u  e.  (
( nei `  J
) `  { x } ) )  /\  w  e.  ( ( nei `  K ) `  { P } ) )  ->  ( ( K  e.  Top  /\  (
w  i^i  N )  e.  ( ( nei `  K
) `  { P } ) )  /\  ( ( w  i^i 
N )  C_  (
( w  i^i  N
)  u.  ( ( `' F " u ) 
\  N ) )  /\  ( ( w  i^i  N )  u.  ( ( `' F " u )  \  N
) )  C_  Y
) ) )
119118ex 423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( ( ( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K
) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K ) `  A ) )  /\  F  e.  ( X  ^m  A ) )  /\  x  e.  X )  /\  u  e.  (
( nei `  J
) `  { x } ) )  -> 
( w  e.  ( ( nei `  K
) `  { P } )  ->  (
( K  e.  Top  /\  ( w  i^i  N
)  e.  ( ( nei `  K ) `
 { P }
) )  /\  (
( w  i^i  N
)  C_  ( (
w  i^i  N )  u.  ( ( `' F " u )  \  N
) )  /\  (
( w  i^i  N
)  u.  ( ( `' F " u ) 
\  N ) ) 
C_  Y ) ) ) )
12020ssnei2 16869 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( ( ( K  e.  Top  /\  ( w  i^i  N
)  e.  ( ( nei `  K ) `
 { P }
) )  /\  (
( w  i^i  N
)  C_  ( (
w  i^i  N )  u.  ( ( `' F " u )  \  N
) )  /\  (
( w  i^i  N
)  u.  ( ( `' F " u ) 
\  N ) ) 
C_  Y ) )  ->  ( ( w  i^i  N )  u.  ( ( `' F " u )  \  N
) )  e.  ( ( nei `  K
) `  { P } ) )
121119, 120syl6 29 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( ( ( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K
) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K ) `  A ) )  /\  F  e.  ( X  ^m  A ) )  /\  x  e.  X )  /\  u  e.  (
( nei `  J
) `  { x } ) )  -> 
( w  e.  ( ( nei `  K
) `  { P } )  ->  (
( w  i^i  N
)  u.  ( ( `' F " u ) 
\  N ) )  e.  ( ( nei `  K ) `  { P } ) ) )
122 ineq1 3376 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( v  =  ( ( w  i^i  N )  u.  ( ( `' F " u )  \  N
) )  ->  (
v  i^i  A )  =  ( ( ( w  i^i  N )  u.  ( ( `' F " u ) 
\  N ) )  i^i  A ) )
123122eqeq2d 2307 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( v  =  ( ( w  i^i  N )  u.  ( ( `' F " u )  \  N
) )  ->  (
( `' F "
u )  =  ( v  i^i  A )  <-> 
( `' F "
u )  =  ( ( ( w  i^i 
N )  u.  (
( `' F "
u )  \  N
) )  i^i  A
) ) )
124123rspcev 2897 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( ( ( ( w  i^i 
N )  u.  (
( `' F "
u )  \  N
) )  e.  ( ( nei `  K
) `  { P } )  /\  ( `' F " u )  =  ( ( ( w  i^i  N )  u.  ( ( `' F " u ) 
\  N ) )  i^i  A ) )  ->  E. v  e.  ( ( nei `  K
) `  { P } ) ( `' F " u )  =  ( v  i^i 
A ) )
125124ex 423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( ( ( w  i^i  N
)  u.  ( ( `' F " u ) 
\  N ) )  e.  ( ( nei `  K ) `  { P } )  ->  (
( `' F "
u )  =  ( ( ( w  i^i 
N )  u.  (
( `' F "
u )  \  N
) )  i^i  A
)  ->  E. v  e.  ( ( nei `  K
) `  { P } ) ( `' F " u )  =  ( v  i^i 
A ) ) )
126121, 125syl6 29 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( ( ( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K
) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K ) `  A ) )  /\  F  e.  ( X  ^m  A ) )  /\  x  e.  X )  /\  u  e.  (
( nei `  J
) `  { x } ) )  -> 
( w  e.  ( ( nei `  K
) `  { P } )  ->  (
( `' F "
u )  =  ( ( ( w  i^i 
N )  u.  (
( `' F "
u )  \  N
) )  i^i  A
)  ->  E. v  e.  ( ( nei `  K
) `  { P } ) ( `' F " u )  =  ( v  i^i 
A ) ) ) )
127126com3r 73 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( ( `' F " u )  =  ( ( ( w  i^i  N )  u.  ( ( `' F " u ) 
\  N ) )  i^i  A )  -> 
( ( ( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K ) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K
) `  A )
)  /\  F  e.  ( X  ^m  A ) )  /\  x  e.  X )  /\  u  e.  ( ( nei `  J
) `  { x } ) )  -> 
( w  e.  ( ( nei `  K
) `  { P } )  ->  E. v  e.  ( ( nei `  K
) `  { P } ) ( `' F " u )  =  ( v  i^i 
A ) ) ) )
12896, 127syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( ( ( `' F "
u )  =  ( ( ( w  i^i 
N )  u.  (
( `' F "
u )  \  N
) )  i^i  ( A  u.  ( ( `' F " u ) 
\  N ) ) )  /\  ( ( ( w  i^i  N
)  u.  ( ( `' F " u ) 
\  N ) )  i^i  ( A  u.  ( ( `' F " u )  \  N
) ) )  =  ( ( ( w  i^i  N )  u.  ( ( `' F " u )  \  N
) )  i^i  A
) )  ->  (
( ( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K
) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K ) `  A ) )  /\  F  e.  ( X  ^m  A ) )  /\  x  e.  X )  /\  u  e.  (
( nei `  J
) `  { x } ) )  -> 
( w  e.  ( ( nei `  K
) `  { P } )  ->  E. v  e.  ( ( nei `  K
) `  { P } ) ( `' F " u )  =  ( v  i^i 
A ) ) ) )
129128ex 423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( ( `' F " u )  =  ( ( ( w  i^i  N )  u.  ( ( `' F " u ) 
\  N ) )  i^i  ( A  u.  ( ( `' F " u )  \  N
) ) )  -> 
( ( ( ( w  i^i  N )  u.  ( ( `' F " u ) 
\  N ) )  i^i  ( A  u.  ( ( `' F " u )  \  N
) ) )  =  ( ( ( w  i^i  N )  u.  ( ( `' F " u )  \  N
) )  i^i  A
)  ->  ( (
( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K
) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K ) `  A ) )  /\  F  e.  ( X  ^m  A ) )  /\  x  e.  X )  /\  u  e.  (
( nei `  J
) `  { x } ) )  -> 
( w  e.  ( ( nei `  K
) `  { P } )  ->  E. v  e.  ( ( nei `  K
) `  { P } ) ( `' F " u )  =  ( v  i^i 
A ) ) ) ) )
130129com3l 75 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( ( ( w  i^i 
N )  u.  (
( `' F "
u )  \  N
) )  i^i  ( A  u.  ( ( `' F " u ) 
\  N ) ) )  =  ( ( ( w  i^i  N
)  u.  ( ( `' F " u ) 
\  N ) )  i^i  A )  -> 
( ( ( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K ) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K
) `  A )
)  /\  F  e.  ( X  ^m  A ) )  /\  x  e.  X )  /\  u  e.  ( ( nei `  J
) `  { x } ) )  -> 
( ( `' F " u )  =  ( ( ( w  i^i 
N )  u.  (
( `' F "
u )  \  N
) )  i^i  ( A  u.  ( ( `' F " u ) 
\  N ) ) )  ->  ( w  e.  ( ( nei `  K
) `  { P } )  ->  E. v  e.  ( ( nei `  K
) `  { P } ) ( `' F " u )  =  ( v  i^i 
A ) ) ) ) )
13195, 130syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( ( A  u.  (
( `' F "
u )  \  N
) )  =  ( ( ( `' F " u )  \  N
)  u.  A )  /\  ( ( ( `' F " u ) 
\  N )  u.  A )  =  A )  ->  ( (
( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K
) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K ) `  A ) )  /\  F  e.  ( X  ^m  A ) )  /\  x  e.  X )  /\  u  e.  (
( nei `  J
) `  { x } ) )  -> 
( ( `' F " u )  =  ( ( ( w  i^i 
N )  u.  (
( `' F "
u )  \  N
) )  i^i  ( A  u.  ( ( `' F " u ) 
\  N ) ) )  ->  ( w  e.  ( ( nei `  K
) `  { P } )  ->  E. v  e.  ( ( nei `  K
) `  { P } ) ( `' F " u )  =  ( v  i^i 
A ) ) ) ) )
13293, 131mpan 651 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( ( ( `' F " u )  \  N
)  u.  A )  =  A  ->  (
( ( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K
) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K ) `  A ) )  /\  F  e.  ( X  ^m  A ) )  /\  x  e.  X )  /\  u  e.  (
( nei `  J
) `  { x } ) )  -> 
( ( `' F " u )  =  ( ( ( w  i^i 
N )  u.  (
( `' F "
u )  \  N
) )  i^i  ( A  u.  ( ( `' F " u ) 
\  N ) ) )  ->  ( w  e.  ( ( nei `  K
) `  { P } )  ->  E. v  e.  ( ( nei `  K
) `  { P } ) ( `' F " u )  =  ( v  i^i 
A ) ) ) ) )
13392, 132sylbi 187 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ( `' F "
u )  \  N
)  C_  A  ->  ( ( ( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K
) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K ) `  A ) )  /\  F  e.  ( X  ^m  A ) )  /\  x  e.  X )  /\  u  e.  (
( nei `  J
) `  { x } ) )  -> 
( ( `' F " u )  =  ( ( ( w  i^i 
N )  u.  (
( `' F "
u )  \  N
) )  i^i  ( A  u.  ( ( `' F " u ) 
\  N ) ) )  ->  ( w  e.  ( ( nei `  K
) `  { P } )  ->  E. v  e.  ( ( nei `  K
) `  { P } ) ( `' F " u )  =  ( v  i^i 
A ) ) ) ) )
13491, 133syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ( ( `' F " u )  \  N
)  C_  ( `' F " u )  /\  ( `' F " u ) 
C_  A )  -> 
( ( ( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K ) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K
) `  A )
)  /\  F  e.  ( X  ^m  A ) )  /\  x  e.  X )  /\  u  e.  ( ( nei `  J
) `  { x } ) )  -> 
( ( `' F " u )  =  ( ( ( w  i^i 
N )  u.  (
( `' F "
u )  \  N
) )  i^i  ( A  u.  ( ( `' F " u ) 
\  N ) ) )  ->  ( w  e.  ( ( nei `  K
) `  { P } )  ->  E. v  e.  ( ( nei `  K
) `  { P } ) ( `' F " u )  =  ( v  i^i 
A ) ) ) ) )
135134ex 423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( `' F "
u )  \  N
)  C_  ( `' F " u )  -> 
( ( `' F " u )  C_  A  ->  ( ( ( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K ) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K
) `  A )
)  /\  F  e.  ( X  ^m  A ) )  /\  x  e.  X )  /\  u  e.  ( ( nei `  J
) `  { x } ) )  -> 
( ( `' F " u )  =  ( ( ( w  i^i 
N )  u.  (
( `' F "
u )  \  N
) )  i^i  ( A  u.  ( ( `' F " u ) 
\  N ) ) )  ->  ( w  e.  ( ( nei `  K
) `  { P } )  ->  E. v  e.  ( ( nei `  K
) `  { P } ) ( `' F " u )  =  ( v  i^i 
A ) ) ) ) ) )
136135com3l 75 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( `' F " u ) 
C_  A  ->  (
( ( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K
) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K ) `  A ) )  /\  F  e.  ( X  ^m  A ) )  /\  x  e.  X )  /\  u  e.  (
( nei `  J
) `  { x } ) )  -> 
( ( ( `' F " u ) 
\  N )  C_  ( `' F " u )  ->  ( ( `' F " u )  =  ( ( ( w  i^i  N )  u.  ( ( `' F " u ) 
\  N ) )  i^i  ( A  u.  ( ( `' F " u )  \  N
) ) )  -> 
( w  e.  ( ( nei `  K
) `  { P } )  ->  E. v  e.  ( ( nei `  K
) `  { P } ) ( `' F " u )  =  ( v  i^i 
A ) ) ) ) ) )
13781, 136mpcom 32 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K
) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K ) `  A ) )  /\  F  e.  ( X  ^m  A ) )  /\  x  e.  X )  /\  u  e.  (
( nei `  J
) `  { x } ) )  -> 
( ( ( `' F " u ) 
\  N )  C_  ( `' F " u )  ->  ( ( `' F " u )  =  ( ( ( w  i^i  N )  u.  ( ( `' F " u ) 
\  N ) )  i^i  ( A  u.  ( ( `' F " u )  \  N
) ) )  -> 
( w  e.  ( ( nei `  K
) `  { P } )  ->  E. v  e.  ( ( nei `  K
) `  { P } ) ( `' F " u )  =  ( v  i^i 
A ) ) ) ) )
138137com3l 75 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( `' F "
u )  \  N
)  C_  ( `' F " u )  -> 
( ( `' F " u )  =  ( ( ( w  i^i 
N )  u.  (
( `' F "
u )  \  N
) )  i^i  ( A  u.  ( ( `' F " u ) 
\  N ) ) )  ->  ( (
( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K
) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K ) `  A ) )  /\  F  e.  ( X  ^m  A ) )  /\  x  e.  X )  /\  u  e.  (
( nei `  J
) `  { x } ) )  -> 
( w  e.  ( ( nei `  K
) `  { P } )  ->  E. v  e.  ( ( nei `  K
) `  { P } ) ( `' F " u )  =  ( v  i^i 
A ) ) ) ) )
13989, 90, 138mpsyl 59 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( `' F "
u )  =  ( ( ( w  i^i 
N )  i^i  A
)  u.  ( ( `' F " u ) 
\  N ) )  /\  ( ( ( w  i^i  N )  i^i  A )  u.  ( ( `' F " u )  \  N
) )  =  ( ( ( w  i^i 
N )  u.  (
( `' F "
u )  \  N
) )  i^i  ( A  u.  ( ( `' F " u ) 
\  N ) ) ) )  ->  (
( ( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K
) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K ) `  A ) )  /\  F  e.  ( X  ^m  A ) )  /\  x  e.  X )  /\  u  e.  (
( nei `  J
) `  { x } ) )  -> 
( w  e.  ( ( nei `  K
) `  { P } )  ->  E. v  e.  ( ( nei `  K
) `  { P } ) ( `' F " u )  =  ( v  i^i 
A ) ) ) )
14087, 88, 139sylancl 643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( `' F "
u )  =  ( ( ( `' F " u )  i^i  N
)  u.  ( ( `' F " u ) 
\  N ) )  /\  ( ( ( `' F " u )  i^i  N )  u.  ( ( `' F " u )  \  N
) )  =  ( ( ( w  i^i 
N )  i^i  A
)  u.  ( ( `' F " u ) 
\  N ) ) )  ->  ( (
( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K
) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K ) `  A ) )  /\  F  e.  ( X  ^m  A ) )  /\  x  e.  X )  /\  u  e.  (
( nei `  J
) `  { x } ) )  -> 
( w  e.  ( ( nei `  K
) `  { P } )  ->  E. v  e.  ( ( nei `  K
) `  { P } ) ( `' F " u )  =  ( v  i^i 
A ) ) ) )
141140ex 423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( `' F " u )  =  ( ( ( `' F " u )  i^i  N )  u.  ( ( `' F " u )  \  N
) )  ->  (
( ( ( `' F " u )  i^i  N )  u.  ( ( `' F " u )  \  N
) )  =  ( ( ( w  i^i 
N )  i^i  A
)  u.  ( ( `' F " u ) 
\  N ) )  ->  ( ( ( ( ( J  e. 
Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K
) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K ) `  A ) )  /\  F  e.  ( X  ^m  A ) )  /\  x  e.  X )  /\  u  e.  (
( nei `  J
) `  { x } ) )  -> 
( w  e.  ( ( nei `  K
) `  { P } )  ->  E. v  e.  ( ( nei `  K
) `  { P } ) ( `' F " u )  =  ( v  i^i 
A ) ) ) ) )
142141eqcoms 2299 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( `' F " u )  i^i  N
)  u.  ( ( `' F " u ) 
\  N ) )  =  ( `' F " u )  ->  (
( ( ( `' F " u )  i^i  N )  u.  ( ( `' F " u )  \  N
) )  =  ( ( ( w  i^i 
N )  i^i  A
)  u.  ( ( `' F " u ) 
\  N ) )  ->  ( ( ( ( ( J  e. 
Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K
) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K ) `  A ) )  /\  F  e.  ( X  ^m  A ) )  /\  x  e.  X )  /\  u  e.  (
( nei `  J
) `  { x } ) )  -> 
( w  e.  ( ( nei `  K
) `  { P } )  ->  E. v  e.  ( ( nei `  K
) `  { P } ) ( `' F " u )  =  ( v  i^i 
A ) ) ) ) )
14385, 86, 142mpsyl 59 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( `' F "
u )  i^i  N
)  =  ( ( w  i^i  N )  i^i  A )  -> 
( ( ( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K ) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K
) `  A )
)  /\  F  e.  ( X  ^m  A ) )  /\  x  e.  X )  /\  u  e.  ( ( nei `  J
) `  { x } ) )  -> 
( w  e.  ( ( nei `  K
) `  { P } )  ->  E. v  e.  ( ( nei `  K
) `  { P } ) ( `' F " u )  =  ( v  i^i 
A ) ) ) )
14484, 143syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( `' F " u )  i^i  N
)  =  ( ( ( `' F "
u )  i^i  A
)  i^i  N )  /\  ( ( ( `' F " u )  i^i  A )  i^i 
N )  =  ( ( w  i^i  N
)  i^i  A )
)  ->  ( (
( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K
) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K ) `  A ) )  /\  F  e.  ( X  ^m  A ) )  /\  x  e.  X )  /\  u  e.  (
( nei `  J
) `  { x } ) )  -> 
( w  e.  ( ( nei `  K
) `  { P } )  ->  E. v  e.  ( ( nei `  K
) `  { P } ) ( `' F " u )  =  ( v  i^i 
A ) ) ) )
145144ex 423 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( `' F "
u )  i^i  N
)  =  ( ( ( `' F "
u )  i^i  A
)  i^i  N )  ->  ( ( ( ( `' F " u )  i^i  A )  i^i 
N )  =  ( ( w  i^i  N
)  i^i  A )  ->  ( ( ( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K ) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K
) `  A )
)  /\  F  e.  ( X  ^m  A ) )  /\  x  e.  X )  /\  u  e.  ( ( nei `  J
) `  { x } ) )  -> 
( w  e.  ( ( nei `  K
) `  { P } )  ->  E. v  e.  ( ( nei `  K
) `  { P } ) ( `' F " u )  =  ( v  i^i 
A ) ) ) ) )
146145com23 72 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( `' F "
u )  i^i  N
)  =  ( ( ( `' F "
u )  i^i  A
)  i^i  N )  ->  ( ( ( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K ) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K
) `  A )
)  /\  F  e.  ( X  ^m  A ) )  /\  x  e.  X )  /\  u  e.  ( ( nei `  J
) `  { x } ) )  -> 
( ( ( ( `' F " u )  i^i  A )  i^i 
N )  =  ( ( w  i^i  N
)  i^i  A )  ->  ( w  e.  ( ( nei `  K
) `  { P } )  ->  E. v  e.  ( ( nei `  K
) `  { P } ) ( `' F " u )  =  ( v  i^i 
A ) ) ) ) )
147146eqcoms 2299 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( `' F " u )  i^i  A
)  i^i  N )  =  ( ( `' F " u )  i^i  N )  -> 
( ( ( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K ) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K
) `  A )
)  /\  F  e.  ( X  ^m  A ) )  /\  x  e.  X )  /\  u  e.  ( ( nei `  J
) `  { x } ) )  -> 
( ( ( ( `' F " u )  i^i  A )  i^i 
N )  =  ( ( w  i^i  N
)  i^i  A )  ->  ( w  e.  ( ( nei `  K
) `  { P } )  ->  E. v  e.  ( ( nei `  K
) `  { P } ) ( `' F " u )  =  ( v  i^i 
A ) ) ) ) )
14883, 147syl 15 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( `' F "
u )  i^i  A
)  =  ( `' F " u )  ->  ( ( ( ( ( J  e. 
Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K
) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K ) `  A ) )  /\  F  e.  ( X  ^m  A ) )  /\  x  e.  X )  /\  u  e.  (
( nei `  J
) `  { x } ) )  -> 
( ( ( ( `' F " u )  i^i  A )  i^i 
N )  =  ( ( w  i^i  N
)  i^i  A )  ->  ( w  e.  ( ( nei `  K
) `  { P } )  ->  E. v  e.  ( ( nei `  K
) `  { P } ) ( `' F " u )  =  ( v  i^i 
A ) ) ) ) )
14982, 148sylbi 187 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( `' F " u ) 
C_  A  ->  (
( ( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K
) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K ) `  A ) )  /\  F  e.  ( X  ^m  A ) )  /\  x  e.  X )  /\  u  e.  (
( nei `  J
) `  { x } ) )  -> 
( ( ( ( `' F " u )  i^i  A )  i^i 
N )  =  ( ( w  i^i  N
)  i^i  A )  ->  ( w  e.  ( ( nei `  K
) `  { P } )  ->  E. v  e.  ( ( nei `  K
) `  { P } ) ( `' F " u )  =  ( v  i^i 
A ) ) ) ) )
15081, 149mpcom 32 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K
) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K ) `  A ) )  /\  F  e.  ( X  ^m  A ) )  /\  x  e.  X )  /\  u  e.  (
( nei `  J
) `  { x } ) )  -> 
( ( ( ( `' F " u )  i^i  A )  i^i 
N )  =  ( ( w  i^i  N
)  i^i  A )  ->  ( w  e.  ( ( nei `  K
) `  { P } )  ->  E. v  e.  ( ( nei `  K
) `  { P } ) ( `' F " u )  =  ( v  i^i 
A ) ) ) )
151150com3l 75 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( `' F " u )  i^i  A
)  i^i  N )  =  ( ( w  i^i  N )  i^i 
A )  ->  (
w  e.  ( ( nei `  K ) `
 { P }
)  ->  ( (
( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K
) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K ) `  A ) )  /\  F  e.  ( X  ^m  A ) )  /\  x  e.  X )  /\  u  e.  (
( nei `  J
) `  { x } ) )  ->  E. v  e.  (
( nei `  K
) `  { P } ) ( `' F " u )  =  ( v  i^i 
A ) ) ) )
15260, 151syl 15 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( `' F " u )  i^i  A )  i^i 
N )  =  ( ( `' F "
u )  i^i  ( A  i^i  N ) )  /\  ( ( `' F " u )  i^i  ( A  i^i  N ) )  =  ( ( w  i^i  N
)  i^i  A )
)  ->  ( w  e.  ( ( nei `  K
) `  { P } )  ->  (
( ( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K
) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K ) `  A ) )  /\  F  e.  ( X  ^m  A ) )  /\  x  e.  X )  /\  u  e.  (
( nei `  J
) `  { x } ) )  ->  E. v  e.  (
( nei `  K
) `  { P } ) ( `' F " u )  =  ( v  i^i 
A ) ) ) )
15358, 59, 152sylancr 644 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( `' F " u )  i^i  ( A  i^i  N ) )  =  ( `' ( F  |`  ( A  i^i  N ) ) "
u )  /\  ( `' ( F  |`  ( A  i^i  N ) ) " u )  =  ( ( w  i^i  N )  i^i 
A ) )  -> 
( w  e.  ( ( nei `  K
) `  { P } )  ->  (
( ( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K
) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K ) `  A ) )  /\  F  e.  ( X  ^m  A ) )  /\  x  e.  X )  /\  u  e.  (
( nei `  J
) `  { x } ) )  ->  E. v  e.  (
( nei `  K
) `  { P } ) ( `' F " u )  =  ( v  i^i 
A ) ) ) )
154153ex 423 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( `' F "
u )  i^i  ( A  i^i  N ) )  =  ( `' ( F  |`  ( A  i^i  N ) ) "
u )  ->  (
( `' ( F  |`  ( A  i^i  N
) ) " u
)  =  ( ( w  i^i  N )  i^i  A )  -> 
( w  e.  ( ( nei `  K
) `  { P } )  ->  (
( ( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K
) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K ) `  A ) )  /\  F  e.  ( X  ^m  A ) )  /\  x  e.  X )  /\  u  e.  (
( nei `  J
) `  { x } ) )  ->  E. v  e.  (
( nei `  K
) `  { P } ) ( `' F " u )  =  ( v  i^i 
A ) ) ) ) )
1551543impd 1165 . . . . . . . . . . . . . . . . 17  |-  ( ( ( `' F "
u )  i^i  ( A  i^i  N ) )  =  ( `' ( F  |`  ( A  i^i  N ) ) "
u )  ->  (
( ( `' ( F  |`  ( A  i^i  N ) ) "
u )  =  ( ( w  i^i  N
)  i^i  A )  /\  w  e.  (
( nei `  K
) `  { P } )  /\  (
( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K
) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K ) `  A ) )  /\  F  e.  ( X  ^m  A ) )  /\  x  e.  X )  /\  u  e.  (
( nei `  J
) `  { x } ) ) )  ->  E. v  e.  ( ( nei `  K
) `  { P } ) ( `' F " u )  =  ( v  i^i 
A ) ) )
156155eqcoms 2299 . . . . . . . . . . . . . . . 16  |-  ( ( `' ( F  |`  ( A  i^i  N ) ) " u )  =  ( ( `' F " u )  i^i  ( A  i^i  N ) )  ->  (
( ( `' ( F  |`  ( A  i^i  N ) ) "
u )  =  ( ( w  i^i  N
)  i^i  A )  /\  w  e.  (
( nei `  K
) `  { P } )  /\  (
( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K
) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K ) `  A ) )  /\  F  e.  ( X  ^m  A ) )  /\  x  e.  X )  /\  u  e.  (
( nei `  J
) `  { x } ) ) )  ->  E. v  e.  ( ( nei `  K
) `  { P } ) ( `' F " u )  =  ( v  i^i 
A ) ) )
15757, 156ax-mp 8 . . . . . . . . . . . . . . 15  |-  ( ( ( `' ( F  |`  ( A  i^i  N
) ) " u
)  =  ( ( w  i^i  N )  i^i  A )  /\  w  e.  ( ( nei `  K ) `  { P } )  /\  ( ( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K
) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K ) `  A ) )  /\  F  e.  ( X  ^m  A ) )  /\  x  e.  X )  /\  u  e.  (
( nei `  J
) `  { x } ) ) )  ->  E. v  e.  ( ( nei `  K
) `  { P } ) ( `' F " u )  =  ( v  i^i 
A ) )
1581573exp 1150 . . . . . . . . . . . . . 14  |-  ( ( `' ( F  |`  ( A  i^i  N ) ) " u )  =  ( ( w  i^i  N )  i^i 
A )  ->  (
w  e.  ( ( nei `  K ) `
 { P }
)  ->  ( (
( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K
) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K ) `  A ) )  /\  F  e.  ( X  ^m  A ) )  /\  x  e.  X )  /\  u  e.  (
( nei `  J
) `  { x } ) )  ->  E. v  e.  (
( nei `  K
) `  { P } ) ( `' F " u )  =  ( v  i^i 
A ) ) ) )
15956, 158syl 15 . . . . . . . . . . . . 13  |-  ( ( ( `' ( F  |`  ( A  i^i  N
) ) " u
)  =  ( w  i^i  ( A  i^i  N ) )  /\  (
w  i^i  ( A  i^i  N ) )  =  ( ( w  i^i 
N )  i^i  A
) )  ->  (
w  e.  ( ( nei `  K ) `
 { P }
)  ->  ( (
( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K
) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K ) `  A ) )  /\  F  e.  ( X  ^m  A ) )  /\  x  e.  X )  /\  u  e.  (
( nei `  J
) `  { x } ) )  ->  E. v  e.  (
( nei `  K
) `  { P } ) ( `' F " u )  =  ( v  i^i 
A ) ) ) )
16055, 159mpan2 652 . . . . . . . . . . . 12  |-  ( ( `' ( F  |`  ( A  i^i  N ) ) " u )  =  ( w  i^i  ( A  i^i  N
) )  ->  (
w  e.  ( ( nei `  K ) `
 { P }
)  ->  ( (
( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K
) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K ) `  A ) )  /\  F  e.  ( X  ^m  A ) )  /\  x  e.  X )  /\  u  e.  (
( nei `  J
) `  { x } ) )  ->  E. v  e.  (
( nei `  K
) `  { P } ) ( `' F " u )  =  ( v  i^i 
A ) ) ) )
161160com12 27 . . . . . . . . . . 11  |-  ( w  e.  ( ( nei `  K ) `  { P } )  ->  (
( `' ( F  |`  ( A  i^i  N
) ) " u
)  =  ( w  i^i  ( A  i^i  N ) )  ->  (
( ( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K
) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K ) `  A ) )  /\  F  e.  ( X  ^m  A ) )  /\  x  e.  X )  /\  u  e.  (
( nei `  J
) `  { x } ) )  ->  E. v  e.  (
( nei `  K
) `  { P } ) ( `' F " u )  =  ( v  i^i 
A ) ) ) )
162161rexlimiv 2674 . . . . . . . . . 10  |-  ( E. w  e.  ( ( nei `  K ) `
 { P }
) ( `' ( F  |`  ( A  i^i  N ) ) "
u )  =  ( w  i^i  ( A  i^i  N ) )  ->  ( ( ( ( ( J  e. 
Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K
) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K ) `  A ) )  /\  F  e.  ( X  ^m  A ) )  /\  x  e.  X )  /\  u  e.  (
( nei `  J
) `  { x } ) )  ->  E. v  e.  (
( nei `  K
) `  { P } ) ( `' F " u )  =  ( v  i^i 
A ) ) )
16351, 162sylbi 187 . . . . . . . . 9  |-  ( E. v  e.  ( ( nei `  K ) `
 { P }
) ( `' ( F  |`  ( A  i^i  N ) ) "
u )  =  ( v  i^i  ( A  i^i  N ) )  ->  ( ( ( ( ( J  e. 
Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K
) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K ) `  A ) )  /\  F  e.  ( X  ^m  A ) )  /\  x  e.  X )  /\  u  e.  (
( nei `  J
) `  { x } ) )  ->  E. v  e.  (
( nei `  K
) `  { P } ) ( `' F " u )  =  ( v  i^i 
A ) ) )
164163com12 27 . . . . . . . 8  |-  ( ( ( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K
) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K ) `  A ) )  /\  F  e.  ( X  ^m  A ) )  /\  x  e.  X )  /\  u  e.  (
( nei `  J
) `  { x } ) )  -> 
( E. v  e.  ( ( nei `  K
) `  { P } ) ( `' ( F  |`  ( A  i^i  N ) )
" u )  =  ( v  i^i  ( A  i^i  N ) )  ->  E. v  e.  ( ( nei `  K
) `  { P } ) ( `' F " u )  =  ( v  i^i 
A ) ) )
165 fvex 5555 . . . . . . . . 9  |-  ( ( nei `  K ) `
 { P }
)  e.  _V
166110adantr 451 . . . . . . . . . . 11  |-  ( ( ( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K
) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K ) `  A ) )  /\  F  e.  ( X  ^m  A ) )  /\  x  e.  X )  /\  u  e.  (
( nei `  J
) `  { x } ) )  ->  A  C_  Y )
16720topopn 16668 . . . . . . . . . . . 12  |-  ( K  e.  Top  ->  Y  e.  K )
168104, 167syl 15 . . . . . . . . . . 11  |-  ( ( ( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K
) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K ) `  A ) )  /\  F  e.  ( X  ^m  A ) )  /\  x  e.  X )  /\  u  e.  (
( nei `  J
) `  { x } ) )  ->  Y  e.  K )
169 ssexg 4176 . . . . . . . . . . 11  |-  ( ( A  C_  Y  /\  Y  e.  K )  ->  A  e.  _V )
170166, 168, 169syl2anc 642 . . . . . . . . . 10  |-  ( ( ( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K
) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K ) `  A ) )  /\  F  e.  ( X  ^m  A ) )  /\  x  e.  X )  /\  u  e.  (
( nei `  J
) `  { x } ) )  ->  A  e.  _V )
171 inex1g 4173 . . . . . . . . . 10  |-  ( A  e.  _V  ->  ( A  i^i  N )  e. 
_V )
172170, 171syl 15 . . . . . . . . 9  |-  ( ( ( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K
) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K ) `  A ) )  /\  F  e.  ( X  ^m  A ) )  /\  x  e.  X )  /\  u  e.  (
( nei `  J
) `  { x } ) )  -> 
( A  i^i  N
)  e.  _V )
173 elrest 13348 . . . . . . . . 9  |-  ( ( ( ( nei `  K
) `  { P } )  e.  _V  /\  ( A  i^i  N
)  e.  _V )  ->  ( ( `' ( F  |`  ( A  i^i  N ) ) "
u )  e.  ( ( ( nei `  K
) `  { P } )t  ( A  i^i  N ) )  <->  E. v  e.  ( ( nei `  K
) `  { P } ) ( `' ( F  |`  ( A  i^i  N ) )
" u )  =  ( v  i^i  ( A  i^i  N ) ) ) )
174165, 172, 173sylancr 644 . . . . . . . 8  |-  ( ( ( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K
) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K ) `  A ) )  /\  F  e.  ( X  ^m  A ) )  /\  x  e.  X )  /\  u  e.  (
( nei `  J
) `  { x } ) )  -> 
( ( `' ( F  |`  ( A  i^i  N ) ) "
u )  e.  ( ( ( nei `  K
) `  { P } )t  ( A  i^i  N ) )  <->  E. v  e.  ( ( nei `  K
) `  { P } ) ( `' ( F  |`  ( A  i^i  N ) )
" u )  =  ( v  i^i  ( A  i^i  N ) ) ) )
17545eleq2i 2360 . . . . . . . . 9  |-  ( ( `' F " u )  e.  L  <->  ( `' F " u )  e.  ( ( ( nei `  K ) `  { P } )t  A ) )
176 elrest 13348 . . . . . . . . . 10  |-  ( ( ( ( nei `  K
) `  { P } )  e.  _V  /\  A  e.  _V )  ->  ( ( `' F " u )  e.  ( ( ( nei `  K
) `  { P } )t  A )  <->  E. v  e.  ( ( nei `  K
) `  { P } ) ( `' F " u )  =  ( v  i^i 
A ) ) )
177165, 170, 176sylancr 644 . . . . . . . . 9  |-  ( ( ( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K
) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K ) `  A ) )  /\  F  e.  ( X  ^m  A ) )  /\  x  e.  X )  /\  u  e.  (
( nei `  J
) `  { x } ) )  -> 
( ( `' F " u )  e.  ( ( ( nei `  K
) `  { P } )t  A )  <->  E. v  e.  ( ( nei `  K
) `  { P } ) ( `' F " u )  =  ( v  i^i 
A ) ) )
178175, 177syl5bb 248 . . . . . . . 8  |-  ( ( ( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K
) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K ) `  A ) )  /\  F  e.  ( X  ^m  A ) )  /\  x  e.  X )  /\  u  e.  (
( nei `  J
) `  { x } ) )  -> 
( ( `' F " u )  e.  L  <->  E. v  e.  ( ( nei `  K ) `
 { P }
) ( `' F " u )  =  ( v  i^i  A ) ) )
179164, 174, 1783imtr4d 259 . . . . . . 7  |-  ( ( ( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K
) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K ) `  A ) )  /\  F  e.  ( X  ^m  A ) )  /\  x  e.  X )  /\  u  e.  (
( nei `  J
) `  { x } ) )  -> 
( ( `' ( F  |`  ( A  i^i  N ) ) "
u )  e.  ( ( ( nei `  K
) `  { P } )t  ( A  i^i  N ) )  ->  ( `' F " u )  e.  L ) )
180179ralimdva 2634 . . . . . 6  |-  ( ( ( ( J  e. 
Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K
) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K ) `  A ) )  /\  F  e.  ( X  ^m  A ) )  /\  x  e.  X )  ->  ( A. u  e.  ( ( nei `  J
) `  { x } ) ( `' ( F  |`  ( A  i^i  N ) )
" u )  e.  ( ( ( nei `  K ) `  { P } )t  ( A  i^i  N ) )  ->  A. u  e.  ( ( nei `  J
) `  { x } ) ( `' F " u )  e.  L ) )
181180imdistanda 674 . . . . 5  |-  ( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K ) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K
) `  A )
)  /\  F  e.  ( X  ^m  A ) )  ->  ( (
x  e.  X  /\  A. u  e.  ( ( nei `  J ) `
 { x }
) ( `' ( F  |`  ( A  i^i  N ) ) "
u )  e.  ( ( ( nei `  K
) `  { P } )t  ( A  i^i  N ) ) )  -> 
( x  e.  X  /\  A. u  e.  ( ( nei `  J
) `  { x } ) ( `' F " u )  e.  L ) ) )
18220toptopon 16687 . . . . . . . . 9  |-  ( K  e.  Top  <->  K  e.  (TopOn `  Y ) )
1832, 182sylib 188 . . . . . . . 8  |-  ( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K ) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K
) `  A )
)  /\  F  e.  ( X  ^m  A ) )  ->  K  e.  (TopOn `  Y ) )
184 trnei 17603 . . . . . . . 8  |-  ( ( K  e.  (TopOn `  Y )  /\  ( A  i^i  N )  C_  Y  /\  P  e.  Y
)  ->  ( P  e.  ( ( cls `  K
) `  ( A  i^i  N ) )  <->  ( (
( nei `  K
) `  { P } )t  ( A  i^i  N ) )  e.  ( Fil `  ( A  i^i  N ) ) ) )
185183, 34, 40, 184syl3anc 1182 . . . . . . 7  |-  ( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K ) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K
) `  A )
)  /\  F  e.  ( X  ^m  A ) )  ->  ( P  e.  ( ( cls `  K
) `  ( A  i^i  N ) )  <->  ( (
( nei `  K
) `  { P } )t  ( A  i^i  N ) )  e.  ( Fil `  ( A  i^i  N ) ) ) )
18643, 185mpbid 201 . . . . . 6  |-  ( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K ) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K
) `  A )
)  /\  F  e.  ( X  ^m  A ) )  ->  ( (
( nei `  K
) `  { P } )t  ( A  i^i  N ) )  e.  ( Fil `  ( A  i^i  N ) ) )
187633ad2ant1 976 . . . . . . . . . 10  |-  ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K
) `  { P } ) )  ->  X  e.  _V )
188187adantr 451 . . . . . . . . 9  |-  ( ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K ) `  { P } ) )  /\  ( A  C_  Y  /\  P  e.  ( ( cls `  K
) `  A )
) )  ->  X  e.  _V )
18920eqcomi 2300 . . . . . . . . . . . . . . . 16  |-  U. K  =  Y
190189eleq1i 2359 . . . . . . . . . . . . . . 15  |-  ( U. K  e.  _V  <->  Y  e.  _V )
19166expcom 424 . . . . . . . . . . . . . . 15  |-  ( Y  e.  _V  ->  ( A  C_  Y  ->  A  e.  _V ) )
192190, 191sylbi 187 . . . . . . . . . . . . . 14  |-  ( U. K  e.  _V  ->  ( A  C_  Y  ->  A  e.  _V ) )
19364, 192syl 15 . . . . . . . . . . . . 13  |-  ( K  e.  Top  ->  ( A  C_  Y  ->  A  e.  _V ) )
1941933ad2ant2 977 . . . . . . . . . . . 12  |-  ( ( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K
) `  { P } ) )  -> 
( A  C_  Y  ->  A  e.  _V )
)
195194com12 27 . . . . . . . . . . 11  |-  ( A 
C_  Y  ->  (
( J  e.  Top  /\  K  e.  Top  /\  N  e.  ( ( nei `  K ) `  { P } ) )  ->