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

Theorem ptbasfi 17276
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 17267 . . . 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 936 . . . . . . . 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 733 . . . . . . . . . . . . . . 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. y  e.  ( A  \  m
) ( h `  y )  =  U. ( F `  y ) )
5 difeq2 3288 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( A  i^i  m )  =  (/)  ->  ( A 
\  ( A  i^i  m ) )  =  ( A  \  (/) ) )
6 difin 3406 . . . . . . . . . . . . . . . . . . . 20  |-  ( A 
\  ( A  i^i  m ) )  =  ( A  \  m
)
7 dif0 3524 . . . . . . . . . . . . . . . . . . . 20  |-  ( A 
\  (/) )  =  A
85, 6, 73eqtr3g 2338 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A  i^i  m )  =  (/)  ->  ( A 
\  m )  =  A )
98raleqdv 2742 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  i^i  m )  =  (/)  ->  ( A. y  e.  ( A  \  m ) ( h `
 y )  = 
U. ( F `  y )  <->  A. y  e.  A  ( h `  y )  =  U. ( F `  y ) ) )
109biimpac 472 . . . . . . . . . . . . . . . . 17  |-  ( ( 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 6830 . . . . . . . . . . . . . . . . 17  |-  ( A. y  e.  A  (
h `  y )  =  U. ( F `  y )  ->  X_ y  e.  A  ( h `  y )  =  X_ y  e.  A  U. ( F `  y ) )
1210, 11syl 15 . . . . . . . . . . . . . . . 16  |-  ( ( 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 . . . . . . . . . . . . . . . . 17  |-  X  = 
X_ n  e.  A  U. ( F `  n
)
14 fveq2 5525 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  y  ->  ( F `  n )  =  ( F `  y ) )
1514unieqd 3838 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  y  ->  U. ( F `  n )  =  U. ( F `  y ) )
1615cbvixpv 6834 . . . . . . . . . . . . . . . . 17  |-  X_ n  e.  A  U. ( F `  n )  =  X_ y  e.  A  U. ( F `  y
)
1713, 16eqtri 2303 . . . . . . . . . . . . . . . 16  |-  X  = 
X_ y  e.  A  U. ( F `  y
)
1812, 17syl6eqr 2333 . . . . . . . . . . . . . . 15  |-  ( ( A. y  e.  ( A  \  m ) ( h `  y
)  =  U. ( F `  y )  /\  ( A  i^i  m
)  =  (/) )  ->  X_ y  e.  A  ( h `  y )  =  X )
194, 18sylan 457 . . . . . . . . . . . . . 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 )
20 ssv 3198 . . . . . . . . . . . . . . . . 17  |-  X  C_  _V
21 iineq1 3919 . . . . . . . . . . . . . . . . . 18  |-  ( ( 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 3960 . . . . . . . . . . . . . . . . . 18  |-  |^|_ n  e.  (/)  ( `' ( w  e.  X  |->  ( w `  n ) ) " ( h `
 n ) )  =  _V
2321, 22syl6eq 2331 . . . . . . . . . . . . . . . . 17  |-  ( ( A  i^i  m )  =  (/)  ->  |^|_ n  e.  ( A  i^i  m
) ( `' ( w  e.  X  |->  ( w `  n ) ) " ( h `
 n ) )  =  _V )
2420, 23syl5sseqr 3227 . . . . . . . . . . . . . . . 16  |-  ( ( A  i^i  m )  =  (/)  ->  X  C_  |^|_
n  e.  ( A  i^i  m ) ( `' ( w  e.  X  |->  ( w `  n ) ) "
( h `  n
) ) )
2524adantl 452 . . . . . . . . . . . . . . 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 )  =  (/) )  ->  X  C_  |^|_
n  e.  ( A  i^i  m ) ( `' ( w  e.  X  |->  ( w `  n ) ) "
( h `  n
) ) )
26 df-ss 3166 . . . . . . . . . . . . . . 15  |-  ( 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 188 . . . . . . . . . . . . . 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  i^i  |^|_ n  e.  ( A  i^i  m ) ( `' ( w  e.  X  |->  ( w `
 n ) )
" ( h `  n ) ) )  =  X )
2819, 27eqtr4d 2318 . . . . . . . . . . . . 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  i^i  |^|_ n  e.  ( A  i^i  m
) ( `' ( w  e.  X  |->  ( w `  n ) ) " ( h `
 n ) ) ) )
29 simplll 734 . . . . . . . . . . . . . . . . 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  e.  V  /\  F : A --> Top )
)
30 inss1 3389 . . . . . . . . . . . . . . . . . 18  |-  ( A  i^i  m )  C_  A
31 simpr 447 . . . . . . . . . . . . . . . . . 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 ) ) )  /\  n  e.  ( A  i^i  m
) )  ->  n  e.  ( A  i^i  m
) )
3230, 31sseldi 3178 . . . . . . . . . . . . . . . . 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 )
33 simprr 733 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( 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 706 . . . . . . . . . . . . . . . . . 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 ) ) )  /\  n  e.  ( A  i^i  m
) )  ->  A. y  e.  A  ( h `  y )  e.  ( F `  y ) )
35 fveq2 5525 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  =  n  ->  (
h `  y )  =  ( h `  n ) )
36 fveq2 5525 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  =  n  ->  ( F `  y )  =  ( F `  n ) )
3735, 36eleq12d 2351 . . . . . . . . . . . . . . . . . . 19  |-  ( y  =  n  ->  (
( h `  y
)  e.  ( F `
 y )  <->  ( h `  n )  e.  ( F `  n ) ) )
3837rspcv 2880 . . . . . . . . . . . . . . . . . 18  |-  ( n  e.  A  ->  ( A. y  e.  A  ( h `  y
)  e.  ( F `
 y )  -> 
( h `  n
)  e.  ( F `
 n ) ) )
3932, 34, 38sylc 56 . . . . . . . . . . . . . . . . 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
) )  ->  (
h `  n )  e.  ( F `  n
) )
4017ptpjpre1 17266 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 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 1180 . . . . . . . . . . . . . . . 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
) )  ->  ( `' ( w  e.  X  |->  ( w `  n ) ) "
( h `  n
) )  =  X_ y  e.  A  if ( y  =  n ,  ( h `  n ) ,  U. ( F `  y ) ) )
4241adantlr 695 . . . . . . . . . . . . . . 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 ) )  = 
X_ y  e.  A  if ( y  =  n ,  ( h `  n ) ,  U. ( F `  y ) ) )
4342iineq2dv 3927 . . . . . . . . . . . . . 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 ) )  =  |^|_ n  e.  ( A  i^i  m )
X_ y  e.  A  if ( y  =  n ,  ( h `  n ) ,  U. ( F `  y ) ) )
44 simpr 447 . . . . . . . . . . . . . . . . . 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 ) ) )  /\  ( A  i^i  m )  =/=  (/) )  ->  ( A  i^i  m )  =/=  (/) )
45 cnvimass 5033 . . . . . . . . . . . . . . . . . . . . 21  |-  ( `' ( w  e.  X  |->  ( w `  n
) ) " (
h `  n )
)  C_  dom  ( w  e.  X  |->  ( w `
 n ) )
46 eqid 2283 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( w  e.  X  |->  ( w `
 n ) )  =  ( w  e.  X  |->  ( w `  n ) )
4746dmmptss 5169 . . . . . . . . . . . . . . . . . . . . 21  |-  dom  (
w  e.  X  |->  ( w `  n ) )  C_  X
4845, 47sstri 3188 . . . . . . . . . . . . . . . . . . . 20  |-  ( `' ( w  e.  X  |->  ( w `  n
) ) " (
h `  n )
)  C_  X
4948, 17sseqtri 3210 . . . . . . . . . . . . . . . . . . 19  |-  ( `' ( w  e.  X  |->  ( w `  n
) ) " (
h `  n )
)  C_  X_ y  e.  A  U. ( F `
 y )
5049rgenw 2610 . . . . . . . . . . . . . . . . . 18  |-  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 3543 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( 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 643 . . . . . . . . . . . . . . . . 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 )  =/=  (/) )  ->  E. n  e.  ( A  i^i  m
) ( `' ( w  e.  X  |->  ( w `  n ) ) " ( h `
 n ) ) 
C_  X_ y  e.  A  U. ( F `  y
) )
53 iinss 3953 . . . . . . . . . . . . . . . . 17  |-  ( 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 15 . . . . . . . . . . . . . . . 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 )  =/=  (/) )  ->  |^|_ n  e.  ( A  i^i  m
) ( `' ( w  e.  X  |->  ( w `  n ) ) " ( h `
 n ) ) 
C_  X_ y  e.  A  U. ( F `  y
) )
5554, 17syl6sseqr 3225 . . . . . . . . . . . . . . 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 )
56 dfss1 3373 . . . . . . . . . . . . . . 15  |-  ( |^|_ 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 188 . . . . . . . . . . . . . 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  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 706 . . . . . . . . . . . . . . . . . 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 ) ) )  /\  ( A  i^i  m )  =/=  (/) )  ->  A. y  e.  A  ( h `  y )  e.  ( F `  y ) )
59 ssralv 3237 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 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 . . . . . . . . . . . . . . . . . 18  |-  ( A. y  e.  A  (
h `  y )  e.  ( F `  y
)  ->  A. y  e.  ( A  i^i  m
) ( h `  y )  e.  ( F `  y ) )
61 elssuni 3855 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( h `  y )  e.  ( F `  y )  ->  (
h `  y )  C_ 
U. ( F `  y ) )
62 iffalse 3572 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( -.  y  =  n  ->  if ( y  =  n ,  ( h `  n ) ,  U. ( F `  y ) )  =  U. ( F `  y )
)
6362sseq2d 3206 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( -.  y  =  n  -> 
( ( h `  y )  C_  if ( y  =  n ,  ( h `  n ) ,  U. ( F `  y ) )  <->  ( h `  y )  C_  U. ( F `  y )
) )
6461, 63syl5ibrcom 213 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( h `  y )  e.  ( F `  y )  ->  ( -.  y  =  n  ->  ( h `  y
)  C_  if (
y  =  n ,  ( h `  n
) ,  U. ( F `  y )
) ) )
65 ssid 3197 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( h `
 y )  C_  ( h `  y
)
66 iftrue 3571 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( y  =  n  ->  if ( y  =  n ,  ( h `  n ) ,  U. ( F `  y ) )  =  ( h `
 n ) )
6766, 35eqtr4d 2318 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  =  n  ->  if ( y  =  n ,  ( h `  n ) ,  U. ( F `  y ) )  =  ( h `
 y ) )
6865, 67syl5sseqr 3227 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  =  n  ->  (
h `  y )  C_  if ( y  =  n ,  ( h `
 n ) , 
U. ( F `  y ) ) )
6964, 68pm2.61d2 152 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( h `  y )  e.  ( F `  y )  ->  (
h `  y )  C_  if ( y  =  n ,  ( h `
 n ) , 
U. ( F `  y ) ) )
7069ralrimivw 2627 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( 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 3952 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( 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 203 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( h `  y )  e.  ( F `  y )  ->  (
h `  y )  C_ 
|^|_ n  e.  ( A  i^i  m ) if ( y  =  n ,  ( h `  n ) ,  U. ( F `  y ) ) )
7372adantl 452 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 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 ) ) )
7466eqcoms 2286 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( n  =  y  ->  if ( y  =  n ,  ( h `  n ) ,  U. ( F `  y ) )  =  ( h `
 n ) )
75 fveq2 5525 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( n  =  y  ->  (
h `  n )  =  ( h `  y ) )
7674, 75eqtrd 2315 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( n  =  y  ->  if ( y  =  n ,  ( h `  n ) ,  U. ( F `  y ) )  =  ( h `
 y ) )
7776sseq1d 3205 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( n  =  y  ->  ( if ( y  =  n ,  ( h `  n ) ,  U. ( F `  y ) )  C_  ( h `  y )  <->  ( h `  y )  C_  (
h `  y )
) )
7877rspcev 2884 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( 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 652 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 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 3953 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 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 15 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  e.  ( A  i^i  m )  ->  |^|_ n  e.  ( A  i^i  m
) if ( y  =  n ,  ( h `  n ) ,  U. ( F `
 y ) ) 
C_  ( h `  y ) )
8281adantr 451 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 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 3196 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 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 2617 . . . . . . . . . . . . . . . . . 18  |-  ( 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 18 . . . . . . . . . . . . . . . . 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  i^i  m
) ( h `  y )  =  |^|_ n  e.  ( A  i^i  m ) if ( y  =  n ,  ( h `  n
) ,  U. ( F `  y )
) )
86 eldifn 3299 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  e.  ( A  \  m )  ->  -.  y  e.  m )
8786ad2antlr 707 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( A  i^i  m )  =/=  (/)  /\  y  e.  ( A  \  m
) )  /\  n  e.  ( A  i^i  m
) )  ->  -.  y  e.  m )
88 inss2 3390 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( A  i^i  m )  C_  m
89 simpr 447 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( A  i^i  m )  =/=  (/)  /\  y  e.  ( A  \  m
) )  /\  n  e.  ( A  i^i  m
) )  ->  n  e.  ( A  i^i  m
) )
9088, 89sseldi 3178 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( A  i^i  m )  =/=  (/)  /\  y  e.  ( A  \  m
) )  /\  n  e.  ( A  i^i  m
) )  ->  n  e.  m )
91 eleq1 2343 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  =  n  ->  (
y  e.  m  <->  n  e.  m ) )
9290, 91syl5ibrcom 213 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( A  i^i  m )  =/=  (/)  /\  y  e.  ( A  \  m
) )  /\  n  e.  ( A  i^i  m
) )  ->  (
y  =  n  -> 
y  e.  m ) )
9387, 92mtod 168 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( A  i^i  m )  =/=  (/)  /\  y  e.  ( A  \  m
) )  /\  n  e.  ( A  i^i  m
) )  ->  -.  y  =  n )
9493, 62syl 15 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( 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 3927 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( 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 3914 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( A  i^i  m )  =/=  (/)  ->  |^|_ n  e.  ( A  i^i  m
) U. ( F `
 y )  = 
U. ( F `  y ) )
9796adantr 451 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( A  i^i  m
)  =/=  (/)  /\  y  e.  ( A  \  m
) )  ->  |^|_ n  e.  ( A  i^i  m
) U. ( F `
 y )  = 
U. ( F `  y ) )
9895, 97eqtr2d 2316 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( 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 2289 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 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 213 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( 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 2621 . . . . . . . . . . . . . . . . . 18  |-  ( ( 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 455 . . . . . . . . . . . . . . . . 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  \  m
) ( h `  y )  =  |^|_ n  e.  ( A  i^i  m ) if ( y  =  n ,  ( h `  n
) ,  U. ( F `  y )
) )
103 inundif 3532 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A  i^i  m )  u.  ( A  \  m ) )  =  A
104103raleqi 2740 . . . . . . . . . . . . . . . . . 18  |-  ( 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 3356 . . . . . . . . . . . . . . . . . 18  |-  ( 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 242 . . . . . . . . . . . . . . . . 17  |-  ( 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 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 )  =/=  (/) )  ->  A. y  e.  A  ( h `  y )  =  |^|_ n  e.  ( A  i^i  m ) if ( y  =  n ,  ( h `  n
) ,  U. ( F `  y )
) )
108 ixpeq2 6830 . . . . . . . . . . . . . . . 16  |-  ( 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 15 . . . . . . . . . . . . . . 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 )  =/=  (/) )  ->  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 6842 . . . . . . . . . . . . . . . 16  |-  ( ( 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 452 . . . . . . . . . . . . . . 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 )  =/=  (/) )  ->  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 2315 . . . . . . . . . . . . . 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 )  =  |^|_ n  e.  ( A  i^i  m ) X_ y  e.  A  if (
y  =  n ,  ( h `  n
) ,  U. ( F `  y )
) )
11343, 57, 1123eqtr4rd 2326 . . . . . . . . . . . . 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  i^i  |^|_ n  e.  ( A  i^i  m
) ( `' ( w  e.  X  |->  ( w `  n ) ) " ( h `
 n ) ) ) )
11428, 113pm2.61dane 2524 . . . . . . . . . . . 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 ) ) )  ->  X_ y  e.  A  ( h `  y )  =  ( X  i^i  |^|_ n  e.  ( A  i^i  m
) ( `' ( w  e.  X  |->  ( w `  n ) ) " ( h `
 n ) ) ) )
115 ixpexg 6840 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( A. n  e.  A  U. ( F `  n )  e.  _V  ->  X_ n  e.  A  U. ( F `  n )  e.  _V )
116 fvex 5539 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( F `
 n )  e. 
_V
117116uniex 4516 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  U. ( F `  n )  e.  _V
118117a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( n  e.  A  ->  U. ( F `  n )  e.  _V )
119115, 118mprg 2612 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  X_ n  e.  A  U. ( F `  n )  e.  _V
12013, 119eqeltri 2353 . . . . . . . . . . . . . . . . . . . . . . 23  |-  X  e. 
_V
121120mptex 5746 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( w  e.  X  |->  ( w `
 n ) )  e.  _V
122121cnvex 5209 . . . . . . . . . . . . . . . . . . . . 21  |-  `' ( w  e.  X  |->  ( w `  n ) )  e.  _V
123 imaexg 5026 . . . . . . . . . . . . . . . . . . . . 21  |-  ( `' ( w  e.  X  |->  ( w `  n
) )  e.  _V  ->  ( `' ( w  e.  X  |->  ( w `
 n ) )
" ( h `  n ) )  e. 
_V )
124122, 123ax-mp 8 . . . . . . . . . . . . . . . . . . . 20  |-  ( `' ( w  e.  X  |->  ( w `  n
) ) " (
h `  n )
)  e.  _V
125124dfiin2 3938 . . . . . . . . . . . . . . . . . . 19  |-  |^|_ 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 3865 . . . . . . . . . . . . . . . . . . 19  |-  ( { 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 2327 . . . . . . . . . . . . . . . . . 18  |-  ( { 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 3876 . . . . . . . . . . . . . . . . . 18  |-  |^| (/)  =  _V
129127, 128syl6eq 2331 . . . . . . . . . . . . . . . . 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 ) )  =  _V )
130129ineq2d 3370 . . . . . . . . . . . . . . . 16  |-  ( { 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 3481 . . . . . . . . . . . . . . . 16  |-  ( X  i^i  _V )  =  X
132130, 131syl6eq 2331 . . . . . . . . . . . . . . 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 )
133132adantl 452 . . . . . . . . . . . . . 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
) ) }  =  (/) )  ->  ( X  i^i  |^|_ n  e.  ( A  i^i  m ) ( `' ( w  e.  X  |->  ( w `
 n ) )
" ( h `  n ) ) )  =  X )
134 snex 4216 . . . . . . . . . . . . . . . . . . 19  |-  { X }  e.  _V
1351, 13ptpjpre2 17275 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( A  e.  V  /\  F : A --> Top )  /\  ( k  e.  A  /\  u  e.  ( F `  k )
) )  ->  ( `' ( w  e.  X  |->  ( w `  k ) ) "
u )  e.  B
)
136135ralrimivva 2635 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( A  e.  V  /\  F : A --> Top )  ->  A. k  e.  A  A. u  e.  ( F `  k )
( `' ( w  e.  X  |->  ( w `
 k ) )
" u )  e.  B )
137 eqid 2283 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( 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 ) )
138137fmpt2x 6190 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 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 )
139136, 138sylib 188 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 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 )
140 frn 5395 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 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 )
141139, 140syl 15 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( A  e.  V  /\  F : A --> Top )  ->  ran  ( k  e.  A ,  u  e.  ( F `  k
)  |->  ( `' ( w  e.  X  |->  ( w `  k ) ) " u ) )  C_  B )
1421ptbas 17274 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( A  e.  V  /\  F : A --> Top )  ->  B  e.  TopBases )
143 ssexg 4160 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ran  ( k  e.  A ,  u  e.  ( F `  k
)  |->  ( `' ( w  e.  X  |->  ( w `  k ) ) " u ) )  C_  B  /\  B  e.  TopBases )  ->  ran  ( k  e.  A ,  u  e.  ( F `  k )  |->  ( `' ( w  e.  X  |->  ( w `
 k ) )
" u ) )  e.  _V )
144141, 142, 143syl2anc 642 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A  e.  V  /\  F : A --> Top )  ->  ran  ( k  e.  A ,  u  e.  ( F `  k
)  |->  ( `' ( w  e.  X  |->  ( w `  k ) ) " u ) )  e.  _V )
145 unexg 4521 . . . . . . . . . . . . . . . . . . 19  |-  ( ( { 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 )
146134, 144, 145sylancr 644 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  e.  V  /\  F : A --> Top )  ->  ( { X }  u.  ran  ( k  e.  A ,  u  e.  ( F `  k
)  |->  ( `' ( w  e.  X  |->  ( w `  k ) ) " u ) ) )  e.  _V )
147 ssfii 7172 . . . . . . . . . . . . . . . . . 18  |-  ( ( { 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 ) ) ) ) )
148146, 147syl 15 . . . . . . . . . . . . . . . . 17  |-  ( ( 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 ) ) ) ) )
149148ad2antrr 706 . . . . . . . . . . . . . . . 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 ) ) )  ->  ( { 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 ) ) ) ) )
150 ssun1 3338 . . . . . . . . . . . . . . . . . 18  |-  { X }  C_  ( { X }  u.  ran  ( k  e.  A ,  u  e.  ( F `  k
)  |->  ( `' ( w  e.  X  |->  ( w `  k ) ) " u ) ) )
151120snss 3748 . . . . . . . . . . . . . . . . . 18  |-  ( 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 ) ) ) )
152150, 151mpbir 200 . . . . . . . . . . . . . . . . 17  |-  X  e.  ( { X }  u.  ran  ( k  e.  A ,  u  e.  ( F `  k
)  |->  ( `' ( w  e.  X  |->  ( w `  k ) ) " u ) ) )
153152a1i 10 . . . . . . . . . . . . . . . 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 ) ) )  ->  X  e.  ( { X }  u.  ran  ( k  e.  A ,  u  e.  ( F `  k
)  |->  ( `' ( w  e.  X  |->  ( w `  k ) ) " u ) ) ) )
154149, 153sseldd 3181 . . . . . . . . . . . . . . 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.  ( fi `  ( { X }  u.  ran  ( k  e.  A ,  u  e.  ( F `  k )  |->  ( `' ( w  e.  X  |->  ( w `
 k ) )
" u ) ) ) ) )
155154adantr 451 . . . . . . . . . . . . . 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
) ) }  =  (/) )  ->  X  e.  ( fi `  ( { X }  u.  ran  ( k  e.  A ,  u  e.  ( F `  k )  |->  ( `' ( w  e.  X  |->  ( w `
 k ) )
" u ) ) ) ) )
156133, 155eqeltrd 2357 . . . . . . . . . . . . 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 ) ) )  e.  ( fi `  ( { X }  u.  ran  ( k  e.  A ,  u  e.  ( F `  k )  |->  ( `' ( w  e.  X  |->  ( w `
 k ) )
" u ) ) ) ) )
157146ad3antrrr 710 . . . . . . . . . . . . . . . . . . 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
) ) }  =/=  (/) )  ->  ( { X }  u.  ran  ( k  e.  A ,  u  e.  ( F `  k )  |->  ( `' ( w  e.  X  |->  ( w `
 k ) )
" u ) ) )  e.  _V )
158 nfv 1605 . . . . . . . . . . . . . . . . . . . . . . 23  |-  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 ) ) )
159 nfcv 2419 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  F/_ n A
160 nfcv 2419 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  F/_ n
( F `  k
)
161 nfixp1 6836 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  F/_ n X_ n  e.  A  U. ( F `  n )
16213, 161nfcxfr 2416 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  F/_ n X
163 nfcv 2419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  F/_ n
( w `  k
)
164162, 163nfmpt 4108 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  F/_ n
( w  e.  X  |->  ( w `  k
) )
165164nfcnv 4860 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  F/_ n `' ( w  e.  X  |->  ( w `  k ) )
166 nfcv 2419 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  F/_ n u
167165, 166nfima 5020 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  F/_ n
( `' ( w  e.  X  |->  ( w `
 k ) )
" u )
168159, 160, 167nfmpt2 5916 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  F/_ n
( k  e.  A ,  u  e.  ( F `  k )  |->  ( `' ( w  e.  X  |->  ( w `
 k ) )
" u ) )
169168nfrn 4921 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  F/_ n ran  ( k  e.  A ,  u  e.  ( F `  k )  |->  ( `' ( w  e.  X  |->  ( w `
 k ) )
" u ) )
170169nfcri 2413 . . . . . . . . . . . . . . . . . . . . . . 23  |-  F/ n  z  e.  ran  ( k  e.  A ,  u  e.  ( F `  k
)  |->  ( `' ( w  e.  X  |->  ( w `  k ) ) " u ) )
171 df-ov 5861 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( 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 )
>. )
172124a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( 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 )
173 fveq2 5525 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( k  =  n  ->  (
w `  k )  =  ( w `  n ) )
174173mpteq2dv 4107 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( k  =  n  ->  (
w  e.  X  |->  ( w `  k ) )  =  ( w  e.  X  |->  ( w `
 n ) ) )
175174cnveqd 4857 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( k  =  n  ->  `' ( w  e.  X  |->  ( w `  k
) )  =  `' ( w  e.  X  |->  ( w `  n
) ) )
176175imaeq1d 5011 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( k  =  n  ->  ( `' ( w  e.  X  |->  ( w `  k ) ) "
u )  =  ( `' ( w  e.  X  |->  ( w `  n ) ) "
u ) )
177 imaeq2 5008 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( u  =  ( h `  n )  ->  ( `' ( w  e.  X  |->  ( w `  n ) ) "
u )  =  ( `' ( w  e.  X  |->  ( w `  n ) ) "
( h `  n
) ) )
178176, 177sylan9eq 2335 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( k  =  n  /\  u  =  ( h `  n ) )  -> 
( `' ( w  e.  X  |->  ( w `
 k ) )
" u )  =  ( `' ( w  e.  X  |->  ( w `
 n ) )
" ( h `  n ) ) )
179 fveq2 5525 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( k  =  n  ->  ( F `  k )  =  ( F `  n ) )
180178, 179, 137ovmpt2x 5976 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( 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 ) ) )
18132, 39, 172, 180syl3anc 1182 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ( k  e.  A ,  u  e.  ( F `  k
)  |->  ( `' ( w  e.  X  |->  ( w `  k ) ) " u ) ) ( h `  n ) )  =  ( `' ( w  e.  X  |->  ( w `
 n ) )
" ( h `  n ) ) )
182171, 181syl5eqr 2329 . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) `
 <. n ,  ( h `  n )
>. )  =  ( `' ( w  e.  X  |->  ( w `  n ) ) "
( h `  n
) ) )
183139ad3antrrr 710 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( 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 )
184 ffn 5389 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( 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 ) ) )
185183, 184syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) )  Fn  U_ k  e.  A  ( { k }  X.  ( F `  k ) ) )
186 opeliunxp 4740 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( <.
n ,  ( h `
 n ) >.  e.  U_ n  e.  A  ( { n }  X.  ( F `  n ) )  <->  ( n  e.  A  /\  ( h `
 n )  e.  ( F `  n
) ) )
18732, 39, 186sylanbrc 645 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( 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 ) ) )
188 sneq 3651 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( n  =  k  ->  { n }  =  { k } )
189 fveq2 5525 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( n  =  k  ->  ( F `  n )  =  ( F `  k ) )
190188, 189xpeq12d 4714 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( n  =  k  ->  ( { n }  X.  ( F `  n ) )  =  ( { k }  X.  ( F `  k )
) )
191190cbviunv 3941 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  U_ n  e.  A  ( {
n }  X.  ( F `  n )
)  =  U_ k  e.  A  ( {
k }  X.  ( F `  k )
)
192187, 191syl6eleq 2373 . . . . . . . . . . . . . . . . . . . . . . . . . . 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_ k  e.  A  ( { k }  X.  ( F `  k ) ) )
193 fnfvelrn 5662 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( 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 ) ) )
194185, 192, 193syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) `
 <. n ,  ( h `  n )
>. )  e.  ran  ( k  e.  A ,  u  e.  ( F `  k )  |->  ( `' ( w  e.  X  |->  ( w `
 k ) )
" u ) ) )
195182, 194eqeltrrd 2358 . . . . . . . . . . . . . . . . . . . . . . . . 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
) )  ->  ( `' ( w  e.  X  |->  ( w `  n ) ) "
( h `  n
) )  e.  ran  ( k  e.  A ,  u  e.  ( F `  k )  |->  ( `' ( w  e.  X  |->  ( w `
 k ) )
" u ) ) )
196 eleq1 2343 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( 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 ) ) ) )
197195, 196syl5ibrcom 213 . . . . . . . . . . . . . . . . . . . . . . . 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
) )  ->  (
z  =  ( `' ( w  e.  X  |->  ( w `  n
) ) " (
h `  n )
)  ->  z  e.  ran  ( k  e.  A ,  u  e.  ( F `  k )  |->  ( `' ( w  e.  X  |->  ( w `
 k ) )
" u ) ) ) )
198197ex 423 . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
199158, 170, 198rexlimd 2664 . . . . . . . . . . . . . . . . . . . . . 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 ) ) )  ->  ( 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 ) ) ) )
200199abssdv 3247 . . . . . . . . . . . . . . . . . . . . 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 ) ) )  ->  { 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 ) ) )
201 ssun2 3339 . . . . . . . . . . . . . . . . . . . . 21  |-  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 ) ) )
202200, 201syl6ss 3191 . . . . . . . . . . . . . . . . . . . 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_  ( { X }  u.  ran  ( k  e.  A ,  u  e.  ( F `  k )  |->  ( `' ( w  e.  X  |->  ( w `
 k ) )
" u ) ) ) )
203202adantr 451 . . . . . . . . . . . . . . . . . . 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
) ) }  =/=  (/) )  ->  { 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 ) ) ) )
204 simpr 447 . . . . . . . . . . . . . . . . . . 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
) ) }  =/=  (/) )  ->  { z  |  E. n  e.  ( A  i^i  m ) z  =  ( `' ( w  e.  X  |->  ( w `  n
) ) " (
h `  n )
) }  =/=  (/) )
205 simplrl 736 . . . . . . . . . . . . . . . . . . . . 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 ) ) )  /\  {
z  |  E. n  e.  ( A  i^i  m
) z  =  ( `' ( w  e.  X  |->  ( w `  n ) ) "
( h `  n
) ) }  =/=  (/) )  ->  m  e.  Fin )
206 ssfi 7083 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( m  e.  Fin  /\  ( A  i^i  m
)  C_  m )  ->  ( A  i^i  m
)  e.  Fin )
207205, 88, 206sylancl 643 . . . . . . . . . . . . . . . . . . . 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
) ) }  =/=  (/) )  ->  ( A  i^i  m )  e.  Fin )
208 abrexfi 7156 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( A  i^i  m )  e.  Fin  ->  { z  |  E. n  e.  ( A  i^i  m
) z  =  ( `' ( w  e.  X  |->  ( w `  n ) ) "
( h `  n
) ) }  e.  Fin )
209207, 208syl 15 . . . . . . . . . . . . . . . . . . 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
) ) }  =/=  (/) )  ->  { z  |  E. n  e.  ( A  i^i  m ) z  =  ( `' ( w  e.  X  |->  ( w `  n
) ) " (
h `  n )
) }  e.  Fin )
210 elfir 7169 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( { 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 ) ) ) ) )
211157, 203, 204, 209, 210syl13anc 1184 . . . . . . . . . . . . . . . . . 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.  ( fi `  ( { X }  u.  ran  ( k  e.  A ,  u  e.  ( F `  k )  |->  ( `' ( w  e.  X  |->  ( w `
 k ) )
" u ) ) ) ) )
212125, 211syl5eqel 2367 . . . . . . . . . . . . . . . . 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
) ) }  =/=  (/) )  ->  |^|_ 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 ) ) ) ) )
213 elssuni 3855 . . . . . . . . . . . . . . . . 17  |-  ( |^|_ 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 ) ) ) ) )
214212, 213syl 15 . . . . . . . . . . . . . . . 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 ) ) 
C_  U. ( fi `  ( { X }  u.  ran  ( k  e.  A ,  u  e.  ( F `  k )  |->  ( `' ( w  e.  X  |->  ( w `
 k ) )
" u ) ) ) ) )
215 fiuni 7181 . . . . . . . . . . . . . . . . . . 19  |-  ( ( { 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 ) ) ) ) )
216146, 215syl 15 . . . . . . . . . . . . . . . . . 18  |-  ( ( 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 ) ) ) ) )
217120pwid 3638 . . . . . . . . . . . . . . . . . . . . . . 23  |-  X  e. 
~P X
218217a1i 10 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( A  e.  V  /\  F : A --> Top )  ->  X  e.  ~P X
)
219218snssd 3760 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( A  e.  V  /\  F : A --> Top )  ->  { X }  C_  ~P X )
2201ptuni2 17271 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( A  e.  V  /\  F : A --> Top )  -> 
X_ n  e.  A  U. ( F `  n
)  =  U. B
)
22113, 220syl5eq 2327 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( A  e.  V  /\  F : A --> Top )  ->  X  =  U. B
)
222 eqimss2 3231 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( X  =  U. B  ->  U. B  C_  X )
223221, 222syl 15 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( A  e.  V  /\  F : A --> Top )  ->  U. B  C_  X
)
224 sspwuni 3987 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( B 
C_  ~P X  <->  U. B  C_  X )
225223, 224sylibr 203 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( A  e.  V  /\  F : A --> Top )  ->  B  C_  ~P X
)
226141, 225sstrd 3189 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( A  e.  V  /\  F : A --> Top )  ->  ran  ( k  e.  A ,  u  e.  ( F `  k
)  |->  ( `' ( w  e.  X  |->  ( w `  k ) ) " u ) )  C_  ~P X
)
227219, 226unssd 3351 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 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 )
228 sspwuni 3987 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( { 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
)
229227, 228sylib 188 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 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
)
230 elssuni 3855 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 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 ) ) ) )
231152, 230ax-mp 8 . . . . . . . . . . . . . . . . . . . 20  |-  X  C_  U. ( { X }  u.  ran  ( k  e.  A ,  u  e.  ( F `  k
)  |->  ( `' ( w  e.  X  |->  ( w `  k ) ) " u ) ) )
232231a1i 10 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 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 ) ) ) )
233229, 232eqssd 3196 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  e.  V  /\  F : A --> Top )  ->  U. ( { X }  u.  ran  ( k  e.  A ,  u  e.  ( F `  k
)  |->  ( `' ( w  e.  X  |->  ( w `  k ) ) " u ) ) )  =  X )
234216, 233eqtr3d 2317 . . . . . . . . . . . . . . . . 17  |-  ( ( 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 )
235234ad3antrrr 710 . . . . . . . . . . . . . . . 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
) ) }  =/=  (/) )  ->  U. ( fi `  ( { X }  u.  ran  ( k  e.  A ,  u  e.  ( F `  k
)  |->  ( `' ( w  e.  X  |->  ( w `  k ) ) " u ) ) ) )  =  X )
236214, 235sseqtrd 3214 . . . . . . . . . . . . . . 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_  X )
237236, 56sylib 188 . . . . . . . . . . . . . 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
) ) }  =/=  (/) )  ->  ( 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 ) ) )
238237, 212eqeltrd 2357 . . . . . . . . . . . . 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 ) ) )  e.  ( fi `  ( { X }  u.  ran  ( k  e.  A ,  u  e.  ( F `  k )  |->  ( `' ( w  e.  X  |->  ( w `
 k ) )
" u ) ) ) ) )
239156, 238pm2.61dane 2524 . . . . . . . . . . . 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 ) ) )  ->  ( 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 ) ) ) ) )
240114, 239eqeltrd 2357 . . . . . . . . . . 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 )  e.  ( fi `  ( { X }  u.  ran  ( k  e.  A ,  u  e.  ( F `  k )  |->  ( `' ( w  e.  X  |->  ( w `
 k ) )
" u ) ) ) ) )
241240expr 598 . . . . . . . . . 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.  (