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

Theorem ptbasfi 17292
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 17283 . . . 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 3301 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( A  i^i  m )  =  (/)  ->  ( A 
\  ( A  i^i  m ) )  =  ( A  \  (/) ) )
6 difin 3419 . . . . . . . . . . . . . . . . . . . 20  |-  ( A 
\  ( A  i^i  m ) )  =  ( A  \  m
)
7 dif0 3537 . . . . . . . . . . . . . . . . . . . 20  |-  ( A 
\  (/) )  =  A
85, 6, 73eqtr3g 2351 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A  i^i  m )  =  (/)  ->  ( A 
\  m )  =  A )
98raleqdv 2755 . . . . . . . . . . . . . . . . . 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 6846 . . . . . . . . . . . . . . . . 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 5541 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  y  ->  ( F `  n )  =  ( F `  y ) )
1514unieqd 3854 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  y  ->  U. ( F `  n )  =  U. ( F `  y ) )
1615cbvixpv 6850 . . . . . . . . . . . . . . . . 17  |-  X_ n  e.  A  U. ( F `  n )  =  X_ y  e.  A  U. ( F `  y
)
1713, 16eqtri 2316 . . . . . . . . . . . . . . . 16  |-  X  = 
X_ y  e.  A  U. ( F `  y
)
1812, 17syl6eqr 2346 . . . . . . . . . . . . . . 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 3211 . . . . . . . . . . . . . . . . 17  |-  X  C_  _V
21 iineq1 3935 . . . . . . . . . . . . . . . . . 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 3976 . . . . . . . . . . . . . . . . . 18  |-  |^|_ n  e.  (/)  ( `' ( w  e.  X  |->  ( w `  n ) ) " ( h `
 n ) )  =  _V
2321, 22syl6eq 2344 . . . . . . . . . . . . . . . . 17  |-  ( ( A  i^i  m )  =  (/)  ->  |^|_ n  e.  ( A  i^i  m
) ( `' ( w  e.  X  |->  ( w `  n ) ) " ( h `
 n ) )  =  _V )
2420, 23syl5sseqr 3240 . . . . . . . . . . . . . . . 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 3179 . . . . . . . . . . . . . . 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 2331 . . . . . . . . . . . . 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 3402 . . . . . . . . . . . . . . . . . 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 3191 . . . . . . . . . . . . . . . . 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 5541 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  =  n  ->  (
h `  y )  =  ( h `  n ) )
36 fveq2 5541 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  =  n  ->  ( F `  y )  =  ( F `  n ) )
3735, 36eleq12d 2364 . . . . . . . . . . . . . . . . . . 19  |-  ( y  =  n  ->  (
( h `  y
)  e.  ( F `
 y )  <->  ( h `  n )  e.  ( F `  n ) ) )
3837rspcv 2893 . . . . . . . . . . . . . . . . . 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 17282 . . . . . . . . . . . . . . . . 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 3943 . . . . . . . . . . . . . 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 5049 . . . . . . . . . . . . . . . . . . . . 21  |-  ( `' ( w  e.  X  |->  ( w `  n
) ) " (
h `  n )
)  C_  dom  ( w  e.  X  |->  ( w `
 n ) )
46 eqid 2296 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( w  e.  X  |->  ( w `
 n ) )  =  ( w  e.  X  |->  ( w `  n ) )
4746dmmptss 5185 . . . . . . . . . . . . . . . . . . . . 21  |-  dom  (
w  e.  X  |->  ( w `  n ) )  C_  X
4845, 47sstri 3201 . . . . . . . . . . . . . . . . . . . 20  |-  ( `' ( w  e.  X  |->  ( w `  n
) ) " (
h `  n )
)  C_  X
4948, 17sseqtri 3223 . . . . . . . . . . . . . . . . . . 19  |-  ( `' ( w  e.  X  |->  ( w `  n
) ) " (
h `  n )
)  C_  X_ y  e.  A  U. ( F `
 y )
5049rgenw 2623 . . . . . . . . . . . . . . . . . 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 3556 . . . . . . . . . . . . . . . . . 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 3969 . . . . . . . . . . . . . . . . 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 3238 . . . . . . . . . . . . . . 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 3386 . . . . . . . . . . . . . . 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 3250 . . . . . . . . . . . . . . . . . . 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 3871 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( h `  y )  e.  ( F `  y )  ->  (
h `  y )  C_ 
U. ( F `  y ) )
62 iffalse 3585 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( -.  y  =  n  ->  if ( y  =  n ,  ( h `  n ) ,  U. ( F `  y ) )  =  U. ( F `  y )
)
6362sseq2d 3219 . . . . . . . . . . . . . . . . . . . . . . . . 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 3210 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( h `
 y )  C_  ( h `  y
)
66 iftrue 3584 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( y  =  n  ->  if ( y  =  n ,  ( h `  n ) ,  U. ( F `  y ) )  =  ( h `
 n ) )
6766, 35eqtr4d 2331 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  =  n  ->  if ( y  =  n ,  ( h `  n ) ,  U. ( F `  y ) )  =  ( h `
 y ) )
6865, 67syl5sseqr 3240 . . . . . . . . . . . . . . . . . . . . . . . 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 2640 . . . . . . . . . . . . . . . . . . . . . 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 3968 . . . . . . . . . . . . . . . . . . . . . 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 2299 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( n  =  y  ->  if ( y  =  n ,  ( h `  n ) ,  U. ( F `  y ) )  =  ( h `
 n ) )
75 fveq2 5541 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( n  =  y  ->  (
h `  n )  =  ( h `  y ) )
7674, 75eqtrd 2328 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( n  =  y  ->  if ( y  =  n ,  ( h `  n ) ,  U. ( F `  y ) )  =  ( h `
 y ) )
7776sseq1d 3218 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( n  =  y  ->  ( if ( y  =  n ,  ( h `  n ) ,  U. ( F `  y ) )  C_  ( h `  y )  <->  ( h `  y )  C_  (
h `  y )
) )
7877rspcev 2897 . . . . . . . . . . . . . . . . . . . . . . 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 3969 . . . . . . . . . . . . . . . . . . . . . 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 3209 . . . . . . . . . . . . . . . . . . 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 2630 . . . . . . . . . . . . . . . . . 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 3312 . . . . . . . . . . . . . . . . . . . . . . . . 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 3403 . . . . . . . . . . . . . . . . . . . . . . . . . 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 3191 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( A  i^i  m )  =/=  (/)  /\  y  e.  ( A  \  m
) )  /\  n  e.  ( A  i^i  m
) )  ->  n  e.  m )
91 eleq1 2356 . . . . . . . . . . . . . . . . . . . . . . . . 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 3943 . . . . . . . . . . . . . . . . . . . . 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 3930 . . . . . . . . . . . . . . . . . . . . . 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 2329 . . . . . . . . . . . . . . . . . . . 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 2302 . . . . . . . . . . . . . . . . . . . 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 2634 . . . . . . . . . . . . . . . . . 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 3545 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A  i^i  m )  u.  ( A  \  m ) )  =  A
104103raleqi 2753 . . . . . . . . . . . . . . . . . 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 3369 . . . . . . . . . . . . . . . . . 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 6846 . . . . . . . . . . . . . . . 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 6858 . . . . . . . . . . . . . . . 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 2328 . . . . . . . . . . . . . 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 2339 . . . . . . . . . . . . 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 2537 . . . . . . . . . . . 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 6856 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( A. n  e.  A  U. ( F `  n )  e.  _V  ->  X_ n  e.  A  U. ( F `  n )  e.  _V )
116 fvex 5555 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( F `
 n )  e. 
_V
117116uniex 4532 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  U. ( F `  n )  e.  _V
118117a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( n  e.  A  ->  U. ( F `  n )  e.  _V )
119115, 118mprg 2625 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  X_ n  e.  A  U. ( F `  n )  e.  _V
12013, 119eqeltri 2366 . . . . . . . . . . . . . . . . . . . . . . 23  |-  X  e. 
_V
121120mptex 5762 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( w  e.  X  |->  ( w `
 n ) )  e.  _V
122121cnvex 5225 . . . . . . . . . . . . . . . . . . . . 21  |-  `' ( w  e.  X  |->  ( w `  n ) )  e.  _V
123 imaexg 5042 . . . . . . . . . . . . . . . . . . . . 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 3954 . . . . . . . . . . . . . . . . . . 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 3881 . . . . . . . . . . . . . . . . . . 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 2340 . . . . . . . . . . . . . . . . . 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 3892 . . . . . . . . . . . . . . . . . 18  |-  |^| (/)  =  _V
129127, 128syl6eq 2344 . . . . . . . . . . . . . . . . 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 3383 . . . . . . . . . . . . . . . 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 3494 . . . . . . . . . . . . . . . 16  |-  ( X  i^i  _V )  =  X
132130, 131syl6eq 2344 . . . . . . . . . . . . . . 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 4232 . . . . . . . . . . . . . . . . . . 19  |-  { X }  e.  _V
1351, 13ptpjpre2 17291 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( A  e.  V  /\  F : A --> Top )  /\  ( k  e.  A  /\  u  e.  ( F `  k )
) )  ->  ( `' ( w  e.  X  |->  ( w `  k ) ) "
u )  e.  B
)
136135ralrimivva 2648 . . . . . . . . . . . . . . . . . . . . . 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 2296 . . . . . . . . . . . . . . . . . . . . . . 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 6206 . . . . . . . . . . . . . . . . . . . . . 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 5411 . . . . . . . . . . . . . . . . . . . . 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 17290 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( A  e.  V  /\  F : A --> Top )  ->  B  e.  TopBases )
143 ssexg 4176 . . . . . . . . . . . . . . . . . . . 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 4537 . . . . . . . . . . . . . . . . . . 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 7188 . . . . . . . . . . . . . . . . . 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 3351 . . . . . . . . . . . . . . . . . 18  |-  { X }  C_  ( { X }  u.  ran  ( k  e.  A ,  u  e.  ( F `  k
)  |->  ( `' ( w  e.  X  |->  ( w `  k ) ) " u ) ) )
151120snss 3761 . . . . . . . . . . . . . . . . . 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 3194 . . . . . . . . . . . . . . 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 2370 . . . . . . . . . . . . 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 1609 . . . . . . . . . . . . . . . . . . . . . . 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 2432 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  F/_ n A
160 nfcv 2432 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  F/_ n
( F `  k
)
161 nfixp1 6852 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  F/_ n X_ n  e.  A  U. ( F `  n )
16213, 161nfcxfr 2429 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  F/_ n X
163 nfcv 2432 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  F/_ n
( w `  k
)
164162, 163nfmpt 4124 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  F/_ n
( w  e.  X  |->  ( w `  k
) )
165164nfcnv 4876 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  F/_ n `' ( w  e.  X  |->  ( w `  k ) )
166 nfcv 2432 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  F/_ n u
167165, 166nfima 5036 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  F/_ n
( `' ( w  e.  X  |->  ( w `
 k ) )
" u )
168159, 160, 167nfmpt2 5932 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  F/_ n
( k  e.  A ,  u  e.  ( F `  k )  |->  ( `' ( w  e.  X  |->  ( w `
 k ) )
" u ) )
169168nfrn 4937 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  F/_ n ran  ( k  e.  A ,  u  e.  ( F `  k )  |->  ( `' ( w  e.  X  |->  ( w `
 k ) )
" u ) )
170169nfcri 2426 . . . . . . . . . . . . . . . . . . . . . . 23  |-  F/ n  z  e.  ran  ( k  e.  A ,  u  e.  ( F `  k
)  |->  ( `' ( w  e.  X  |->  ( w `  k ) ) " u ) )
171 df-ov 5877 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5541 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( k  =  n  ->  (
w `  k )  =  ( w `  n ) )
174173mpteq2dv 4123 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( k  =  n  ->  (
w  e.  X  |->  ( w `  k ) )  =  ( w  e.  X  |->  ( w `
 n ) ) )
175174cnveqd 4873 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( k  =  n  ->  `' ( w  e.  X  |->  ( w `  k
) )  =  `' ( w  e.  X  |->  ( w `  n
) ) )
176175imaeq1d 5027 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( k  =  n  ->  ( `' ( w  e.  X  |->  ( w `  k ) ) "
u )  =  ( `' ( w  e.  X  |->  ( w `  n ) ) "
u ) )
177 imaeq2 5024 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( u  =  ( h `  n )  ->  ( `' ( w  e.  X  |->  ( w `  n ) ) "
u )  =  ( `' ( w  e.  X  |->  ( w `  n ) ) "
( h `  n
) ) )
178176, 177sylan9eq 2348 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( k  =  n  /\  u  =  ( h `  n ) )  -> 
( `' ( w  e.  X  |->  ( w `
 k ) )
" u )  =  ( `' ( w  e.  X  |->  ( w `
 n ) )
" ( h `  n ) ) )
179 fveq2 5541 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( k  =  n  ->  ( F `  k )  =  ( F `  n ) )
180178, 179, 137ovmpt2x 5992 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2342 . . . . . . . . . . . . . . . . . . . . . . . . . 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 5405 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4756 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3664 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( n  =  k  ->  { n }  =  { k } )
189 fveq2 5541 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( n  =  k  ->  ( F `  n )  =  ( F `  k ) )
190188, 189xpeq12d 4730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( n  =  k  ->  ( { n }  X.  ( F `  n ) )  =  ( { k }  X.  ( F `  k )
) )
191190cbviunv 3957 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  U_ n  e.  A  ( {
n }  X.  ( F `  n )
)  =  U_ k  e.  A  ( {
k }  X.  ( F `  k )
)
192187, 191syl6eleq 2386 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5678 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2371 . . . . . . . . . . . . . . . . . . . . . . . . 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 2356 . . . . . . . . . . . . . . . . . . . . . . . . 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 2677 . . . . . . . . . . . . . . . . . . . . . 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 3260 . . . . . . . . . . . . . . . . . . . . 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 3352 . . . . . . . . . . . . . . . . . . . . 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 3204 . . . . . . . . . . . . . . . . . . . 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 7099 . . . . . . . . . . . . . . . . . . . . 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 7172 . . . . . . . . . . . . . . . . . . . 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 7185 . . . . . . . . . . . . . . . . . . 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 2380 . . . . . . . . . . . . . . . . 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 3871 . . . . . . . . . . . . . . . . 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 7197 . . . . . . . . . . . . . . . . . . 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 3651 . . . . . . . . . . . . . . . . . . . . . . 23  |-  X  e. 
~P X
218217a1i 10 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( A  e.  V  /\  F : A --> Top )  ->  X  e.  ~P X
)
219218snssd 3776 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( A  e.  V  /\  F : A --> Top )  ->  { X }  C_  ~P X )
2201ptuni2 17287 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( A  e.  V  /\  F : A --> Top )  -> 
X_ n  e.  A  U. ( F `  n
)  =  U. B
)
22113, 220syl5eq 2340 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( A  e.  V  /\  F : A --> Top )  ->  X  =  U. B
)
222 eqimss2 3244 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( X  =  U. B  ->  U. B  C_  X )
223221, 222syl 15 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( A  e.  V  /\  F : A --> Top )  ->  U. B  C_  X
)
224 sspwuni 4003 . . . . . . . . . . . . . . . . . . . . . . 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 3202 . . . . . . . . . . . . . . . . . . . . 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 3364 . . . . . . . . . . . . . . . . . . . 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 4003 . . . . . . . . . . . . . . . . . . . 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 3871 . . . . . . . . . . . . . . . . . . . . 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 3209 . . . . . . . . . . . . . . . . . 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 2330 . . . . . . . . . . . . . . . . 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 3227 . . . . . . . . . . . . . . 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 2370 . . . . . . . . . . . . 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 2537 . . . . . . . . . . . 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 2370 . . . . . . . . . . 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 `