MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ptbasfi Structured version   Unicode version

Theorem ptbasfi 17615
Description: The basis for the product topology can also be written as the set of finite intersections of "cylinder sets", the preimages of projections into one factor from open sets in the factor. (We have to add  X itself to the list because if  A is empty we get  ( fi `  (/) )  =  (/) while  B  =  { (/) }.) (Contributed by Mario Carneiro, 3-Feb-2015.)
Hypotheses
Ref Expression
ptbas.1  |-  B  =  { x  |  E. g ( ( g  Fn  A  /\  A. y  e.  A  (
g `  y )  e.  ( F `  y
)  /\  E. z  e.  Fin  A. y  e.  ( A  \  z
) ( g `  y )  =  U. ( F `  y ) )  /\  x  = 
X_ y  e.  A  ( g `  y
) ) }
ptbasfi.2  |-  X  = 
X_ n  e.  A  U. ( F `  n
)
Assertion
Ref Expression
ptbasfi  |-  ( ( A  e.  V  /\  F : A --> Top )  ->  B  =  ( fi
`  ( { X }  u.  ran  ( k  e.  A ,  u  e.  ( F `  k
)  |->  ( `' ( w  e.  X  |->  ( w `  k ) ) " u ) ) ) ) )
Distinct variable groups:    k, n, u, B    w, g, x, y, n, k, u, z, A    g, F, k, n, u, w, x, y, z    g, X, k, u, w, x, z    g, V, k, n, u, w, x, y, z
Allowed substitution hints:    B( x, y, z, w, g)    X( y, n)

Proof of Theorem ptbasfi
Dummy variables  s  h  m are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ptbas.1 . . . . 5  |-  B  =  { x  |  E. g ( ( g  Fn  A  /\  A. y  e.  A  (
g `  y )  e.  ( F `  y
)  /\  E. z  e.  Fin  A. y  e.  ( A  \  z
) ( g `  y )  =  U. ( F `  y ) )  /\  x  = 
X_ y  e.  A  ( g `  y
) ) }
21elpt 17606 . . . 4  |-  ( s  e.  B  <->  E. h
( ( h  Fn  A  /\  A. y  e.  A  ( h `  y )  e.  ( F `  y )  /\  E. m  e. 
Fin  A. y  e.  ( A  \  m ) ( h `  y
)  =  U. ( F `  y )
)  /\  s  =  X_ y  e.  A  ( h `  y ) ) )
3 df-3an 939 . . . . . . . 8  |-  ( ( h  Fn  A  /\  A. y  e.  A  ( h `  y )  e.  ( F `  y )  /\  E. m  e.  Fin  A. y  e.  ( A  \  m
) ( h `  y )  =  U. ( F `  y ) )  <->  ( ( h  Fn  A  /\  A. y  e.  A  (
h `  y )  e.  ( F `  y
) )  /\  E. m  e.  Fin  A. y  e.  ( A  \  m
) ( h `  y )  =  U. ( F `  y ) ) )
4 simprr 735 . . . . . . . . . . . . . 14  |-  ( ( ( ( A  e.  V  /\  F : A
--> Top )  /\  (
h  Fn  A  /\  A. y  e.  A  ( h `  y )  e.  ( F `  y ) ) )  /\  ( m  e. 
Fin  /\  A. y  e.  ( A  \  m
) ( h `  y )  =  U. ( F `  y ) ) )  ->  A. y  e.  ( A  \  m
) ( h `  y )  =  U. ( F `  y ) )
5 difeq2 3461 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A  i^i  m )  =  (/)  ->  ( A 
\  ( A  i^i  m ) )  =  ( A  \  (/) ) )
6 difin 3580 . . . . . . . . . . . . . . . . . . 19  |-  ( A 
\  ( A  i^i  m ) )  =  ( A  \  m
)
7 dif0 3700 . . . . . . . . . . . . . . . . . . 19  |-  ( A 
\  (/) )  =  A
85, 6, 73eqtr3g 2493 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  i^i  m )  =  (/)  ->  ( A 
\  m )  =  A )
98raleqdv 2912 . . . . . . . . . . . . . . . . 17  |-  ( ( A  i^i  m )  =  (/)  ->  ( A. y  e.  ( A  \  m ) ( h `
 y )  = 
U. ( F `  y )  <->  A. y  e.  A  ( h `  y )  =  U. ( F `  y ) ) )
109biimpac 474 . . . . . . . . . . . . . . . 16  |-  ( ( A. y  e.  ( A  \  m ) ( h `  y
)  =  U. ( F `  y )  /\  ( A  i^i  m
)  =  (/) )  ->  A. y  e.  A  ( h `  y
)  =  U. ( F `  y )
)
11 ixpeq2 7078 . . . . . . . . . . . . . . . 16  |-  ( A. y  e.  A  (
h `  y )  =  U. ( F `  y )  ->  X_ y  e.  A  ( h `  y )  =  X_ y  e.  A  U. ( F `  y ) )
1210, 11syl 16 . . . . . . . . . . . . . . 15  |-  ( ( A. y  e.  ( A  \  m ) ( h `  y
)  =  U. ( F `  y )  /\  ( A  i^i  m
)  =  (/) )  ->  X_ y  e.  A  ( h `  y )  =  X_ y  e.  A  U. ( F `  y
) )
13 ptbasfi.2 . . . . . . . . . . . . . . . 16  |-  X  = 
X_ n  e.  A  U. ( F `  n
)
14 fveq2 5730 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  y  ->  ( F `  n )  =  ( F `  y ) )
1514unieqd 4028 . . . . . . . . . . . . . . . . 17  |-  ( n  =  y  ->  U. ( F `  n )  =  U. ( F `  y ) )
1615cbvixpv 7082 . . . . . . . . . . . . . . . 16  |-  X_ n  e.  A  U. ( F `  n )  =  X_ y  e.  A  U. ( F `  y
)
1713, 16eqtri 2458 . . . . . . . . . . . . . . 15  |-  X  = 
X_ y  e.  A  U. ( F `  y
)
1812, 17syl6eqr 2488 . . . . . . . . . . . . . 14  |-  ( ( A. y  e.  ( A  \  m ) ( h `  y
)  =  U. ( F `  y )  /\  ( A  i^i  m
)  =  (/) )  ->  X_ y  e.  A  ( h `  y )  =  X )
194, 18sylan 459 . . . . . . . . . . . . 13  |-  ( ( ( ( ( A  e.  V  /\  F : A --> Top )  /\  (
h  Fn  A  /\  A. y  e.  A  ( h `  y )  e.  ( F `  y ) ) )  /\  ( m  e. 
Fin  /\  A. y  e.  ( A  \  m
) ( h `  y )  =  U. ( F `  y ) ) )  /\  ( A  i^i  m )  =  (/) )  ->  X_ y  e.  A  ( h `  y )  =  X )
20 ssv 3370 . . . . . . . . . . . . . . . 16  |-  X  C_  _V
21 iineq1 4109 . . . . . . . . . . . . . . . . 17  |-  ( ( A  i^i  m )  =  (/)  ->  |^|_ n  e.  ( A  i^i  m
) ( `' ( w  e.  X  |->  ( w `  n ) ) " ( h `
 n ) )  =  |^|_ n  e.  (/)  ( `' ( w  e.  X  |->  ( w `  n ) ) "
( h `  n
) ) )
22 0iin 4151 . . . . . . . . . . . . . . . . 17  |-  |^|_ n  e.  (/)  ( `' ( w  e.  X  |->  ( w `  n ) ) " ( h `
 n ) )  =  _V
2321, 22syl6eq 2486 . . . . . . . . . . . . . . . 16  |-  ( ( A  i^i  m )  =  (/)  ->  |^|_ n  e.  ( A  i^i  m
) ( `' ( w  e.  X  |->  ( w `  n ) ) " ( h `
 n ) )  =  _V )
2420, 23syl5sseqr 3399 . . . . . . . . . . . . . . 15  |-  ( ( A  i^i  m )  =  (/)  ->  X  C_  |^|_
n  e.  ( A  i^i  m ) ( `' ( w  e.  X  |->  ( w `  n ) ) "
( h `  n
) ) )
2524adantl 454 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( A  e.  V  /\  F : A --> Top )  /\  (
h  Fn  A  /\  A. y  e.  A  ( h `  y )  e.  ( F `  y ) ) )  /\  ( m  e. 
Fin  /\  A. y  e.  ( A  \  m
) ( h `  y )  =  U. ( F `  y ) ) )  /\  ( A  i^i  m )  =  (/) )  ->  X  C_  |^|_
n  e.  ( A  i^i  m ) ( `' ( w  e.  X  |->  ( w `  n ) ) "
( h `  n
) ) )
26 df-ss 3336 . . . . . . . . . . . . . 14  |-  ( X 
C_  |^|_ n  e.  ( A  i^i  m ) ( `' ( w  e.  X  |->  ( w `
 n ) )
" ( h `  n ) )  <->  ( X  i^i  |^|_ n  e.  ( A  i^i  m ) ( `' ( w  e.  X  |->  ( w `
 n ) )
" ( h `  n ) ) )  =  X )
2725, 26sylib 190 . . . . . . . . . . . . 13  |-  ( ( ( ( ( A  e.  V  /\  F : A --> Top )  /\  (
h  Fn  A  /\  A. y  e.  A  ( h `  y )  e.  ( F `  y ) ) )  /\  ( m  e. 
Fin  /\  A. y  e.  ( A  \  m
) ( h `  y )  =  U. ( F `  y ) ) )  /\  ( A  i^i  m )  =  (/) )  ->  ( X  i^i  |^|_ n  e.  ( A  i^i  m ) ( `' ( w  e.  X  |->  ( w `
 n ) )
" ( h `  n ) ) )  =  X )
2819, 27eqtr4d 2473 . . . . . . . . . . . 12  |-  ( ( ( ( ( A  e.  V  /\  F : A --> Top )  /\  (
h  Fn  A  /\  A. y  e.  A  ( h `  y )  e.  ( F `  y ) ) )  /\  ( m  e. 
Fin  /\  A. y  e.  ( A  \  m
) ( h `  y )  =  U. ( F `  y ) ) )  /\  ( A  i^i  m )  =  (/) )  ->  X_ y  e.  A  ( h `  y )  =  ( X  i^i  |^|_ n  e.  ( A  i^i  m
) ( `' ( w  e.  X  |->  ( w `  n ) ) " ( h `
 n ) ) ) )
29 simplll 736 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( A  e.  V  /\  F : A --> Top )  /\  (
h  Fn  A  /\  A. y  e.  A  ( h `  y )  e.  ( F `  y ) ) )  /\  ( m  e. 
Fin  /\  A. y  e.  ( A  \  m
) ( h `  y )  =  U. ( F `  y ) ) )  /\  n  e.  ( A  i^i  m
) )  ->  ( A  e.  V  /\  F : A --> Top )
)
30 inss1 3563 . . . . . . . . . . . . . . . . 17  |-  ( A  i^i  m )  C_  A
31 simpr 449 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( A  e.  V  /\  F : A --> Top )  /\  (
h  Fn  A  /\  A. y  e.  A  ( h `  y )  e.  ( F `  y ) ) )  /\  ( m  e. 
Fin  /\  A. y  e.  ( A  \  m
) ( h `  y )  =  U. ( F `  y ) ) )  /\  n  e.  ( A  i^i  m
) )  ->  n  e.  ( A  i^i  m
) )
3230, 31sseldi 3348 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( A  e.  V  /\  F : A --> Top )  /\  (
h  Fn  A  /\  A. y  e.  A  ( h `  y )  e.  ( F `  y ) ) )  /\  ( m  e. 
Fin  /\  A. y  e.  ( A  \  m
) ( h `  y )  =  U. ( F `  y ) ) )  /\  n  e.  ( A  i^i  m
) )  ->  n  e.  A )
33 simprr 735 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( A  e.  V  /\  F : A --> Top )  /\  ( h  Fn  A  /\  A. y  e.  A  ( h `  y
)  e.  ( F `
 y ) ) )  ->  A. y  e.  A  ( h `  y )  e.  ( F `  y ) )
3433ad2antrr 708 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( A  e.  V  /\  F : A --> Top )  /\  (
h  Fn  A  /\  A. y  e.  A  ( h `  y )  e.  ( F `  y ) ) )  /\  ( m  e. 
Fin  /\  A. y  e.  ( A  \  m
) ( h `  y )  =  U. ( F `  y ) ) )  /\  n  e.  ( A  i^i  m
) )  ->  A. y  e.  A  ( h `  y )  e.  ( F `  y ) )
35 fveq2 5730 . . . . . . . . . . . . . . . . . . 19  |-  ( y  =  n  ->  (
h `  y )  =  ( h `  n ) )
36 fveq2 5730 . . . . . . . . . . . . . . . . . . 19  |-  ( y  =  n  ->  ( F `  y )  =  ( F `  n ) )
3735, 36eleq12d 2506 . . . . . . . . . . . . . . . . . 18  |-  ( y  =  n  ->  (
( h `  y
)  e.  ( F `
 y )  <->  ( h `  n )  e.  ( F `  n ) ) )
3837rspcv 3050 . . . . . . . . . . . . . . . . 17  |-  ( n  e.  A  ->  ( A. y  e.  A  ( h `  y
)  e.  ( F `
 y )  -> 
( h `  n
)  e.  ( F `
 n ) ) )
3932, 34, 38sylc 59 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( A  e.  V  /\  F : A --> Top )  /\  (
h  Fn  A  /\  A. y  e.  A  ( h `  y )  e.  ( F `  y ) ) )  /\  ( m  e. 
Fin  /\  A. y  e.  ( A  \  m
) ( h `  y )  =  U. ( F `  y ) ) )  /\  n  e.  ( A  i^i  m
) )  ->  (
h `  n )  e.  ( F `  n
) )
4017ptpjpre1 17605 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  V  /\  F : A --> Top )  /\  ( n  e.  A  /\  ( h `  n
)  e.  ( F `
 n ) ) )  ->  ( `' ( w  e.  X  |->  ( w `  n
) ) " (
h `  n )
)  =  X_ y  e.  A  if (
y  =  n ,  ( h `  n
) ,  U. ( F `  y )
) )
4129, 32, 39, 40syl12anc 1183 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( A  e.  V  /\  F : A --> Top )  /\  (
h  Fn  A  /\  A. y  e.  A  ( h `  y )  e.  ( F `  y ) ) )  /\  ( m  e. 
Fin  /\  A. y  e.  ( A  \  m
) ( h `  y )  =  U. ( F `  y ) ) )  /\  n  e.  ( A  i^i  m
) )  ->  ( `' ( w  e.  X  |->  ( w `  n ) ) "
( h `  n
) )  =  X_ y  e.  A  if ( y  =  n ,  ( h `  n ) ,  U. ( F `  y ) ) )
4241adantlr 697 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( A  e.  V  /\  F : A --> Top )  /\  ( h  Fn  A  /\  A. y  e.  A  ( h `  y
)  e.  ( F `
 y ) ) )  /\  ( m  e.  Fin  /\  A. y  e.  ( A  \  m ) ( h `
 y )  = 
U. ( F `  y ) ) )  /\  ( A  i^i  m )  =/=  (/) )  /\  n  e.  ( A  i^i  m ) )  -> 
( `' ( w  e.  X  |->  ( w `
 n ) )
" ( h `  n ) )  = 
X_ y  e.  A  if ( y  =  n ,  ( h `  n ) ,  U. ( F `  y ) ) )
4342iineq2dv 4117 . . . . . . . . . . . . 13  |-  ( ( ( ( ( A  e.  V  /\  F : A --> Top )  /\  (
h  Fn  A  /\  A. y  e.  A  ( h `  y )  e.  ( F `  y ) ) )  /\  ( m  e. 
Fin  /\  A. y  e.  ( A  \  m
) ( h `  y )  =  U. ( F `  y ) ) )  /\  ( A  i^i  m )  =/=  (/) )  ->  |^|_ n  e.  ( A  i^i  m
) ( `' ( w  e.  X  |->  ( w `  n ) ) " ( h `
 n ) )  =  |^|_ n  e.  ( A  i^i  m )
X_ y  e.  A  if ( y  =  n ,  ( h `  n ) ,  U. ( F `  y ) ) )
44 simpr 449 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( A  e.  V  /\  F : A --> Top )  /\  (
h  Fn  A  /\  A. y  e.  A  ( h `  y )  e.  ( F `  y ) ) )  /\  ( m  e. 
Fin  /\  A. y  e.  ( A  \  m
) ( h `  y )  =  U. ( F `  y ) ) )  /\  ( A  i^i  m )  =/=  (/) )  ->  ( A  i^i  m )  =/=  (/) )
45 cnvimass 5226 . . . . . . . . . . . . . . . . . . . 20  |-  ( `' ( w  e.  X  |->  ( w `  n
) ) " (
h `  n )
)  C_  dom  ( w  e.  X  |->  ( w `
 n ) )
46 eqid 2438 . . . . . . . . . . . . . . . . . . . . 21  |-  ( w  e.  X  |->  ( w `
 n ) )  =  ( w  e.  X  |->  ( w `  n ) )
4746dmmptss 5368 . . . . . . . . . . . . . . . . . . . 20  |-  dom  (
w  e.  X  |->  ( w `  n ) )  C_  X
4845, 47sstri 3359 . . . . . . . . . . . . . . . . . . 19  |-  ( `' ( w  e.  X  |->  ( w `  n
) ) " (
h `  n )
)  C_  X
4948, 17sseqtri 3382 . . . . . . . . . . . . . . . . . 18  |-  ( `' ( w  e.  X  |->  ( w `  n
) ) " (
h `  n )
)  C_  X_ y  e.  A  U. ( F `
 y )
5049rgenw 2775 . . . . . . . . . . . . . . . . 17  |-  A. n  e.  ( A  i^i  m
) ( `' ( w  e.  X  |->  ( w `  n ) ) " ( h `
 n ) ) 
C_  X_ y  e.  A  U. ( F `  y
)
51 r19.2z 3719 . . . . . . . . . . . . . . . . 17  |-  ( ( ( A  i^i  m
)  =/=  (/)  /\  A. n  e.  ( A  i^i  m ) ( `' ( w  e.  X  |->  ( w `  n
) ) " (
h `  n )
)  C_  X_ y  e.  A  U. ( F `
 y ) )  ->  E. n  e.  ( A  i^i  m ) ( `' ( w  e.  X  |->  ( w `
 n ) )
" ( h `  n ) )  C_  X_ y  e.  A  U. ( F `  y ) )
5244, 50, 51sylancl 645 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( A  e.  V  /\  F : A --> Top )  /\  (
h  Fn  A  /\  A. y  e.  A  ( h `  y )  e.  ( F `  y ) ) )  /\  ( m  e. 
Fin  /\  A. y  e.  ( A  \  m
) ( h `  y )  =  U. ( F `  y ) ) )  /\  ( A  i^i  m )  =/=  (/) )  ->  E. n  e.  ( A  i^i  m
) ( `' ( w  e.  X  |->  ( w `  n ) ) " ( h `
 n ) ) 
C_  X_ y  e.  A  U. ( F `  y
) )
53 iinss 4144 . . . . . . . . . . . . . . . 16  |-  ( E. n  e.  ( A  i^i  m ) ( `' ( w  e.  X  |->  ( w `  n ) ) "
( h `  n
) )  C_  X_ y  e.  A  U. ( F `  y )  -> 
|^|_ n  e.  ( A  i^i  m ) ( `' ( w  e.  X  |->  ( w `  n ) ) "
( h `  n
) )  C_  X_ y  e.  A  U. ( F `  y )
)
5452, 53syl 16 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( A  e.  V  /\  F : A --> Top )  /\  (
h  Fn  A  /\  A. y  e.  A  ( h `  y )  e.  ( F `  y ) ) )  /\  ( m  e. 
Fin  /\  A. y  e.  ( A  \  m
) ( h `  y )  =  U. ( F `  y ) ) )  /\  ( A  i^i  m )  =/=  (/) )  ->  |^|_ n  e.  ( A  i^i  m
) ( `' ( w  e.  X  |->  ( w `  n ) ) " ( h `
 n ) ) 
C_  X_ y  e.  A  U. ( F `  y
) )
5554, 17syl6sseqr 3397 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( A  e.  V  /\  F : A --> Top )  /\  (
h  Fn  A  /\  A. y  e.  A  ( h `  y )  e.  ( F `  y ) ) )  /\  ( m  e. 
Fin  /\  A. y  e.  ( A  \  m
) ( h `  y )  =  U. ( F `  y ) ) )  /\  ( A  i^i  m )  =/=  (/) )  ->  |^|_ n  e.  ( A  i^i  m
) ( `' ( w  e.  X  |->  ( w `  n ) ) " ( h `
 n ) ) 
C_  X )
56 dfss1 3547 . . . . . . . . . . . . . 14  |-  ( |^|_ n  e.  ( A  i^i  m ) ( `' ( w  e.  X  |->  ( w `  n
) ) " (
h `  n )
)  C_  X  <->  ( X  i^i  |^|_ n  e.  ( A  i^i  m ) ( `' ( w  e.  X  |->  ( w `
 n ) )
" ( h `  n ) ) )  =  |^|_ n  e.  ( A  i^i  m ) ( `' ( w  e.  X  |->  ( w `
 n ) )
" ( h `  n ) ) )
5755, 56sylib 190 . . . . . . . . . . . . 13  |-  ( ( ( ( ( A  e.  V  /\  F : A --> Top )  /\  (
h  Fn  A  /\  A. y  e.  A  ( h `  y )  e.  ( F `  y ) ) )  /\  ( m  e. 
Fin  /\  A. y  e.  ( A  \  m
) ( h `  y )  =  U. ( F `  y ) ) )  /\  ( A  i^i  m )  =/=  (/) )  ->  ( X  i^i  |^|_ n  e.  ( A  i^i  m ) ( `' ( w  e.  X  |->  ( w `
 n ) )
" ( h `  n ) ) )  =  |^|_ n  e.  ( A  i^i  m ) ( `' ( w  e.  X  |->  ( w `
 n ) )
" ( h `  n ) ) )
5833ad2antrr 708 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( A  e.  V  /\  F : A --> Top )  /\  (
h  Fn  A  /\  A. y  e.  A  ( h `  y )  e.  ( F `  y ) ) )  /\  ( m  e. 
Fin  /\  A. y  e.  ( A  \  m
) ( h `  y )  =  U. ( F `  y ) ) )  /\  ( A  i^i  m )  =/=  (/) )  ->  A. y  e.  A  ( h `  y )  e.  ( F `  y ) )
59 ssralv 3409 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  i^i  m ) 
C_  A  ->  ( A. y  e.  A  ( h `  y
)  e.  ( F `
 y )  ->  A. y  e.  ( A  i^i  m ) ( h `  y )  e.  ( F `  y ) ) )
6030, 59ax-mp 8 . . . . . . . . . . . . . . . . 17  |-  ( A. y  e.  A  (
h `  y )  e.  ( F `  y
)  ->  A. y  e.  ( A  i^i  m
) ( h `  y )  e.  ( F `  y ) )
61 elssuni 4045 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( h `  y )  e.  ( F `  y )  ->  (
h `  y )  C_ 
U. ( F `  y ) )
62 iffalse 3748 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( -.  y  =  n  ->  if ( y  =  n ,  ( h `  n ) ,  U. ( F `  y ) )  =  U. ( F `  y )
)
6362sseq2d 3378 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( -.  y  =  n  -> 
( ( h `  y )  C_  if ( y  =  n ,  ( h `  n ) ,  U. ( F `  y ) )  <->  ( h `  y )  C_  U. ( F `  y )
) )
6461, 63syl5ibrcom 215 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( h `  y )  e.  ( F `  y )  ->  ( -.  y  =  n  ->  ( h `  y
)  C_  if (
y  =  n ,  ( h `  n
) ,  U. ( F `  y )
) ) )
65 ssid 3369 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( h `
 y )  C_  ( h `  y
)
66 iftrue 3747 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  =  n  ->  if ( y  =  n ,  ( h `  n ) ,  U. ( F `  y ) )  =  ( h `
 n ) )
6766, 35eqtr4d 2473 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  =  n  ->  if ( y  =  n ,  ( h `  n ) ,  U. ( F `  y ) )  =  ( h `
 y ) )
6865, 67syl5sseqr 3399 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( y  =  n  ->  (
h `  y )  C_  if ( y  =  n ,  ( h `
 n ) , 
U. ( F `  y ) ) )
6964, 68pm2.61d2 155 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( h `  y )  e.  ( F `  y )  ->  (
h `  y )  C_  if ( y  =  n ,  ( h `
 n ) , 
U. ( F `  y ) ) )
7069ralrimivw 2792 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( h `  y )  e.  ( F `  y )  ->  A. n  e.  ( A  i^i  m
) ( h `  y )  C_  if ( y  =  n ,  ( h `  n ) ,  U. ( F `  y ) ) )
71 ssiin 4143 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( h `  y ) 
C_  |^|_ n  e.  ( A  i^i  m ) if ( y  =  n ,  ( h `
 n ) , 
U. ( F `  y ) )  <->  A. n  e.  ( A  i^i  m
) ( h `  y )  C_  if ( y  =  n ,  ( h `  n ) ,  U. ( F `  y ) ) )
7270, 71sylibr 205 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( h `  y )  e.  ( F `  y )  ->  (
h `  y )  C_ 
|^|_ n  e.  ( A  i^i  m ) if ( y  =  n ,  ( h `  n ) ,  U. ( F `  y ) ) )
7372adantl 454 . . . . . . . . . . . . . . . . . . 19  |-  ( ( y  e.  ( A  i^i  m )  /\  ( h `  y
)  e.  ( F `
 y ) )  ->  ( h `  y )  C_  |^|_ n  e.  ( A  i^i  m
) if ( y  =  n ,  ( h `  n ) ,  U. ( F `
 y ) ) )
7466equcoms 1694 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( n  =  y  ->  if ( y  =  n ,  ( h `  n ) ,  U. ( F `  y ) )  =  ( h `
 n ) )
75 fveq2 5730 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( n  =  y  ->  (
h `  n )  =  ( h `  y ) )
7674, 75eqtrd 2470 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( n  =  y  ->  if ( y  =  n ,  ( h `  n ) ,  U. ( F `  y ) )  =  ( h `
 y ) )
7776sseq1d 3377 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( n  =  y  ->  ( if ( y  =  n ,  ( h `  n ) ,  U. ( F `  y ) )  C_  ( h `  y )  <->  ( h `  y )  C_  (
h `  y )
) )
7877rspcev 3054 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( y  e.  ( A  i^i  m )  /\  ( h `  y
)  C_  ( h `  y ) )  ->  E. n  e.  ( A  i^i  m ) if ( y  =  n ,  ( h `  n ) ,  U. ( F `  y ) )  C_  ( h `  y ) )
7965, 78mpan2 654 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  e.  ( A  i^i  m )  ->  E. n  e.  ( A  i^i  m
) if ( y  =  n ,  ( h `  n ) ,  U. ( F `
 y ) ) 
C_  ( h `  y ) )
80 iinss 4144 . . . . . . . . . . . . . . . . . . . . 21  |-  ( E. n  e.  ( A  i^i  m ) if ( y  =  n ,  ( h `  n ) ,  U. ( F `  y ) )  C_  ( h `  y )  ->  |^|_ n  e.  ( A  i^i  m
) if ( y  =  n ,  ( h `  n ) ,  U. ( F `
 y ) ) 
C_  ( h `  y ) )
8179, 80syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  ( A  i^i  m )  ->  |^|_ n  e.  ( A  i^i  m
) if ( y  =  n ,  ( h `  n ) ,  U. ( F `
 y ) ) 
C_  ( h `  y ) )
8281adantr 453 . . . . . . . . . . . . . . . . . . 19  |-  ( ( y  e.  ( A  i^i  m )  /\  ( h `  y
)  e.  ( F `
 y ) )  ->  |^|_ n  e.  ( A  i^i  m ) if ( y  =  n ,  ( h `
 n ) , 
U. ( F `  y ) )  C_  ( h `  y
) )
8373, 82eqssd 3367 . . . . . . . . . . . . . . . . . 18  |-  ( ( y  e.  ( A  i^i  m )  /\  ( h `  y
)  e.  ( F `
 y ) )  ->  ( h `  y )  =  |^|_ n  e.  ( A  i^i  m ) if ( y  =  n ,  ( h `  n
) ,  U. ( F `  y )
) )
8483ralimiaa 2782 . . . . . . . . . . . . . . . . 17  |-  ( A. y  e.  ( A  i^i  m ) ( h `
 y )  e.  ( F `  y
)  ->  A. y  e.  ( A  i^i  m
) ( h `  y )  =  |^|_ n  e.  ( A  i^i  m ) if ( y  =  n ,  ( h `  n
) ,  U. ( F `  y )
) )
8558, 60, 843syl 19 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( A  e.  V  /\  F : A --> Top )  /\  (
h  Fn  A  /\  A. y  e.  A  ( h `  y )  e.  ( F `  y ) ) )  /\  ( m  e. 
Fin  /\  A. y  e.  ( A  \  m
) ( h `  y )  =  U. ( F `  y ) ) )  /\  ( A  i^i  m )  =/=  (/) )  ->  A. y  e.  ( A  i^i  m
) ( h `  y )  =  |^|_ n  e.  ( A  i^i  m ) if ( y  =  n ,  ( h `  n
) ,  U. ( F `  y )
) )
86 eldifn 3472 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  e.  ( A  \  m )  ->  -.  y  e.  m )
8786ad2antlr 709 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( A  i^i  m )  =/=  (/)  /\  y  e.  ( A  \  m
) )  /\  n  e.  ( A  i^i  m
) )  ->  -.  y  e.  m )
88 inss2 3564 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( A  i^i  m )  C_  m
89 simpr 449 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( A  i^i  m )  =/=  (/)  /\  y  e.  ( A  \  m
) )  /\  n  e.  ( A  i^i  m
) )  ->  n  e.  ( A  i^i  m
) )
9088, 89sseldi 3348 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( A  i^i  m )  =/=  (/)  /\  y  e.  ( A  \  m
) )  /\  n  e.  ( A  i^i  m
) )  ->  n  e.  m )
91 eleq1 2498 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  =  n  ->  (
y  e.  m  <->  n  e.  m ) )
9290, 91syl5ibrcom 215 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( A  i^i  m )  =/=  (/)  /\  y  e.  ( A  \  m
) )  /\  n  e.  ( A  i^i  m
) )  ->  (
y  =  n  -> 
y  e.  m ) )
9387, 92mtod 171 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( A  i^i  m )  =/=  (/)  /\  y  e.  ( A  \  m
) )  /\  n  e.  ( A  i^i  m
) )  ->  -.  y  =  n )
9493, 62syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( A  i^i  m )  =/=  (/)  /\  y  e.  ( A  \  m
) )  /\  n  e.  ( A  i^i  m
) )  ->  if ( y  =  n ,  ( h `  n ) ,  U. ( F `  y ) )  =  U. ( F `  y )
)
9594iineq2dv 4117 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( A  i^i  m
)  =/=  (/)  /\  y  e.  ( A  \  m
) )  ->  |^|_ n  e.  ( A  i^i  m
) if ( y  =  n ,  ( h `  n ) ,  U. ( F `
 y ) )  =  |^|_ n  e.  ( A  i^i  m ) U. ( F `  y ) )
96 iinconst 4104 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( A  i^i  m )  =/=  (/)  ->  |^|_ n  e.  ( A  i^i  m
) U. ( F `
 y )  = 
U. ( F `  y ) )
9796adantr 453 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( A  i^i  m
)  =/=  (/)  /\  y  e.  ( A  \  m
) )  ->  |^|_ n  e.  ( A  i^i  m
) U. ( F `
 y )  = 
U. ( F `  y ) )
9895, 97eqtr2d 2471 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( A  i^i  m
)  =/=  (/)  /\  y  e.  ( A  \  m
) )  ->  U. ( F `  y )  =  |^|_ n  e.  ( A  i^i  m ) if ( y  =  n ,  ( h `
 n ) , 
U. ( F `  y ) ) )
99 eqeq1 2444 . . . . . . . . . . . . . . . . . . 19  |-  ( ( h `  y )  =  U. ( F `
 y )  -> 
( ( h `  y )  =  |^|_ n  e.  ( A  i^i  m ) if ( y  =  n ,  ( h `  n
) ,  U. ( F `  y )
)  <->  U. ( F `  y )  =  |^|_ n  e.  ( A  i^i  m ) if ( y  =  n ,  ( h `  n
) ,  U. ( F `  y )
) ) )
10098, 99syl5ibrcom 215 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( A  i^i  m
)  =/=  (/)  /\  y  e.  ( A  \  m
) )  ->  (
( h `  y
)  =  U. ( F `  y )  ->  ( h `  y
)  =  |^|_ n  e.  ( A  i^i  m
) if ( y  =  n ,  ( h `  n ) ,  U. ( F `
 y ) ) ) )
101100ralimdva 2786 . . . . . . . . . . . . . . . . 17  |-  ( ( A  i^i  m )  =/=  (/)  ->  ( A. y  e.  ( A  \  m ) ( h `
 y )  = 
U. ( F `  y )  ->  A. y  e.  ( A  \  m
) ( h `  y )  =  |^|_ n  e.  ( A  i^i  m ) if ( y  =  n ,  ( h `  n
) ,  U. ( F `  y )
) ) )
1024, 101mpan9 457 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( A  e.  V  /\  F : A --> Top )  /\  (
h  Fn  A  /\  A. y  e.  A  ( h `  y )  e.  ( F `  y ) ) )  /\  ( m  e. 
Fin  /\  A. y  e.  ( A  \  m
) ( h `  y )  =  U. ( F `  y ) ) )  /\  ( A  i^i  m )  =/=  (/) )  ->  A. y  e.  ( A  \  m
) ( h `  y )  =  |^|_ n  e.  ( A  i^i  m ) if ( y  =  n ,  ( h `  n
) ,  U. ( F `  y )
) )
103 inundif 3708 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  i^i  m )  u.  ( A  \  m ) )  =  A
104103raleqi 2910 . . . . . . . . . . . . . . . . 17  |-  ( A. y  e.  ( ( A  i^i  m )  u.  ( A  \  m
) ) ( h `
 y )  = 
|^|_ n  e.  ( A  i^i  m ) if ( y  =  n ,  ( h `  n ) ,  U. ( F `  y ) )  <->  A. y  e.  A  ( h `  y
)  =  |^|_ n  e.  ( A  i^i  m
) if ( y  =  n ,  ( h `  n ) ,  U. ( F `
 y ) ) )
105 ralunb 3530 . . . . . . . . . . . . . . . . 17  |-  ( A. y  e.  ( ( A  i^i  m )  u.  ( A  \  m
) ) ( h `
 y )  = 
|^|_ n  e.  ( A  i^i  m ) if ( y  =  n ,  ( h `  n ) ,  U. ( F `  y ) )  <->  ( A. y  e.  ( A  i^i  m
) ( h `  y )  =  |^|_ n  e.  ( A  i^i  m ) if ( y  =  n ,  ( h `  n
) ,  U. ( F `  y )
)  /\  A. y  e.  ( A  \  m
) ( h `  y )  =  |^|_ n  e.  ( A  i^i  m ) if ( y  =  n ,  ( h `  n
) ,  U. ( F `  y )
) ) )
106104, 105bitr3i 244 . . . . . . . . . . . . . . . 16  |-  ( A. y  e.  A  (
h `  y )  =  |^|_ n  e.  ( A  i^i  m ) if ( y  =  n ,  ( h `
 n ) , 
U. ( F `  y ) )  <->  ( A. y  e.  ( A  i^i  m ) ( h `
 y )  = 
|^|_ n  e.  ( A  i^i  m ) if ( y  =  n ,  ( h `  n ) ,  U. ( F `  y ) )  /\  A. y  e.  ( A  \  m
) ( h `  y )  =  |^|_ n  e.  ( A  i^i  m ) if ( y  =  n ,  ( h `  n
) ,  U. ( F `  y )
) ) )
10785, 102, 106sylanbrc 647 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( A  e.  V  /\  F : A --> Top )  /\  (
h  Fn  A  /\  A. y  e.  A  ( h `  y )  e.  ( F `  y ) ) )  /\  ( m  e. 
Fin  /\  A. y  e.  ( A  \  m
) ( h `  y )  =  U. ( F `  y ) ) )  /\  ( A  i^i  m )  =/=  (/) )  ->  A. y  e.  A  ( h `  y )  =  |^|_ n  e.  ( A  i^i  m ) if ( y  =  n ,  ( h `  n
) ,  U. ( F `  y )
) )
108 ixpeq2 7078 . . . . . . . . . . . . . . 15  |-  ( A. y  e.  A  (
h `  y )  =  |^|_ n  e.  ( A  i^i  m ) if ( y  =  n ,  ( h `
 n ) , 
U. ( F `  y ) )  ->  X_ y  e.  A  ( h `  y )  =  X_ y  e.  A  |^|_
n  e.  ( A  i^i  m ) if ( y  =  n ,  ( h `  n ) ,  U. ( F `  y ) ) )
109107, 108syl 16 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( A  e.  V  /\  F : A --> Top )  /\  (
h  Fn  A  /\  A. y  e.  A  ( h `  y )  e.  ( F `  y ) ) )  /\  ( m  e. 
Fin  /\  A. y  e.  ( A  \  m
) ( h `  y )  =  U. ( F `  y ) ) )  /\  ( A  i^i  m )  =/=  (/) )  ->  X_ y  e.  A  ( h `  y )  =  X_ y  e.  A  |^|_ n  e.  ( A  i^i  m
) if ( y  =  n ,  ( h `  n ) ,  U. ( F `
 y ) ) )
110 ixpiin 7090 . . . . . . . . . . . . . . 15  |-  ( ( A  i^i  m )  =/=  (/)  ->  X_ y  e.  A  |^|_ n  e.  ( A  i^i  m ) if ( y  =  n ,  ( h `
 n ) , 
U. ( F `  y ) )  = 
|^|_ n  e.  ( A  i^i  m ) X_ y  e.  A  if ( y  =  n ,  ( h `  n ) ,  U. ( F `  y ) ) )
111110adantl 454 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( A  e.  V  /\  F : A --> Top )  /\  (
h  Fn  A  /\  A. y  e.  A  ( h `  y )  e.  ( F `  y ) ) )  /\  ( m  e. 
Fin  /\  A. y  e.  ( A  \  m
) ( h `  y )  =  U. ( F `  y ) ) )  /\  ( A  i^i  m )  =/=  (/) )  ->  X_ y  e.  A  |^|_ n  e.  ( A  i^i  m
) if ( y  =  n ,  ( h `  n ) ,  U. ( F `
 y ) )  =  |^|_ n  e.  ( A  i^i  m )
X_ y  e.  A  if ( y  =  n ,  ( h `  n ) ,  U. ( F `  y ) ) )
112109, 111eqtrd 2470 . . . . . . . . . . . . 13  |-  ( ( ( ( ( A  e.  V  /\  F : A --> Top )  /\  (
h  Fn  A  /\  A. y  e.  A  ( h `  y )  e.  ( F `  y ) ) )  /\  ( m  e. 
Fin  /\  A. y  e.  ( A  \  m
) ( h `  y )  =  U. ( F `  y ) ) )  /\  ( A  i^i  m )  =/=  (/) )  ->  X_ y  e.  A  ( h `  y )  =  |^|_ n  e.  ( A  i^i  m ) X_ y  e.  A  if (
y  =  n ,  ( h `  n
) ,  U. ( F `  y )
) )
11343, 57, 1123eqtr4rd 2481 . . . . . . . . . . . 12  |-  ( ( ( ( ( A  e.  V  /\  F : A --> Top )  /\  (
h  Fn  A  /\  A. y  e.  A  ( h `  y )  e.  ( F `  y ) ) )  /\  ( m  e. 
Fin  /\  A. y  e.  ( A  \  m
) ( h `  y )  =  U. ( F `  y ) ) )  /\  ( A  i^i  m )  =/=  (/) )  ->  X_ y  e.  A  ( h `  y )  =  ( X  i^i  |^|_ n  e.  ( A  i^i  m
) ( `' ( w  e.  X  |->  ( w `  n ) ) " ( h `
 n ) ) ) )
11428, 113pm2.61dane 2684 . . . . . . . . . . 11  |-  ( ( ( ( A  e.  V  /\  F : A
--> Top )  /\  (
h  Fn  A  /\  A. y  e.  A  ( h `  y )  e.  ( F `  y ) ) )  /\  ( m  e. 
Fin  /\  A. y  e.  ( A  \  m
) ( h `  y )  =  U. ( F `  y ) ) )  ->  X_ y  e.  A  ( h `  y )  =  ( X  i^i  |^|_ n  e.  ( A  i^i  m
) ( `' ( w  e.  X  |->  ( w `  n ) ) " ( h `
 n ) ) ) )
115 ixpexg 7088 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( A. n  e.  A  U. ( F `  n )  e.  _V  ->  X_ n  e.  A  U. ( F `  n )  e.  _V )
116 fvex 5744 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( F `
 n )  e. 
_V
117116uniex 4707 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  U. ( F `  n )  e.  _V
118117a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( n  e.  A  ->  U. ( F `  n )  e.  _V )
119115, 118mprg 2777 . . . . . . . . . . . . . . . . . . . . . . 23  |-  X_ n  e.  A  U. ( F `  n )  e.  _V
12013, 119eqeltri 2508 . . . . . . . . . . . . . . . . . . . . . 22  |-  X  e. 
_V
121120mptex 5968 . . . . . . . . . . . . . . . . . . . . 21  |-  ( w  e.  X  |->  ( w `
 n ) )  e.  _V
122121cnvex 5408 . . . . . . . . . . . . . . . . . . . 20  |-  `' ( w  e.  X  |->  ( w `  n ) )  e.  _V
123 imaexg 5219 . . . . . . . . . . . . . . . . . . . 20  |-  ( `' ( w  e.  X  |->  ( w `  n
) )  e.  _V  ->  ( `' ( w  e.  X  |->  ( w `
 n ) )
" ( h `  n ) )  e. 
_V )
124122, 123ax-mp 8 . . . . . . . . . . . . . . . . . . 19  |-  ( `' ( w  e.  X  |->  ( w `  n
) ) " (
h `  n )
)  e.  _V
125124dfiin2 4128 . . . . . . . . . . . . . . . . . 18  |-  |^|_ n  e.  ( A  i^i  m
) ( `' ( w  e.  X  |->  ( w `  n ) ) " ( h `
 n ) )  =  |^| { z  |  E. n  e.  ( A  i^i  m
) z  =  ( `' ( w  e.  X  |->  ( w `  n ) ) "
( h `  n
) ) }
126 inteq 4055 . . . . . . . . . . . . . . . . . 18  |-  ( { z  |  E. n  e.  ( A  i^i  m
) z  =  ( `' ( w  e.  X  |->  ( w `  n ) ) "
( h `  n
) ) }  =  (/) 
->  |^| { z  |  E. n  e.  ( A  i^i  m ) z  =  ( `' ( w  e.  X  |->  ( w `  n
) ) " (
h `  n )
) }  =  |^| (/) )
127125, 126syl5eq 2482 . . . . . . . . . . . . . . . . 17  |-  ( { z  |  E. n  e.  ( A  i^i  m
) z  =  ( `' ( w  e.  X  |->  ( w `  n ) ) "
( h `  n
) ) }  =  (/) 
->  |^|_ n  e.  ( A  i^i  m ) ( `' ( w  e.  X  |->  ( w `
 n ) )
" ( h `  n ) )  = 
|^| (/) )
128 int0 4066 . . . . . . . . . . . . . . . . 17  |-  |^| (/)  =  _V
129127, 128syl6eq 2486 . . . . . . . . . . . . . . . 16  |-  ( { z  |  E. n  e.  ( A  i^i  m
) z  =  ( `' ( w  e.  X  |->  ( w `  n ) ) "
( h `  n
) ) }  =  (/) 
->  |^|_ n  e.  ( A  i^i  m ) ( `' ( w  e.  X  |->  ( w `
 n ) )
" ( h `  n ) )  =  _V )
130129ineq2d 3544 . . . . . . . . . . . . . . 15  |-  ( { z  |  E. n  e.  ( A  i^i  m
) z  =  ( `' ( w  e.  X  |->  ( w `  n ) ) "
( h `  n
) ) }  =  (/) 
->  ( X  i^i  |^|_ n  e.  ( A  i^i  m ) ( `' ( w  e.  X  |->  ( w `  n
) ) " (
h `  n )
) )  =  ( X  i^i  _V )
)
131 inv1 3656 . . . . . . . . . . . . . . 15  |-  ( X  i^i  _V )  =  X
132130, 131syl6eq 2486 . . . . . . . . . . . . . 14  |-  ( { z  |  E. n  e.  ( A  i^i  m
) z  =  ( `' ( w  e.  X  |->  ( w `  n ) ) "
( h `  n
) ) }  =  (/) 
->  ( X  i^i  |^|_ n  e.  ( A  i^i  m ) ( `' ( w  e.  X  |->  ( w `  n
) ) " (
h `  n )
) )  =  X )
133132adantl 454 . . . . . . . . . . . . 13  |-  ( ( ( ( ( A  e.  V  /\  F : A --> Top )  /\  (
h  Fn  A  /\  A. y  e.  A  ( h `  y )  e.  ( F `  y ) ) )  /\  ( m  e. 
Fin  /\  A. y  e.  ( A  \  m
) ( h `  y )  =  U. ( F `  y ) ) )  /\  {
z  |  E. n  e.  ( A  i^i  m
) z  =  ( `' ( w  e.  X  |->  ( w `  n ) ) "
( h `  n
) ) }  =  (/) )  ->  ( X  i^i  |^|_ n  e.  ( A  i^i  m ) ( `' ( w  e.  X  |->  ( w `
 n ) )
" ( h `  n ) ) )  =  X )
134 snex 4407 . . . . . . . . . . . . . . . . . 18  |-  { X }  e.  _V
1351ptbas 17613 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A  e.  V  /\  F : A --> Top )  ->  B  e.  TopBases )
1361, 13ptpjpre2 17614 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( A  e.  V  /\  F : A --> Top )  /\  ( k  e.  A  /\  u  e.  ( F `  k )
) )  ->  ( `' ( w  e.  X  |->  ( w `  k ) ) "
u )  e.  B
)
137136ralrimivva 2800 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( A  e.  V  /\  F : A --> Top )  ->  A. k  e.  A  A. u  e.  ( F `  k )
( `' ( w  e.  X  |->  ( w `
 k ) )
" u )  e.  B )
138 eqid 2438 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( k  e.  A ,  u  e.  ( F `  k
)  |->  ( `' ( w  e.  X  |->  ( w `  k ) ) " u ) )  =  ( k  e.  A ,  u  e.  ( F `  k
)  |->  ( `' ( w  e.  X  |->  ( w `  k ) ) " u ) )
139138fmpt2x 6419 . . . . . . . . . . . . . . . . . . . . 21  |-  ( A. k  e.  A  A. u  e.  ( F `  k ) ( `' ( w  e.  X  |->  ( w `  k
) ) " u
)  e.  B  <->  ( k  e.  A ,  u  e.  ( F `  k
)  |->  ( `' ( w  e.  X  |->  ( w `  k ) ) " u ) ) : U_ k  e.  A  ( {
k }  X.  ( F `  k )
) --> B )
140137, 139sylib 190 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( A  e.  V  /\  F : A --> Top )  ->  ( k  e.  A ,  u  e.  ( F `  k )  |->  ( `' ( w  e.  X  |->  ( w `
 k ) )
" u ) ) : U_ k  e.  A  ( { k }  X.  ( F `
 k ) ) --> B )
141 frn 5599 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( k  e.  A ,  u  e.  ( F `  k )  |->  ( `' ( w  e.  X  |->  ( w `  k
) ) " u
) ) : U_ k  e.  A  ( { k }  X.  ( F `  k ) ) --> B  ->  ran  ( k  e.  A ,  u  e.  ( F `  k )  |->  ( `' ( w  e.  X  |->  ( w `
 k ) )
" u ) ) 
C_  B )
142140, 141syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A  e.  V  /\  F : A --> Top )  ->  ran  ( k  e.  A ,  u  e.  ( F `  k
)  |->  ( `' ( w  e.  X  |->  ( w `  k ) ) " u ) )  C_  B )
143135, 142ssexd 4352 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  e.  V  /\  F : A --> Top )  ->  ran  ( k  e.  A ,  u  e.  ( F `  k
)  |->  ( `' ( w  e.  X  |->  ( w `  k ) ) " u ) )  e.  _V )
144 unexg 4712 . . . . . . . . . . . . . . . . . 18  |-  ( ( { X }  e.  _V  /\  ran  ( k  e.  A ,  u  e.  ( F `  k
)  |->  ( `' ( w  e.  X  |->  ( w `  k ) ) " u ) )  e.  _V )  ->  ( { X }  u.  ran  ( k  e.  A ,  u  e.  ( F `  k
)  |->  ( `' ( w  e.  X  |->  ( w `  k ) ) " u ) ) )  e.  _V )
145134, 143, 144sylancr 646 . . . . . . . . . . . . . . . . 17  |-  ( ( A  e.  V  /\  F : A --> Top )  ->  ( { X }  u.  ran  ( k  e.  A ,  u  e.  ( F `  k
)  |->  ( `' ( w  e.  X  |->  ( w `  k ) ) " u ) ) )  e.  _V )
146 ssfii 7426 . . . . . . . . . . . . . . . . 17  |-  ( ( { X }  u.  ran  ( k  e.  A ,  u  e.  ( F `  k )  |->  ( `' ( w  e.  X  |->  ( w `
 k ) )
" u ) ) )  e.  _V  ->  ( { X }  u.  ran  ( k  e.  A ,  u  e.  ( F `  k )  |->  ( `' ( w  e.  X  |->  ( w `
 k ) )
" u ) ) )  C_  ( fi `  ( { X }  u.  ran  ( k  e.  A ,  u  e.  ( F `  k
)  |->  ( `' ( w  e.  X  |->  ( w `  k ) ) " u ) ) ) ) )
147145, 146syl 16 . . . . . . . . . . . . . . . 16  |-  ( ( A  e.  V  /\  F : A --> Top )  ->  ( { X }  u.  ran  ( k  e.  A ,  u  e.  ( F `  k
)  |->  ( `' ( w  e.  X  |->  ( w `  k ) ) " u ) ) )  C_  ( fi `  ( { X }  u.  ran  ( k  e.  A ,  u  e.  ( F `  k
)  |->  ( `' ( w  e.  X  |->  ( w `  k ) ) " u ) ) ) ) )
148147ad2antrr 708 . . . . . . . . . . . . . . 15  |-  ( ( ( ( A  e.  V  /\  F : A
--> Top )  /\  (
h  Fn  A  /\  A. y  e.  A  ( h `  y )  e.  ( F `  y ) ) )  /\  ( m  e. 
Fin  /\  A. y  e.  ( A  \  m
) ( h `  y )  =  U. ( F `  y ) ) )  ->  ( { X }  u.  ran  ( k  e.  A ,  u  e.  ( F `  k )  |->  ( `' ( w  e.  X  |->  ( w `
 k ) )
" u ) ) )  C_  ( fi `  ( { X }  u.  ran  ( k  e.  A ,  u  e.  ( F `  k
)  |->  ( `' ( w  e.  X  |->  ( w `  k ) ) " u ) ) ) ) )
149 ssun1 3512 . . . . . . . . . . . . . . . . 17  |-  { X }  C_  ( { X }  u.  ran  ( k  e.  A ,  u  e.  ( F `  k
)  |->  ( `' ( w  e.  X  |->  ( w `  k ) ) " u ) ) )
150120snss 3928 . . . . . . . . . . . . . . . . 17  |-  ( X  e.  ( { X }  u.  ran  ( k  e.  A ,  u  e.  ( F `  k
)  |->  ( `' ( w  e.  X  |->  ( w `  k ) ) " u ) ) )  <->  { X }  C_  ( { X }  u.  ran  ( k  e.  A ,  u  e.  ( F `  k
)  |->  ( `' ( w  e.  X  |->  ( w `  k ) ) " u ) ) ) )
151149, 150mpbir 202 . . . . . . . . . . . . . . . 16  |-  X  e.  ( { X }  u.  ran  ( k  e.  A ,  u  e.  ( F `  k
)  |->  ( `' ( w  e.  X  |->  ( w `  k ) ) " u ) ) )
152151a1i 11 . . . . . . . . . . . . . . 15  |-  ( ( ( ( A  e.  V  /\  F : A
--> Top )  /\  (
h  Fn  A  /\  A. y  e.  A  ( h `  y )  e.  ( F `  y ) ) )  /\  ( m  e. 
Fin  /\  A. y  e.  ( A  \  m
) ( h `  y )  =  U. ( F `  y ) ) )  ->  X  e.  ( { X }  u.  ran  ( k  e.  A ,  u  e.  ( F `  k
)  |->  ( `' ( w  e.  X  |->  ( w `  k ) ) " u ) ) ) )
153148, 152sseldd 3351 . . . . . . . . . . . . . 14  |-  ( ( ( ( A  e.  V  /\  F : A
--> Top )  /\  (
h  Fn  A  /\  A. y  e.  A  ( h `  y )  e.  ( F `  y ) ) )  /\  ( m  e. 
Fin  /\  A. y  e.  ( A  \  m
) ( h `  y )  =  U. ( F `  y ) ) )  ->  X  e.  ( fi `  ( { X }  u.  ran  ( k  e.  A ,  u  e.  ( F `  k )  |->  ( `' ( w  e.  X  |->  ( w `
 k ) )
" u ) ) ) ) )
154153adantr 453 . . . . . . . . . . . . 13  |-  ( ( ( ( ( A  e.  V  /\  F : A --> Top )  /\  (
h  Fn  A  /\  A. y  e.  A  ( h `  y )  e.  ( F `  y ) ) )  /\  ( m  e. 
Fin  /\  A. y  e.  ( A  \  m
) ( h `  y )  =  U. ( F `  y ) ) )  /\  {
z  |  E. n  e.  ( A  i^i  m
) z  =  ( `' ( w  e.  X  |->  ( w `  n ) ) "
( h `  n
) ) }  =  (/) )  ->  X  e.  ( fi `  ( { X }  u.  ran  ( k  e.  A ,  u  e.  ( F `  k )  |->  ( `' ( w  e.  X  |->  ( w `
 k ) )
" u ) ) ) ) )
155133, 154eqeltrd 2512 . . . . . . . . . . . 12  |-  ( ( ( ( ( A  e.  V  /\  F : A --> Top )  /\  (
h  Fn  A  /\  A. y  e.  A  ( h `  y )  e.  ( F `  y ) ) )  /\  ( m  e. 
Fin  /\  A. y  e.  ( A  \  m
) ( h `  y )  =  U. ( F `  y ) ) )  /\  {
z  |  E. n  e.  ( A  i^i  m
) z  =  ( `' ( w  e.  X  |->  ( w `  n ) ) "
( h `  n
) ) }  =  (/) )  ->  ( X  i^i  |^|_ n  e.  ( A  i^i  m ) ( `' ( w  e.  X  |->  ( w `
 n ) )
" ( h `  n ) ) )  e.  ( fi `  ( { X }  u.  ran  ( k  e.  A ,  u  e.  ( F `  k )  |->  ( `' ( w  e.  X  |->  ( w `
 k ) )
" u ) ) ) ) )
156145ad3antrrr 712 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( A  e.  V  /\  F : A --> Top )  /\  (
h  Fn  A  /\  A. y  e.  A  ( h `  y )  e.  ( F `  y ) ) )  /\  ( m  e. 
Fin  /\  A. y  e.  ( A  \  m
) ( h `  y )  =  U. ( F `  y ) ) )  /\  {
z  |  E. n  e.  ( A  i^i  m
) z  =  ( `' ( w  e.  X  |->  ( w `  n ) ) "
( h `  n
) ) }  =/=  (/) )  ->  ( { X }  u.  ran  ( k  e.  A ,  u  e.  ( F `  k )  |->  ( `' ( w  e.  X  |->  ( w `
 k ) )
" u ) ) )  e.  _V )
157 nfv 1630 . . . . . . . . . . . . . . . . . . . . . 22  |-  F/ n
( ( ( A  e.  V  /\  F : A --> Top )  /\  (
h  Fn  A  /\  A. y  e.  A  ( h `  y )  e.  ( F `  y ) ) )  /\  ( m  e. 
Fin  /\  A. y  e.  ( A  \  m
) ( h `  y )  =  U. ( F `  y ) ) )
158 nfcv 2574 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  F/_ n A
159 nfcv 2574 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  F/_ n
( F `  k
)
160 nfixp1 7084 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  F/_ n X_ n  e.  A  U. ( F `  n )
16113, 160nfcxfr 2571 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  F/_ n X
162 nfcv 2574 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  F/_ n
( w `  k
)
163161, 162nfmpt 4299 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  F/_ n
( w  e.  X  |->  ( w `  k
) )
164163nfcnv 5053 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  F/_ n `' ( w  e.  X  |->  ( w `  k ) )
165 nfcv 2574 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  F/_ n u
166164, 165nfima 5213 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  F/_ n
( `' ( w  e.  X  |->  ( w `
 k ) )
" u )
167158, 159, 166nfmpt2 6144 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  F/_ n
( k  e.  A ,  u  e.  ( F `  k )  |->  ( `' ( w  e.  X  |->  ( w `
 k ) )
" u ) )
168167nfrn 5114 . . . . . . . . . . . . . . . . . . . . . . 23  |-  F/_ n ran  ( k  e.  A ,  u  e.  ( F `  k )  |->  ( `' ( w  e.  X  |->  ( w `
 k ) )
" u ) )
169168nfcri 2568 . . . . . . . . . . . . . . . . . . . . . 22  |-  F/ n  z  e.  ran  ( k  e.  A ,  u  e.  ( F `  k
)  |->  ( `' ( w  e.  X  |->  ( w `  k ) ) " u ) )
170 df-ov 6086 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( n ( k  e.  A ,  u  e.  ( F `  k )  |->  ( `' ( w  e.  X  |->  ( w `
 k ) )
" u ) ) ( h `  n
) )  =  ( ( k  e.  A ,  u  e.  ( F `  k )  |->  ( `' ( w  e.  X  |->  ( w `
 k ) )
" u ) ) `
 <. n ,  ( h `  n )
>. )
171124a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( A  e.  V  /\  F : A --> Top )  /\  (
h  Fn  A  /\  A. y  e.  A  ( h `  y )  e.  ( F `  y ) ) )  /\  ( m  e. 
Fin  /\  A. y  e.  ( A  \  m
) ( h `  y )  =  U. ( F `  y ) ) )  /\  n  e.  ( A  i^i  m
) )  ->  ( `' ( w  e.  X  |->  ( w `  n ) ) "
( h `  n
) )  e.  _V )
172 fveq2 5730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( k  =  n  ->  (
w `  k )  =  ( w `  n ) )
173172mpteq2dv 4298 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( k  =  n  ->  (
w  e.  X  |->  ( w `  k ) )  =  ( w  e.  X  |->  ( w `
 n ) ) )
174173cnveqd 5050 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( k  =  n  ->  `' ( w  e.  X  |->  ( w `  k
) )  =  `' ( w  e.  X  |->  ( w `  n
) ) )
175174imaeq1d 5204 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( k  =  n  ->  ( `' ( w  e.  X  |->  ( w `  k ) ) "
u )  =  ( `' ( w  e.  X  |->  ( w `  n ) ) "
u ) )
176 imaeq2 5201 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( u  =  ( h `  n )  ->  ( `' ( w  e.  X  |->  ( w `  n ) ) "
u )  =  ( `' ( w  e.  X  |->  ( w `  n ) ) "
( h `  n
) ) )
177175, 176sylan9eq 2490 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( k  =  n  /\  u  =  ( h `  n ) )  -> 
( `' ( w  e.  X  |->  ( w `
 k ) )
" u )  =  ( `' ( w  e.  X  |->  ( w `
 n ) )
" ( h `  n ) ) )
178 fveq2 5730 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( k  =  n  ->  ( F `  k )  =  ( F `  n ) )
179177, 178, 138ovmpt2x 6204 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( n  e.  A  /\  ( h `  n
)  e.  ( F `
 n )  /\  ( `' ( w  e.  X  |->  ( w `  n ) ) "
( h `  n
) )  e.  _V )  ->  ( n ( k  e.  A ,  u  e.  ( F `  k )  |->  ( `' ( w  e.  X  |->  ( w `  k
) ) " u
) ) ( h `
 n ) )  =  ( `' ( w  e.  X  |->  ( w `  n ) ) " ( h `
 n ) ) )
18032, 39, 171, 179syl3anc 1185 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( A  e.  V  /\  F : A --> Top )  /\  (
h  Fn  A  /\  A. y  e.  A  ( h `  y )  e.  ( F `  y ) ) )  /\  ( m  e. 
Fin  /\  A. y  e.  ( A  \  m
) ( h `  y )  =  U. ( F `  y ) ) )  /\  n  e.  ( A  i^i  m
) )  ->  (
n ( k  e.  A ,  u  e.  ( F `  k
)  |->  ( `' ( w  e.  X  |->  ( w `  k ) ) " u ) ) ( h `  n ) )  =  ( `' ( w  e.  X  |->  ( w `
 n ) )
" ( h `  n ) ) )
181170, 180syl5eqr 2484 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( A  e.  V  /\  F : A --> Top )  /\  (
h  Fn  A  /\  A. y  e.  A  ( h `  y )  e.  ( F `  y ) ) )  /\  ( m  e. 
Fin  /\  A. y  e.  ( A  \  m
) ( h `  y )  =  U. ( F `  y ) ) )  /\  n  e.  ( A  i^i  m
) )  ->  (
( k  e.  A ,  u  e.  ( F `  k )  |->  ( `' ( w  e.  X  |->  ( w `
 k ) )
" u ) ) `
 <. n ,  ( h `  n )
>. )  =  ( `' ( w  e.  X  |->  ( w `  n ) ) "
( h `  n
) ) )
182140ad3antrrr 712 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( A  e.  V  /\  F : A --> Top )  /\  (
h  Fn  A  /\  A. y  e.  A  ( h `  y )  e.  ( F `  y ) ) )  /\  ( m  e. 
Fin  /\  A. y  e.  ( A  \  m
) ( h `  y )  =  U. ( F `  y ) ) )  /\  n  e.  ( A  i^i  m
) )  ->  (
k  e.  A ,  u  e.  ( F `  k )  |->  ( `' ( w  e.  X  |->  ( w `  k
) ) " u
) ) : U_ k  e.  A  ( { k }  X.  ( F `  k ) ) --> B )
183 ffn 5593 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( k  e.  A ,  u  e.  ( F `  k )  |->  ( `' ( w  e.  X  |->  ( w `  k
) ) " u
) ) : U_ k  e.  A  ( { k }  X.  ( F `  k ) ) --> B  ->  (
k  e.  A ,  u  e.  ( F `  k )  |->  ( `' ( w  e.  X  |->  ( w `  k
) ) " u
) )  Fn  U_ k  e.  A  ( { k }  X.  ( F `  k ) ) )
184182, 183syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( A  e.  V  /\  F : A --> Top )  /\  (
h  Fn  A  /\  A. y  e.  A  ( h `  y )  e.  ( F `  y ) ) )  /\  ( m  e. 
Fin  /\  A. y  e.  ( A  \  m
) ( h `  y )  =  U. ( F `  y ) ) )  /\  n  e.  ( A  i^i  m
) )  ->  (
k  e.  A ,  u  e.  ( F `  k )  |->  ( `' ( w  e.  X  |->  ( w `  k
) ) " u
) )  Fn  U_ k  e.  A  ( { k }  X.  ( F `  k ) ) )
185 opeliunxp 4931 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( <.
n ,  ( h `
 n ) >.  e.  U_ n  e.  A  ( { n }  X.  ( F `  n ) )  <->  ( n  e.  A  /\  ( h `
 n )  e.  ( F `  n
) ) )
18632, 39, 185sylanbrc 647 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( A  e.  V  /\  F : A --> Top )  /\  (
h  Fn  A  /\  A. y  e.  A  ( h `  y )  e.  ( F `  y ) ) )  /\  ( m  e. 
Fin  /\  A. y  e.  ( A  \  m
) ( h `  y )  =  U. ( F `  y ) ) )  /\  n  e.  ( A  i^i  m
) )  ->  <. n ,  ( h `  n ) >.  e.  U_ n  e.  A  ( { n }  X.  ( F `  n ) ) )
187 sneq 3827 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( n  =  k  ->  { n }  =  { k } )
188 fveq2 5730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( n  =  k  ->  ( F `  n )  =  ( F `  k ) )
189187, 188xpeq12d 4905 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( n  =  k  ->  ( { n }  X.  ( F `  n ) )  =  ( { k }  X.  ( F `  k )
) )
190189cbviunv 4132 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  U_ n  e.  A  ( {
n }  X.  ( F `  n )
)  =  U_ k  e.  A  ( {
k }  X.  ( F `  k )
)
191186, 190syl6eleq 2528 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( A  e.  V  /\  F : A --> Top )  /\  (
h  Fn  A  /\  A. y  e.  A  ( h `  y )  e.  ( F `  y ) ) )  /\  ( m  e. 
Fin  /\  A. y  e.  ( A  \  m
) ( h `  y )  =  U. ( F `  y ) ) )  /\  n  e.  ( A  i^i  m
) )  ->  <. n ,  ( h `  n ) >.  e.  U_ k  e.  A  ( { k }  X.  ( F `  k ) ) )
192 fnfvelrn 5869 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( k  e.  A ,  u  e.  ( F `  k )  |->  ( `' ( w  e.  X  |->  ( w `
 k ) )
" u ) )  Fn  U_ k  e.  A  ( { k }  X.  ( F `
 k ) )  /\  <. n ,  ( h `  n )
>.  e.  U_ k  e.  A  ( { k }  X.  ( F `
 k ) ) )  ->  ( (
k  e.  A ,  u  e.  ( F `  k )  |->  ( `' ( w  e.  X  |->  ( w `  k
) ) " u
) ) `  <. n ,  ( h `  n ) >. )  e.  ran  ( k  e.  A ,  u  e.  ( F `  k
)  |->  ( `' ( w  e.  X  |->  ( w `  k ) ) " u ) ) )
193184, 191, 192syl2anc 644 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( A  e.  V  /\  F : A --> Top )  /\  (
h  Fn  A  /\  A. y  e.  A  ( h `  y )  e.  ( F `  y ) ) )  /\  ( m  e. 
Fin  /\  A. y  e.  ( A  \  m
) ( h `  y )  =  U. ( F `  y ) ) )  /\  n  e.  ( A  i^i  m
) )  ->  (
( k  e.  A ,  u  e.  ( F `  k )  |->  ( `' ( w  e.  X  |->  ( w `
 k ) )
" u ) ) `
 <. n ,  ( h `  n )
>. )  e.  ran  ( k  e.  A ,  u  e.  ( F `  k )  |->  ( `' ( w  e.  X  |->  ( w `
 k ) )
" u ) ) )
194181, 193eqeltrrd 2513 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( A  e.  V  /\  F : A --> Top )  /\  (
h  Fn  A  /\  A. y  e.  A  ( h `  y )  e.  ( F `  y ) ) )  /\  ( m  e. 
Fin  /\  A. y  e.  ( A  \  m
) ( h `  y )  =  U. ( F `  y ) ) )  /\  n  e.  ( A  i^i  m
) )  ->  ( `' ( w  e.  X  |->  ( w `  n ) ) "
( h `  n
) )  e.  ran  ( k  e.  A ,  u  e.  ( F `  k )  |->  ( `' ( w  e.  X  |->  ( w `
 k ) )
" u ) ) )
195 eleq1 2498 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( z  =  ( `' ( w  e.  X  |->  ( w `  n ) ) " ( h `
 n ) )  ->  ( z  e. 
ran  ( k  e.  A ,  u  e.  ( F `  k
)  |->  ( `' ( w  e.  X  |->  ( w `  k ) ) " u ) )  <->  ( `' ( w  e.  X  |->  ( w `  n ) ) " ( h `
 n ) )  e.  ran  ( k  e.  A ,  u  e.  ( F `  k
)  |->  ( `' ( w  e.  X  |->  ( w `  k ) ) " u ) ) ) )
196194, 195syl5ibrcom 215 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( A  e.  V  /\  F : A --> Top )  /\  (
h  Fn  A  /\  A. y  e.  A  ( h `  y )  e.  ( F `  y ) ) )  /\  ( m  e. 
Fin  /\  A. y  e.  ( A  \  m
) ( h `  y )  =  U. ( F `  y ) ) )  /\  n  e.  ( A  i^i  m
) )  ->  (
z  =  ( `' ( w  e.  X  |->  ( w `  n
) ) " (
h `  n )
)  ->  z  e.  ran  ( k  e.  A ,  u  e.  ( F `  k )  |->  ( `' ( w  e.  X  |->  ( w `
 k ) )
" u ) ) ) )
197196ex 425 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( A  e.  V  /\  F : A
--> Top )  /\  (
h  Fn  A  /\  A. y  e.  A  ( h `  y )  e.  ( F `  y ) ) )  /\  ( m  e. 
Fin  /\  A. y  e.  ( A  \  m
) ( h `  y )  =  U. ( F `  y ) ) )  ->  (
n  e.  ( A  i^i  m )  -> 
( z  =  ( `' ( w  e.  X  |->  ( w `  n ) ) "
( h `  n
) )  ->  z  e.  ran  ( k  e.  A ,  u  e.  ( F `  k
)  |->  ( `' ( w  e.  X  |->  ( w `  k ) ) " u ) ) ) ) )
198157, 169, 197rexlimd 2829 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( A  e.  V  /\  F : A
--> Top )  /\  (
h  Fn  A  /\  A. y  e.  A  ( h `  y )  e.  ( F `  y ) ) )  /\  ( m  e. 
Fin  /\  A. y  e.  ( A  \  m
) ( h `  y )  =  U. ( F `  y ) ) )  ->  ( E. n  e.  ( A  i^i  m ) z  =  ( `' ( w  e.  X  |->  ( w `  n ) ) " ( h `
 n ) )  ->  z  e.  ran  ( k  e.  A ,  u  e.  ( F `  k )  |->  ( `' ( w  e.  X  |->  ( w `
 k ) )
" u ) ) ) )
199198abssdv 3419 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( A  e.  V  /\  F : A
--> Top )  /\  (
h  Fn  A  /\  A. y  e.  A  ( h `  y )  e.  ( F `  y ) ) )  /\  ( m  e. 
Fin  /\  A. y  e.  ( A  \  m
) ( h `  y )  =  U. ( F `  y ) ) )  ->  { z  |  E. n  e.  ( A  i^i  m
) z  =  ( `' ( w  e.  X  |->  ( w `  n ) ) "
( h `  n
) ) }  C_  ran  ( k  e.  A ,  u  e.  ( F `  k )  |->  ( `' ( w  e.  X  |->  ( w `
 k ) )
" u ) ) )
200 ssun2 3513 . . . . . . . . . . . . . . . . . . . 20  |-  ran  (
k  e.  A ,  u  e.  ( F `  k )  |->  ( `' ( w  e.  X  |->  ( w `  k
) ) " u
) )  C_  ( { X }  u.  ran  ( k  e.  A ,  u  e.  ( F `  k )  |->  ( `' ( w  e.  X  |->  ( w `
 k ) )
" u ) ) )
201199, 200syl6ss 3362 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( A  e.  V  /\  F : A
--> Top )  /\  (
h  Fn  A  /\  A. y  e.  A  ( h `  y )  e.  ( F `  y ) ) )  /\  ( m  e. 
Fin  /\  A. y  e.  ( A  \  m
) ( h `  y )  =  U. ( F `  y ) ) )  ->  { z  |  E. n  e.  ( A  i^i  m
) z  =  ( `' ( w  e.  X  |->  ( w `  n ) ) "
( h `  n
) ) }  C_  ( { X }  u.  ran  ( k  e.  A ,  u  e.  ( F `  k )  |->  ( `' ( w  e.  X  |->  ( w `
 k ) )
" u ) ) ) )
202201adantr 453 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( A  e.  V  /\  F : A --> Top )  /\  (
h  Fn  A  /\  A. y  e.  A  ( h `  y )  e.  ( F `  y ) ) )  /\  ( m  e. 
Fin  /\  A. y  e.  ( A  \  m
) ( h `  y )  =  U. ( F `  y ) ) )  /\  {
z  |  E. n  e.  ( A  i^i  m
) z  =  ( `' ( w  e.  X  |->  ( w `  n ) ) "
( h `  n
) ) }  =/=  (/) )  ->  { z  |  E. n  e.  ( A  i^i  m ) z  =  ( `' ( w  e.  X  |->  ( w `  n
) ) " (
h `  n )
) }  C_  ( { X }  u.  ran  ( k  e.  A ,  u  e.  ( F `  k )  |->  ( `' ( w  e.  X  |->  ( w `
 k ) )
" u ) ) ) )
203 simpr 449 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( A  e.  V  /\  F : A --> Top )  /\  (
h  Fn  A  /\  A. y  e.  A  ( h `  y )  e.  ( F `  y ) ) )  /\  ( m  e. 
Fin  /\  A. y  e.  ( A  \  m
) ( h `  y )  =  U. ( F `  y ) ) )  /\  {
z  |  E. n  e.  ( A  i^i  m
) z  =  ( `' ( w  e.  X  |->  ( w `  n ) ) "
( h `  n
) ) }  =/=  (/) )  ->  { z  |  E. n  e.  ( A  i^i  m ) z  =  ( `' ( w  e.  X  |->  ( w `  n
) ) " (
h `  n )
) }  =/=  (/) )
204 simplrl 738 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( A  e.  V  /\  F : A --> Top )  /\  (
h  Fn  A  /\  A. y  e.  A  ( h `  y )  e.  ( F `  y ) ) )  /\  ( m  e. 
Fin  /\  A. y  e.  ( A  \  m
) ( h `  y )  =  U. ( F `  y ) ) )  /\  {
z  |  E. n  e.  ( A  i^i  m
) z  =  ( `' ( w  e.  X  |->  ( w `  n ) ) "
( h `  n
) ) }  =/=  (/) )  ->  m  e.  Fin )
205 ssfi 7331 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( m  e.  Fin  /\  ( A  i^i  m
)  C_  m )  ->  ( A  i^i  m
)  e.  Fin )
206204, 88, 205sylancl 645 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( A  e.  V  /\  F : A --> Top )  /\  (
h  Fn  A  /\  A. y  e.  A  ( h `  y )  e.  ( F `  y ) ) )  /\  ( m  e. 
Fin  /\  A. y  e.  ( A  \  m
) ( h `  y )  =  U. ( F `  y ) ) )  /\  {
z  |  E. n  e.  ( A  i^i  m
) z  =  ( `' ( w  e.  X  |->  ( w `  n ) ) "
( h `  n
) ) }  =/=  (/) )  ->  ( A  i^i  m )  e.  Fin )
207 abrexfi 7409 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A  i^i  m )  e.  Fin  ->  { z  |  E. n  e.  ( A  i^i  m
) z  =  ( `' ( w  e.  X  |->  ( w `  n ) ) "
( h `  n
) ) }  e.  Fin )
208206, 207syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( A  e.  V  /\  F : A --> Top )  /\  (
h  Fn  A  /\  A. y  e.  A  ( h `  y )  e.  ( F `  y ) ) )  /\  ( m  e. 
Fin  /\  A. y  e.  ( A  \  m
) ( h `  y )  =  U. ( F `  y ) ) )  /\  {
z  |  E. n  e.  ( A  i^i  m
) z  =  ( `' ( w  e.  X  |->  ( w `  n ) ) "
( h `  n
) ) }  =/=  (/) )  ->  { z  |  E. n  e.  ( A  i^i  m ) z  =  ( `' ( w  e.  X  |->  ( w `  n
) ) " (
h `  n )
) }  e.  Fin )
209 elfir 7422 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( { X }  u.  ran  ( k  e.  A ,  u  e.  ( F `  k
)  |->  ( `' ( w  e.  X  |->  ( w `  k ) ) " u ) ) )  e.  _V  /\  ( { z  |  E. n  e.  ( A  i^i  m ) z  =  ( `' ( w  e.  X  |->  ( w `  n
) ) " (
h `  n )
) }  C_  ( { X }  u.  ran  ( k  e.  A ,  u  e.  ( F `  k )  |->  ( `' ( w  e.  X  |->  ( w `
 k ) )
" u ) ) )  /\  { z  |  E. n  e.  ( A  i^i  m
) z  =  ( `' ( w  e.  X  |->  ( w `  n ) ) "
( h `  n
) ) }  =/=  (/) 
/\  { z  |  E. n  e.  ( A  i^i  m ) z  =  ( `' ( w  e.  X  |->  ( w `  n
) ) " (
h `  n )
) }  e.  Fin ) )  ->  |^| { z  |  E. n  e.  ( A  i^i  m
) z  =  ( `' ( w  e.  X  |->  ( w `  n ) ) "
( h `  n
) ) }  e.  ( fi `  ( { X }  u.  ran  ( k  e.  A ,  u  e.  ( F `  k )  |->  ( `' ( w  e.  X  |->  ( w `
 k ) )
" u ) ) ) ) )
210156, 202, 203, 208, 209syl13anc 1187 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( A  e.  V  /\  F : A --> Top )  /\  (
h  Fn  A  /\  A. y  e.  A  ( h `  y )  e.  ( F `  y ) ) )  /\  ( m  e. 
Fin  /\  A. y  e.  ( A  \  m
) ( h `  y )  =  U. ( F `  y ) ) )  /\  {
z  |  E. n  e.  ( A  i^i  m
) z  =  ( `' ( w  e.  X  |->  ( w `  n ) ) "
( h `  n
) ) }  =/=  (/) )  ->  |^| { z  |  E. n  e.  ( A  i^i  m
) z  =  ( `' ( w  e.  X  |->  ( w `  n ) ) "
( h `  n
) ) }  e.  ( fi `  ( { X }  u.  ran  ( k  e.  A ,  u  e.  ( F `  k )  |->  ( `' ( w  e.  X  |->  ( w `
 k ) )
" u ) ) ) ) )
211125, 210syl5eqel 2522 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( A  e.  V  /\  F : A --> Top )  /\  (
h  Fn  A  /\  A. y  e.  A  ( h `  y )  e.  ( F `  y ) ) )  /\  ( m  e. 
Fin  /\  A. y  e.  ( A  \  m
) ( h `  y )  =  U. ( F `  y ) ) )  /\  {
z  |  E. n  e.  ( A  i^i  m
) z  =  ( `' ( w  e.  X  |->  ( w `  n ) ) "
( h `  n
) ) }  =/=  (/) )  ->  |^|_ n  e.  ( A  i^i  m
) ( `' ( w  e.  X  |->  ( w `  n ) ) " ( h `
 n ) )  e.  ( fi `  ( { X }  u.  ran  ( k  e.  A ,  u  e.  ( F `  k )  |->  ( `' ( w  e.  X  |->  ( w `
 k ) )
" u ) ) ) ) )
212 elssuni 4045 . . . . . . . . . . . . . . . 16  |-  ( |^|_ n  e.  ( A  i^i  m ) ( `' ( w  e.  X  |->  ( w `  n
) ) " (
h `  n )
)  e.  ( fi
`  ( { X }  u.  ran  ( k  e.  A ,  u  e.  ( F `  k
)  |->  ( `' ( w  e.  X  |->  ( w `  k ) ) " u ) ) ) )  ->  |^|_ n  e.  ( A  i^i  m ) ( `' ( w  e.  X  |->  ( w `  n ) ) "
( h `  n
) )  C_  U. ( fi `  ( { X }  u.  ran  ( k  e.  A ,  u  e.  ( F `  k
)  |->  ( `' ( w  e.  X  |->  ( w `  k ) ) " u ) ) ) ) )
213211, 212syl 16 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( A  e.  V  /\  F : A --> Top )  /\  (
h  Fn  A  /\  A. y  e.  A  ( h `  y )  e.  ( F `  y ) ) )  /\  ( m  e. 
Fin  /\  A. y  e.  ( A  \  m
) ( h `  y )  =  U. ( F `  y ) ) )  /\  {
z  |  E. n  e.  ( A  i^i  m
) z  =  ( `' ( w  e.  X  |->  ( w `  n ) ) "
( h `  n
) ) }  =/=  (/) )  ->  |^|_ n  e.  ( A  i^i  m
) ( `' ( w  e.  X  |->  ( w `  n ) ) " ( h `
 n ) ) 
C_  U. ( fi `  ( { X }  u.  ran  ( k  e.  A ,  u  e.  ( F `  k )  |->  ( `' ( w  e.  X  |->  ( w `
 k ) )
" u ) ) ) ) )
214 fiuni 7435 . . . . . . . . . . . . . . . . . 18  |-  ( ( { X }  u.  ran  ( k  e.  A ,  u  e.  ( F `  k )  |->  ( `' ( w  e.  X  |->  ( w `
 k ) )
" u ) ) )  e.  _V  ->  U. ( { X }  u.  ran  ( k  e.  A ,  u  e.  ( F `  k
)  |->  ( `' ( w  e.  X  |->  ( w `  k ) ) " u ) ) )  =  U. ( fi `  ( { X }  u.  ran  ( k  e.  A ,  u  e.  ( F `  k )  |->  ( `' ( w  e.  X  |->  ( w `
 k ) )
" u ) ) ) ) )
215145, 214syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ( A  e.  V  /\  F : A --> Top )  ->  U. ( { X }  u.  ran  ( k  e.  A ,  u  e.  ( F `  k
)  |->  ( `' ( w  e.  X  |->  ( w `  k ) ) " u ) ) )  =  U. ( fi `  ( { X }  u.  ran  ( k  e.  A ,  u  e.  ( F `  k )  |->  ( `' ( w  e.  X  |->  ( w `
 k ) )
" u ) ) ) ) )
216120pwid 3814 . . . . . . . . . . . . . . . . . . . . . 22  |-  X  e. 
~P X
217216a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( A  e.  V  /\  F : A --> Top )  ->  X  e.  ~P X
)
218217snssd 3945 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( A  e.  V  /\  F : A --> Top )  ->  { X }  C_  ~P X )
2191ptuni2 17610 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( A  e.  V  /\  F : A --> Top )  -> 
X_ n  e.  A  U. ( F `  n
)  =  U. B
)
22013, 219syl5eq 2482 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( A  e.  V  /\  F : A --> Top )  ->  X  =  U. B
)
221 eqimss2 3403 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( X  =  U. B  ->  U. B  C_  X )
222220, 221syl 16 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( A  e.  V  /\  F : A --> Top )  ->  U. B  C_  X
)
223 sspwuni 4178 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( B 
C_  ~P X  <->  U. B  C_  X )
224222, 223sylibr 205 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( A  e.  V  /\  F : A --> Top )  ->  B  C_  ~P X
)
225142, 224sstrd 3360 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( A  e.  V  /\  F : A --> Top )  ->  ran  ( k  e.  A ,  u  e.  ( F `  k
)  |->  ( `' ( w  e.  X  |->  ( w `  k ) ) " u ) )  C_  ~P X
)
226218, 225unssd 3525 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A  e.  V  /\  F : A --> Top )  ->  ( { X }  u.  ran  ( k  e.  A ,  u  e.  ( F `  k
)  |->  ( `' ( w  e.  X  |->  ( w `  k ) ) " u ) ) )  C_  ~P X )
227 sspwuni 4178 . . . . . . . . . . . . . . . . . . 19  |-  ( ( { X }  u.  ran  ( k  e.  A ,  u  e.  ( F `  k )  |->  ( `' ( w  e.  X  |->  ( w `
 k ) )
" u ) ) )  C_  ~P X  <->  U. ( { X }  u.  ran  ( k  e.  A ,  u  e.  ( F `  k
)  |->  ( `' ( w  e.  X  |->  ( w `  k ) ) " u ) ) )  C_  X
)
228226, 227sylib 190 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  e.  V  /\  F : A --> Top )  ->  U. ( { X }  u.  ran  ( k  e.  A ,  u  e.  ( F `  k
)  |->  ( `' ( w  e.  X  |->  ( w `  k ) ) " u ) ) )  C_  X
)
229 elssuni 4045 . . . . . . . . . . . . . . . . . . . 20  |-  ( X  e.  ( { X }  u.  ran  ( k  e.  A ,  u  e.  ( F `  k
)  |->  ( `' ( w  e.  X  |->  ( w `  k ) ) " u ) ) )  ->  X  C_ 
U. ( { X }  u.  ran  ( k  e.  A ,  u  e.  ( F `  k
)  |->  ( `' ( w  e.  X  |->  ( w `  k ) ) " u ) ) ) )
230151, 229ax-mp 8 . . . . . . . . . . . . . . . . . . 19  |-  X  C_  U. ( { X }  u.  ran  ( k  e.  A ,  u  e.  ( F `  k
)  |->  ( `' ( w  e.  X  |->  ( w `  k ) ) " u ) ) )
231230a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  e.  V  /\  F : A --> Top )  ->  X  C_  U. ( { X }  u.  ran  ( k  e.  A ,  u  e.  ( F `  k )  |->  ( `' ( w  e.  X  |->  ( w `
 k ) )
" u ) ) ) )
232228, 231eqssd 3367 . . . . . . . . . . . . . . . . 17  |-  ( ( A  e.  V  /\  F : A --> Top )  ->  U. ( { X }  u.  ran  ( k  e.  A ,  u  e.  ( F `  k
)  |->  ( `' ( w  e.  X  |->  ( w `  k ) ) " u ) ) )  =  X )
233215, 232eqtr3d 2472 . . . . . . . . . . . . . . . 16  |-  ( ( A  e.  V  /\  F : A --> Top )  ->  U. ( fi `  ( { X }  u.  ran  ( k  e.  A ,  u  e.  ( F `  k )  |->  ( `' ( w  e.  X  |->  ( w `
 k ) )
" u ) ) ) )  =  X )
234233ad3antrrr 712 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( A  e.  V  /\  F : A --> Top )  /\  (
h  Fn  A  /\  A. y  e.  A  ( h `  y )  e.  ( F `  y ) ) )  /\  ( m  e. 
Fin  /\  A. y  e.  ( A  \  m
) ( h `  y )  =  U. ( F `  y ) ) )  /\  {
z  |  E. n  e.  ( A  i^i  m
) z  =  ( `' ( w  e.  X  |->  ( w `  n ) ) "
( h `  n
) ) }  =/=  (/) )  ->  U. ( fi `  ( { X }  u.  ran  ( k  e.  A ,  u  e.  ( F `  k
)  |->  ( `' ( w  e.  X  |->  ( w `  k ) ) " u ) ) ) )  =  X )
235213, 234sseqtrd 3386 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( A  e.  V  /\  F : A --> Top )  /\  (
h  Fn  A  /\  A. y  e.  A  ( h `  y )  e.  ( F `  y ) ) )  /\  ( m  e. 
Fin  /\  A. y  e.  ( A  \  m
) ( h `  y )  =  U. ( F `  y ) ) )  /\  {
z  |  E. n  e.  ( A  i^i  m
) z  =  ( `' ( w  e.  X  |->  ( w `  n ) ) "
( h `  n
) ) }  =/=  (/) )  ->  |^|_ n  e.  ( A  i^i  m
) ( `' ( w  e.  X  |->  ( w `  n ) ) " ( h `
 n ) ) 
C_  X )
236235, 56sylib 190 . . . . . . . . . . . . 13  |-  ( ( ( ( ( A  e.  V  /\  F : A --> Top )  /\  (
h  Fn  A  /\  A. y  e.  A  ( h `  y )  e.  ( F `  y ) ) )  /\  ( m  e. 
Fin  /\  A. y  e.  ( A  \  m
) ( h `  y )  =  U. ( F `  y ) ) )  /\  {
z  |  E. n  e.  ( A  i^i  m
) z  =  ( `' ( w  e.  X  |->  ( w `  n ) ) "
( h `  n
) ) }  =/=  (/) )  ->  ( X  i^i  |^|_ n  e.  ( A  i^i  m ) ( `' ( w  e.  X  |->  ( w `
 n ) )
" ( h `  n ) ) )  =  |^|_ n  e.  ( A  i^i  m ) ( `' ( w  e.  X  |->  ( w `
 n ) )
" ( h `  n ) ) )
237236, 211eqeltrd 2512 . . . . . . . . . . . 12  |-  ( ( ( ( ( A  e.  V  /\  F : A --> Top )  /\  (
h  Fn  A  /\  A. y  e.  A  ( h `  y )  e.  ( F `  y ) ) )  /\  ( m  e. 
Fin  /\  A. y  e.  ( A  \  m
) ( h `  y )  =  U. ( F `  y ) ) )  /\  {
z  |  E. n  e.  ( A  i^i  m
) z  =  ( `' ( w  e.  X  |->  ( w `  n ) ) "
( h `  n
) ) }  =/=  (/) )  ->  ( X  i^i  |^|_ n  e.  ( A  i^i  m ) ( `' ( w  e.  X  |->  ( w `
 n ) )
" ( h `  n ) ) )  e.  ( fi `  ( { X }  u.  ran  ( k  e.  A ,  u  e.  ( F `  k )  |->  ( `' ( w  e.  X  |->  ( w `
 k ) )
" u ) ) ) ) )
238155, 237pm2.61dane 2684 . . . . . . . . . . 11  |-  ( ( ( ( A  e.  V  /\  F : A
--> Top )  /\  (
h  Fn  A  /\  A. y  e.  A  ( h `  y )  e.  ( F `  y ) ) )  /\  ( m  e. 
Fin  /\  A. y  e.  ( A  \  m
) ( h `  y )  =  U. ( F `  y ) ) )  ->  ( X  i^i  |^|_ n  e.  ( A  i^i  m ) ( `' ( w  e.  X  |->  ( w `
 n ) )
" ( h `  n ) ) )  e.  ( fi `  ( { X }  u.  ran  ( k  e.  A ,  u  e.  ( F `  k )  |->  ( `' ( w  e.  X  |->  ( w `
 k ) )
" u ) ) ) ) )
239114, 238eqeltrd 2512 . . . . . . . . . 10  |-  ( ( ( ( A  e.  V  /\  F : A
--> Top )  /\  (
h  Fn  A  /\  A. y  e.  A  ( h `  y )  e.  ( F `  y ) ) )  /\  ( m  e. 
Fin  /\  A. y  e.  ( A  \  m
) ( h `  y )  =  U. ( F `  y ) ) )  ->  X_ y  e.  A  ( h `  y )  e.  ( fi `  ( { X }  u.  ran  ( k  e.  A ,  u  e.  ( F `  k )  |->  ( `' ( w  e.  X  |->  ( w `
 k ) )
" u ) ) ) ) )
240239rexlimdvaa 2833 . . . . . . . . 9  |-  ( ( ( A  e.  V  /\  F : A --> Top )  /\  ( h  Fn  A  /\  A. y  e.  A  ( h `  y
)  e.  ( F `
 y ) ) )  ->  ( E. m  e.  Fin  A. y  e.  ( A  \  m
) ( h `  y )  =  U. ( F `  y )  ->  X_ y  e.  A  ( h `  y
)  e.  ( fi
`  ( { X }  u.  ran  ( k  e.  A ,  u  e.  ( F `  k
)  |->  ( `' ( w  e.  X  |->  ( w `  k ) ) " u ) ) ) ) ) )
241240impr 604 . . . . . . . 8  |-  ( ( ( A  e.  V  /\  F : A --> Top )  /\  ( ( h  Fn  A  /\  A. y  e.  A  ( h `  y )  e.  ( F `  y ) )  /\  E. m  e.  Fin  A. y  e.  ( A  \  m
) ( h `  y )  =  U. ( F `  y ) ) )  ->  X_ y  e.  A  ( h `  y )  e.  ( fi `  ( { X }  u.  ran  ( k  e.  A ,  u  e.  ( F `  k )  |->  ( `' ( w  e.  X  |->  ( w `
 k ) )
" u ) ) ) ) )
2423, 241sylan2b 463 . . . . . . 7  |-  ( ( ( A  e.  V  /\  F : A --> Top )  /\  ( h