Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  locfinreflem Structured version   Unicode version

Theorem locfinreflem 28497
Description: A locally finite refinement of an open cover induces a locally finite open cover with the original index set. This is fact 2 of http://at.yorku.ca/p/a/c/a/02.pdf , it is expressed by exposing a function  f from the original cover  U, which is taken as the index set. The solution is constructed by building unions, so the same method can be used to prove a similar theorem about closed covers. (Contributed by Thierry Arnoux, 29-Jan-2020.)
Hypotheses
Ref Expression
locfinref.x  |-  X  = 
U. J
locfinref.1  |-  ( ph  ->  U  C_  J )
locfinref.2  |-  ( ph  ->  X  =  U. U
)
locfinref.3  |-  ( ph  ->  V  C_  J )
locfinref.4  |-  ( ph  ->  V Ref U )
locfinref.5  |-  ( ph  ->  V  e.  ( LocFin `  J ) )
Assertion
Ref Expression
locfinreflem  |-  ( ph  ->  E. f ( ( Fun  f  /\  dom  f  C_  U  /\  ran  f  C_  J )  /\  ( ran  f Ref U  /\  ran  f  e.  (
LocFin `  J ) ) ) )
Distinct variable groups:    f, J    U, f    f, V    ph, f
Allowed substitution hint:    X( f)

Proof of Theorem locfinreflem
Dummy variables  g 
j  k  u  v  w  x are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 locfinref.4 . . . 4  |-  ( ph  ->  V Ref U )
2 locfinref.5 . . . . 5  |-  ( ph  ->  V  e.  ( LocFin `  J ) )
3 reff 28496 . . . . 5  |-  ( V  e.  ( LocFin `  J
)  ->  ( V Ref U  <->  ( U. U  C_ 
U. V  /\  E. g ( g : V --> U  /\  A. v  e.  V  v  C_  ( g `  v
) ) ) ) )
42, 3syl 17 . . . 4  |-  ( ph  ->  ( V Ref U  <->  ( U. U  C_  U. V  /\  E. g ( g : V --> U  /\  A. v  e.  V  v 
C_  ( g `  v ) ) ) ) )
51, 4mpbid 213 . . 3  |-  ( ph  ->  ( U. U  C_  U. V  /\  E. g
( g : V --> U  /\  A. v  e.  V  v  C_  (
g `  v )
) ) )
65simprd 464 . 2  |-  ( ph  ->  E. g ( g : V --> U  /\  A. v  e.  V  v 
C_  ( g `  v ) ) )
7 funmpt 5637 . . . . . 6  |-  Fun  (
u  e.  ran  g  |-> 
U. ( `' g
" { u }
) )
87a1i 11 . . . . 5  |-  ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v 
C_  ( g `  v ) )  ->  Fun  ( u  e.  ran  g  |->  U. ( `' g
" { u }
) ) )
9 eqid 2429 . . . . . . 7  |-  ( u  e.  ran  g  |->  U. ( `' g " { u } ) )  =  ( u  e.  ran  g  |->  U. ( `' g " { u } ) )
109dmmptss 5351 . . . . . 6  |-  dom  (
u  e.  ran  g  |-> 
U. ( `' g
" { u }
) )  C_  ran  g
11 frn 5752 . . . . . . 7  |-  ( g : V --> U  ->  ran  g  C_  U )
1211ad2antlr 731 . . . . . 6  |-  ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v 
C_  ( g `  v ) )  ->  ran  g  C_  U )
1310, 12syl5ss 3481 . . . . 5  |-  ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v 
C_  ( g `  v ) )  ->  dom  ( u  e.  ran  g  |->  U. ( `' g
" { u }
) )  C_  U
)
14 locfintop 20458 . . . . . . . . . 10  |-  ( V  e.  ( LocFin `  J
)  ->  J  e.  Top )
152, 14syl 17 . . . . . . . . 9  |-  ( ph  ->  J  e.  Top )
1615ad3antrrr 734 . . . . . . . 8  |-  ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v  C_  (
g `  v )
)  /\  u  e.  ran  g )  ->  J  e.  Top )
17 cnvimass 5208 . . . . . . . . . 10  |-  ( `' g " { u } )  C_  dom  g
18 fdm 5750 . . . . . . . . . . 11  |-  ( g : V --> U  ->  dom  g  =  V
)
1918ad3antlr 735 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v  C_  (
g `  v )
)  /\  u  e.  ran  g )  ->  dom  g  =  V )
2017, 19syl5sseq 3518 . . . . . . . . 9  |-  ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v  C_  (
g `  v )
)  /\  u  e.  ran  g )  ->  ( `' g " {
u } )  C_  V )
21 locfinref.3 . . . . . . . . . 10  |-  ( ph  ->  V  C_  J )
2221ad3antrrr 734 . . . . . . . . 9  |-  ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v  C_  (
g `  v )
)  /\  u  e.  ran  g )  ->  V  C_  J )
2320, 22sstrd 3480 . . . . . . . 8  |-  ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v  C_  (
g `  v )
)  /\  u  e.  ran  g )  ->  ( `' g " {
u } )  C_  J )
24 uniopn 19849 . . . . . . . 8  |-  ( ( J  e.  Top  /\  ( `' g " {
u } )  C_  J )  ->  U. ( `' g " {
u } )  e.  J )
2516, 23, 24syl2anc 665 . . . . . . 7  |-  ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v  C_  (
g `  v )
)  /\  u  e.  ran  g )  ->  U. ( `' g " {
u } )  e.  J )
2625ralrimiva 2846 . . . . . 6  |-  ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v 
C_  ( g `  v ) )  ->  A. u  e.  ran  g U. ( `' g
" { u }
)  e.  J )
279rnmptss 6067 . . . . . 6  |-  ( A. u  e.  ran  g U. ( `' g " {
u } )  e.  J  ->  ran  ( u  e.  ran  g  |->  U. ( `' g " { u } ) )  C_  J )
2826, 27syl 17 . . . . 5  |-  ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v 
C_  ( g `  v ) )  ->  ran  ( u  e.  ran  g  |->  U. ( `' g
" { u }
) )  C_  J
)
29 eqid 2429 . . . . . . . . . 10  |-  U. V  =  U. V
30 eqid 2429 . . . . . . . . . 10  |-  U. U  =  U. U
3129, 30refbas 20447 . . . . . . . . 9  |-  ( V Ref U  ->  U. U  =  U. V )
321, 31syl 17 . . . . . . . 8  |-  ( ph  ->  U. U  =  U. V )
3332ad2antrr 730 . . . . . . 7  |-  ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v 
C_  ( g `  v ) )  ->  U. U  =  U. V )
34 nfv 1754 . . . . . . . . . . . . 13  |-  F/ v ( ph  /\  g : V --> U )
35 nfra1 2813 . . . . . . . . . . . . 13  |-  F/ v A. v  e.  V  v  C_  ( g `  v )
3634, 35nfan 1986 . . . . . . . . . . . 12  |-  F/ v ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v  C_  (
g `  v )
)
37 nfre1 2893 . . . . . . . . . . . 12  |-  F/ v E. v  e.  V  x  e.  v
3836, 37nfan 1986 . . . . . . . . . . 11  |-  F/ v ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v  C_  (
g `  v )
)  /\  E. v  e.  V  x  e.  v )
39 ffn 5746 . . . . . . . . . . . . . . 15  |-  ( g : V --> U  -> 
g  Fn  V )
4039ad4antlr 737 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v  C_  (
g `  v )
)  /\  v  e.  V )  /\  x  e.  v )  ->  g  Fn  V )
41 simplr 760 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v  C_  (
g `  v )
)  /\  v  e.  V )  /\  x  e.  v )  ->  v  e.  V )
42 fnfvelrn 6034 . . . . . . . . . . . . . 14  |-  ( ( g  Fn  V  /\  v  e.  V )  ->  ( g `  v
)  e.  ran  g
)
4340, 41, 42syl2anc 665 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v  C_  (
g `  v )
)  /\  v  e.  V )  /\  x  e.  v )  ->  (
g `  v )  e.  ran  g )
44 ssid 3489 . . . . . . . . . . . . . . 15  |-  v  C_  v
4539ad3antlr 735 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v  C_  (
g `  v )
)  /\  v  e.  V )  ->  g  Fn  V )
46 eqid 2429 . . . . . . . . . . . . . . . . 17  |-  ( g `
 v )  =  ( g `  v
)
47 fniniseg 6018 . . . . . . . . . . . . . . . . . 18  |-  ( g  Fn  V  ->  (
v  e.  ( `' g " { ( g `  v ) } )  <->  ( v  e.  V  /\  (
g `  v )  =  ( g `  v ) ) ) )
4847biimpar 487 . . . . . . . . . . . . . . . . 17  |-  ( ( g  Fn  V  /\  ( v  e.  V  /\  ( g `  v
)  =  ( g `
 v ) ) )  ->  v  e.  ( `' g " {
( g `  v
) } ) )
4946, 48mpanr2 688 . . . . . . . . . . . . . . . 16  |-  ( ( g  Fn  V  /\  v  e.  V )  ->  v  e.  ( `' g " { ( g `  v ) } ) )
5045, 49sylancom 671 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v  C_  (
g `  v )
)  /\  v  e.  V )  ->  v  e.  ( `' g " { ( g `  v ) } ) )
51 ssuni 4244 . . . . . . . . . . . . . . 15  |-  ( ( v  C_  v  /\  v  e.  ( `' g " { ( g `
 v ) } ) )  ->  v  C_ 
U. ( `' g
" { ( g `
 v ) } ) )
5244, 50, 51sylancr 667 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v  C_  (
g `  v )
)  /\  v  e.  V )  ->  v  C_ 
U. ( `' g
" { ( g `
 v ) } ) )
5352sselda 3470 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v  C_  (
g `  v )
)  /\  v  e.  V )  /\  x  e.  v )  ->  x  e.  U. ( `' g
" { ( g `
 v ) } ) )
54 sneq 4012 . . . . . . . . . . . . . . . . 17  |-  ( u  =  ( g `  v )  ->  { u }  =  { (
g `  v ) } )
5554imaeq2d 5188 . . . . . . . . . . . . . . . 16  |-  ( u  =  ( g `  v )  ->  ( `' g " {
u } )  =  ( `' g " { ( g `  v ) } ) )
5655unieqd 4232 . . . . . . . . . . . . . . 15  |-  ( u  =  ( g `  v )  ->  U. ( `' g " {
u } )  = 
U. ( `' g
" { ( g `
 v ) } ) )
5756eleq2d 2499 . . . . . . . . . . . . . 14  |-  ( u  =  ( g `  v )  ->  (
x  e.  U. ( `' g " {
u } )  <->  x  e.  U. ( `' g " { ( g `  v ) } ) ) )
5857rspcev 3188 . . . . . . . . . . . . 13  |-  ( ( ( g `  v
)  e.  ran  g  /\  x  e.  U. ( `' g " {
( g `  v
) } ) )  ->  E. u  e.  ran  g  x  e.  U. ( `' g " {
u } ) )
5943, 53, 58syl2anc 665 . . . . . . . . . . . 12  |-  ( ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v  C_  (
g `  v )
)  /\  v  e.  V )  /\  x  e.  v )  ->  E. u  e.  ran  g  x  e. 
U. ( `' g
" { u }
) )
6059adantllr 723 . . . . . . . . . . 11  |-  ( ( ( ( ( (
ph  /\  g : V
--> U )  /\  A. v  e.  V  v  C_  ( g `  v
) )  /\  E. v  e.  V  x  e.  v )  /\  v  e.  V )  /\  x  e.  v )  ->  E. u  e.  ran  g  x  e. 
U. ( `' g
" { u }
) )
61 simpr 462 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v  C_  (
g `  v )
)  /\  E. v  e.  V  x  e.  v )  ->  E. v  e.  V  x  e.  v )
6238, 60, 61r19.29af 2975 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v  C_  (
g `  v )
)  /\  E. v  e.  V  x  e.  v )  ->  E. u  e.  ran  g  x  e. 
U. ( `' g
" { u }
) )
63 nfv 1754 . . . . . . . . . . . . . 14  |-  F/ v  u  e.  ran  g
6436, 63nfan 1986 . . . . . . . . . . . . 13  |-  F/ v ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v  C_  (
g `  v )
)  /\  u  e.  ran  g )
65 nfv 1754 . . . . . . . . . . . . 13  |-  F/ v  x  e.  U. ( `' g " {
u } )
6664, 65nfan 1986 . . . . . . . . . . . 12  |-  F/ v ( ( ( (
ph  /\  g : V
--> U )  /\  A. v  e.  V  v  C_  ( g `  v
) )  /\  u  e.  ran  g )  /\  x  e.  U. ( `' g " {
u } ) )
6720ad3antrrr 734 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v 
C_  ( g `  v ) )  /\  u  e.  ran  g )  /\  x  e.  U. ( `' g " {
u } ) )  /\  v  e.  ( `' g " {
u } ) )  /\  x  e.  v )  ->  ( `' g " { u }
)  C_  V )
68 simplr 760 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v 
C_  ( g `  v ) )  /\  u  e.  ran  g )  /\  x  e.  U. ( `' g " {
u } ) )  /\  v  e.  ( `' g " {
u } ) )  /\  x  e.  v )  ->  v  e.  ( `' g " {
u } ) )
6967, 68sseldd 3471 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v 
C_  ( g `  v ) )  /\  u  e.  ran  g )  /\  x  e.  U. ( `' g " {
u } ) )  /\  v  e.  ( `' g " {
u } ) )  /\  x  e.  v )  ->  v  e.  V )
70 simpr 462 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v 
C_  ( g `  v ) )  /\  u  e.  ran  g )  /\  x  e.  U. ( `' g " {
u } ) )  /\  v  e.  ( `' g " {
u } ) )  /\  x  e.  v )  ->  x  e.  v )
71 simpr 462 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v  C_  (
g `  v )
)  /\  u  e.  ran  g )  /\  x  e.  U. ( `' g
" { u }
) )  ->  x  e.  U. ( `' g
" { u }
) )
72 eluni2 4226 . . . . . . . . . . . . 13  |-  ( x  e.  U. ( `' g " { u } )  <->  E. v  e.  ( `' g " { u } ) x  e.  v )
7371, 72sylib 199 . . . . . . . . . . . 12  |-  ( ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v  C_  (
g `  v )
)  /\  u  e.  ran  g )  /\  x  e.  U. ( `' g
" { u }
) )  ->  E. v  e.  ( `' g " { u } ) x  e.  v )
7466, 69, 70, 73reximd2a 2902 . . . . . . . . . . 11  |-  ( ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v  C_  (
g `  v )
)  /\  u  e.  ran  g )  /\  x  e.  U. ( `' g
" { u }
) )  ->  E. v  e.  V  x  e.  v )
7574r19.29an 2976 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v  C_  (
g `  v )
)  /\  E. u  e.  ran  g  x  e. 
U. ( `' g
" { u }
) )  ->  E. v  e.  V  x  e.  v )
7662, 75impbida 840 . . . . . . . . 9  |-  ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v 
C_  ( g `  v ) )  -> 
( E. v  e.  V  x  e.  v  <->  E. u  e.  ran  g  x  e.  U. ( `' g " {
u } ) ) )
77 eluni2 4226 . . . . . . . . 9  |-  ( x  e.  U. V  <->  E. v  e.  V  x  e.  v )
78 eliun 4307 . . . . . . . . 9  |-  ( x  e.  U_ u  e. 
ran  g U. ( `' g " {
u } )  <->  E. u  e.  ran  g  x  e. 
U. ( `' g
" { u }
) )
7976, 77, 783bitr4g 291 . . . . . . . 8  |-  ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v 
C_  ( g `  v ) )  -> 
( x  e.  U. V 
<->  x  e.  U_ u  e.  ran  g U. ( `' g " {
u } ) ) )
8079eqrdv 2426 . . . . . . 7  |-  ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v 
C_  ( g `  v ) )  ->  U. V  =  U_ u  e.  ran  g U. ( `' g " {
u } ) )
81 dfiun3g 5107 . . . . . . . 8  |-  ( A. u  e.  ran  g U. ( `' g " {
u } )  e.  J  ->  U_ u  e. 
ran  g U. ( `' g " {
u } )  = 
U. ran  ( u  e.  ran  g  |->  U. ( `' g " {
u } ) ) )
8226, 81syl 17 . . . . . . 7  |-  ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v 
C_  ( g `  v ) )  ->  U_ u  e.  ran  g U. ( `' g
" { u }
)  =  U. ran  ( u  e.  ran  g  |->  U. ( `' g
" { u }
) ) )
8333, 80, 823eqtrd 2474 . . . . . 6  |-  ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v 
C_  ( g `  v ) )  ->  U. U  =  U. ran  ( u  e.  ran  g  |->  U. ( `' g
" { u }
) ) )
8411ad3antlr 735 . . . . . . . . 9  |-  ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v  C_  (
g `  v )
)  /\  w  e.  ran  ( u  e.  ran  g  |->  U. ( `' g
" { u }
) ) )  ->  ran  g  C_  U )
85 vex 3090 . . . . . . . . . . 11  |-  w  e. 
_V
869elrnmpt 5101 . . . . . . . . . . 11  |-  ( w  e.  _V  ->  (
w  e.  ran  (
u  e.  ran  g  |-> 
U. ( `' g
" { u }
) )  <->  E. u  e.  ran  g  w  = 
U. ( `' g
" { u }
) ) )
8785, 86mp1i 13 . . . . . . . . . 10  |-  ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v 
C_  ( g `  v ) )  -> 
( w  e.  ran  ( u  e.  ran  g  |->  U. ( `' g
" { u }
) )  <->  E. u  e.  ran  g  w  = 
U. ( `' g
" { u }
) ) )
8887biimpa 486 . . . . . . . . 9  |-  ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v  C_  (
g `  v )
)  /\  w  e.  ran  ( u  e.  ran  g  |->  U. ( `' g
" { u }
) ) )  ->  E. u  e.  ran  g  w  =  U. ( `' g " {
u } ) )
89 ssrexv 3532 . . . . . . . . 9  |-  ( ran  g  C_  U  ->  ( E. u  e.  ran  g  w  =  U. ( `' g " {
u } )  ->  E. u  e.  U  w  =  U. ( `' g " {
u } ) ) )
9084, 88, 89sylc 62 . . . . . . . 8  |-  ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v  C_  (
g `  v )
)  /\  w  e.  ran  ( u  e.  ran  g  |->  U. ( `' g
" { u }
) ) )  ->  E. u  e.  U  w  =  U. ( `' g " {
u } ) )
91 nfv 1754 . . . . . . . . . 10  |-  F/ u
( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v  C_  (
g `  v )
)
92 nfmpt1 4515 . . . . . . . . . . . 12  |-  F/_ u
( u  e.  ran  g  |->  U. ( `' g
" { u }
) )
9392nfrn 5097 . . . . . . . . . . 11  |-  F/_ u ran  ( u  e.  ran  g  |->  U. ( `' g
" { u }
) )
9493nfcri 2584 . . . . . . . . . 10  |-  F/ u  w  e.  ran  ( u  e.  ran  g  |->  U. ( `' g " { u } ) )
9591, 94nfan 1986 . . . . . . . . 9  |-  F/ u
( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v  C_  (
g `  v )
)  /\  w  e.  ran  ( u  e.  ran  g  |->  U. ( `' g
" { u }
) ) )
96 simpr 462 . . . . . . . . . . 11  |-  ( ( ( ( ( (
ph  /\  g : V
--> U )  /\  A. v  e.  V  v  C_  ( g `  v
) )  /\  w  e.  ran  ( u  e. 
ran  g  |->  U. ( `' g " {
u } ) ) )  /\  u  e.  U )  /\  w  =  U. ( `' g
" { u }
) )  ->  w  =  U. ( `' g
" { u }
) )
97 nfv 1754 . . . . . . . . . . . . . . . 16  |-  F/ v  w  e.  ran  (
u  e.  ran  g  |-> 
U. ( `' g
" { u }
) )
9836, 97nfan 1986 . . . . . . . . . . . . . . 15  |-  F/ v ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v  C_  (
g `  v )
)  /\  w  e.  ran  ( u  e.  ran  g  |->  U. ( `' g
" { u }
) ) )
99 nfv 1754 . . . . . . . . . . . . . . 15  |-  F/ v  u  e.  U
10098, 99nfan 1986 . . . . . . . . . . . . . 14  |-  F/ v ( ( ( (
ph  /\  g : V
--> U )  /\  A. v  e.  V  v  C_  ( g `  v
) )  /\  w  e.  ran  ( u  e. 
ran  g  |->  U. ( `' g " {
u } ) ) )  /\  u  e.  U )
101 nfv 1754 . . . . . . . . . . . . . 14  |-  F/ v  w  =  U. ( `' g " {
u } )
102100, 101nfan 1986 . . . . . . . . . . . . 13  |-  F/ v ( ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v 
C_  ( g `  v ) )  /\  w  e.  ran  ( u  e.  ran  g  |->  U. ( `' g " { u } ) ) )  /\  u  e.  U )  /\  w  =  U. ( `' g
" { u }
) )
103 simp-5r 777 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v 
C_  ( g `  v ) )  /\  w  e.  ran  ( u  e.  ran  g  |->  U. ( `' g " { u } ) ) )  /\  u  e.  U )  /\  w  =  U. ( `' g
" { u }
) )  /\  v  e.  ( `' g " { u } ) )  ->  A. v  e.  V  v  C_  ( g `  v
) )
10439ad5antlr 739 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( (
ph  /\  g : V
--> U )  /\  A. v  e.  V  v  C_  ( g `  v
) )  /\  w  e.  ran  ( u  e. 
ran  g  |->  U. ( `' g " {
u } ) ) )  /\  u  e.  U )  /\  w  =  U. ( `' g
" { u }
) )  ->  g  Fn  V )
105 fniniseg 6018 . . . . . . . . . . . . . . . . . . 19  |-  ( g  Fn  V  ->  (
v  e.  ( `' g " { u } )  <->  ( v  e.  V  /\  (
g `  v )  =  u ) ) )
106104, 105syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( (
ph  /\  g : V
--> U )  /\  A. v  e.  V  v  C_  ( g `  v
) )  /\  w  e.  ran  ( u  e. 
ran  g  |->  U. ( `' g " {
u } ) ) )  /\  u  e.  U )  /\  w  =  U. ( `' g
" { u }
) )  ->  (
v  e.  ( `' g " { u } )  <->  ( v  e.  V  /\  (
g `  v )  =  u ) ) )
107106biimpa 486 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v 
C_  ( g `  v ) )  /\  w  e.  ran  ( u  e.  ran  g  |->  U. ( `' g " { u } ) ) )  /\  u  e.  U )  /\  w  =  U. ( `' g
" { u }
) )  /\  v  e.  ( `' g " { u } ) )  ->  ( v  e.  V  /\  (
g `  v )  =  u ) )
108107simpld 460 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v 
C_  ( g `  v ) )  /\  w  e.  ran  ( u  e.  ran  g  |->  U. ( `' g " { u } ) ) )  /\  u  e.  U )  /\  w  =  U. ( `' g
" { u }
) )  /\  v  e.  ( `' g " { u } ) )  ->  v  e.  V )
109 rspa 2799 . . . . . . . . . . . . . . . 16  |-  ( ( A. v  e.  V  v  C_  ( g `  v )  /\  v  e.  V )  ->  v  C_  ( g `  v
) )
110103, 108, 109syl2anc 665 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v 
C_  ( g `  v ) )  /\  w  e.  ran  ( u  e.  ran  g  |->  U. ( `' g " { u } ) ) )  /\  u  e.  U )  /\  w  =  U. ( `' g
" { u }
) )  /\  v  e.  ( `' g " { u } ) )  ->  v  C_  ( g `  v
) )
111107simprd 464 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v 
C_  ( g `  v ) )  /\  w  e.  ran  ( u  e.  ran  g  |->  U. ( `' g " { u } ) ) )  /\  u  e.  U )  /\  w  =  U. ( `' g
" { u }
) )  /\  v  e.  ( `' g " { u } ) )  ->  ( g `  v )  =  u )
112110, 111sseqtrd 3506 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v 
C_  ( g `  v ) )  /\  w  e.  ran  ( u  e.  ran  g  |->  U. ( `' g " { u } ) ) )  /\  u  e.  U )  /\  w  =  U. ( `' g
" { u }
) )  /\  v  e.  ( `' g " { u } ) )  ->  v  C_  u )
113112ex 435 . . . . . . . . . . . . 13  |-  ( ( ( ( ( (
ph  /\  g : V
--> U )  /\  A. v  e.  V  v  C_  ( g `  v
) )  /\  w  e.  ran  ( u  e. 
ran  g  |->  U. ( `' g " {
u } ) ) )  /\  u  e.  U )  /\  w  =  U. ( `' g
" { u }
) )  ->  (
v  e.  ( `' g " { u } )  ->  v  C_  u ) )
114102, 113ralrimi 2832 . . . . . . . . . . . 12  |-  ( ( ( ( ( (
ph  /\  g : V
--> U )  /\  A. v  e.  V  v  C_  ( g `  v
) )  /\  w  e.  ran  ( u  e. 
ran  g  |->  U. ( `' g " {
u } ) ) )  /\  u  e.  U )  /\  w  =  U. ( `' g
" { u }
) )  ->  A. v  e.  ( `' g " { u } ) v  C_  u )
115 unissb 4253 . . . . . . . . . . . 12  |-  ( U. ( `' g " {
u } )  C_  u 
<-> 
A. v  e.  ( `' g " {
u } ) v 
C_  u )
116114, 115sylibr 215 . . . . . . . . . . 11  |-  ( ( ( ( ( (
ph  /\  g : V
--> U )  /\  A. v  e.  V  v  C_  ( g `  v
) )  /\  w  e.  ran  ( u  e. 
ran  g  |->  U. ( `' g " {
u } ) ) )  /\  u  e.  U )  /\  w  =  U. ( `' g
" { u }
) )  ->  U. ( `' g " {
u } )  C_  u )
11796, 116eqsstrd 3504 . . . . . . . . . 10  |-  ( ( ( ( ( (
ph  /\  g : V
--> U )  /\  A. v  e.  V  v  C_  ( g `  v
) )  /\  w  e.  ran  ( u  e. 
ran  g  |->  U. ( `' g " {
u } ) ) )  /\  u  e.  U )  /\  w  =  U. ( `' g
" { u }
) )  ->  w  C_  u )
118117exp31 607 . . . . . . . . 9  |-  ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v  C_  (
g `  v )
)  /\  w  e.  ran  ( u  e.  ran  g  |->  U. ( `' g
" { u }
) ) )  -> 
( u  e.  U  ->  ( w  =  U. ( `' g " {
u } )  ->  w  C_  u ) ) )
11995, 118reximdai 2901 . . . . . . . 8  |-  ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v  C_  (
g `  v )
)  /\  w  e.  ran  ( u  e.  ran  g  |->  U. ( `' g
" { u }
) ) )  -> 
( E. u  e.  U  w  =  U. ( `' g " {
u } )  ->  E. u  e.  U  w  C_  u ) )
12090, 119mpd 15 . . . . . . 7  |-  ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v  C_  (
g `  v )
)  /\  w  e.  ran  ( u  e.  ran  g  |->  U. ( `' g
" { u }
) ) )  ->  E. u  e.  U  w  C_  u )
121120ralrimiva 2846 . . . . . 6  |-  ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v 
C_  ( g `  v ) )  ->  A. w  e.  ran  ( u  e.  ran  g  |->  U. ( `' g
" { u }
) ) E. u  e.  U  w  C_  u
)
122 vex 3090 . . . . . . . . . 10  |-  g  e. 
_V
123122rnex 6741 . . . . . . . . 9  |-  ran  g  e.  _V
124123mptex 6151 . . . . . . . 8  |-  ( u  e.  ran  g  |->  U. ( `' g " { u } ) )  e.  _V
125 rnexg 6739 . . . . . . . 8  |-  ( ( u  e.  ran  g  |-> 
U. ( `' g
" { u }
) )  e.  _V  ->  ran  ( u  e. 
ran  g  |->  U. ( `' g " {
u } ) )  e.  _V )
126124, 125mp1i 13 . . . . . . 7  |-  ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v 
C_  ( g `  v ) )  ->  ran  ( u  e.  ran  g  |->  U. ( `' g
" { u }
) )  e.  _V )
127 eqid 2429 . . . . . . . 8  |-  U. ran  ( u  e.  ran  g  |->  U. ( `' g
" { u }
) )  =  U. ran  ( u  e.  ran  g  |->  U. ( `' g
" { u }
) )
128127, 30isref 20446 . . . . . . 7  |-  ( ran  ( u  e.  ran  g  |->  U. ( `' g
" { u }
) )  e.  _V  ->  ( ran  ( u  e.  ran  g  |->  U. ( `' g " { u } ) ) Ref U  <->  ( U. U  =  U. ran  (
u  e.  ran  g  |-> 
U. ( `' g
" { u }
) )  /\  A. w  e.  ran  ( u  e.  ran  g  |->  U. ( `' g " { u } ) ) E. u  e.  U  w  C_  u
) ) )
129126, 128syl 17 . . . . . 6  |-  ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v 
C_  ( g `  v ) )  -> 
( ran  ( u  e.  ran  g  |->  U. ( `' g " {
u } ) ) Ref U  <->  ( U. U  =  U. ran  (
u  e.  ran  g  |-> 
U. ( `' g
" { u }
) )  /\  A. w  e.  ran  ( u  e.  ran  g  |->  U. ( `' g " { u } ) ) E. u  e.  U  w  C_  u
) ) )
13083, 121, 129mpbir2and 930 . . . . 5  |-  ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v 
C_  ( g `  v ) )  ->  ran  ( u  e.  ran  g  |->  U. ( `' g
" { u }
) ) Ref U
)
13115ad2antrr 730 . . . . . 6  |-  ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v 
C_  ( g `  v ) )  ->  J  e.  Top )
132 locfinref.2 . . . . . . . 8  |-  ( ph  ->  X  =  U. U
)
133132ad2antrr 730 . . . . . . 7  |-  ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v 
C_  ( g `  v ) )  ->  X  =  U. U )
134133, 83eqtrd 2470 . . . . . 6  |-  ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v 
C_  ( g `  v ) )  ->  X  =  U. ran  (
u  e.  ran  g  |-> 
U. ( `' g
" { u }
) ) )
135 nfv 1754 . . . . . . . . 9  |-  F/ v  x  e.  X
13636, 135nfan 1986 . . . . . . . 8  |-  F/ v ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v  C_  (
g `  v )
)  /\  x  e.  X )
137 simplr 760 . . . . . . . 8  |-  ( ( ( ( ( (
ph  /\  g : V
--> U )  /\  A. v  e.  V  v  C_  ( g `  v
) )  /\  x  e.  X )  /\  v  e.  J )  /\  (
x  e.  v  /\  { j  e.  V  | 
( j  i^i  v
)  =/=  (/) }  e.  Fin ) )  ->  v  e.  J )
138 ffun 5748 . . . . . . . . . . . . . 14  |-  ( g : V --> U  ->  Fun  g )
139138ad6antlr 741 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v 
C_  ( g `  v ) )  /\  x  e.  X )  /\  v  e.  J
)  /\  x  e.  v )  /\  {
j  e.  V  | 
( j  i^i  v
)  =/=  (/) }  e.  Fin )  ->  Fun  g
)
140 imafi 7873 . . . . . . . . . . . . 13  |-  ( ( Fun  g  /\  {
j  e.  V  | 
( j  i^i  v
)  =/=  (/) }  e.  Fin )  ->  ( g
" { j  e.  V  |  ( j  i^i  v )  =/=  (/) } )  e.  Fin )
141139, 140sylancom 671 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v 
C_  ( g `  v ) )  /\  x  e.  X )  /\  v  e.  J
)  /\  x  e.  v )  /\  {
j  e.  V  | 
( j  i^i  v
)  =/=  (/) }  e.  Fin )  ->  ( g
" { j  e.  V  |  ( j  i^i  v )  =/=  (/) } )  e.  Fin )
142 simp3 1007 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v  C_  (
g `  v )
)  /\  x  e.  X )  /\  v  e.  J )  /\  x  e.  v )  /\  {
j  e.  V  | 
( j  i^i  v
)  =/=  (/) }  e.  Fin )  /\  k  e.  ran  g  /\  w  =  ( ( u  e.  ran  g  |->  U. ( `' g " { u } ) ) `  k ) )  ->  w  =  ( ( u  e. 
ran  g  |->  U. ( `' g " {
u } ) ) `
 k ) )
143 sneq 4012 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( u  =  k  ->  { u }  =  { k } )
144143imaeq2d 5188 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( u  =  k  ->  ( `' g " {
u } )  =  ( `' g " { k } ) )
145144unieqd 4232 . . . . . . . . . . . . . . . . . . . . 21  |-  ( u  =  k  ->  U. ( `' g " {
u } )  = 
U. ( `' g
" { k } ) )
146122cnvex 6754 . . . . . . . . . . . . . . . . . . . . . . 23  |-  `' g  e.  _V
147 imaexg 6744 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( `' g  e.  _V  ->  ( `' g " {
k } )  e. 
_V )
148146, 147ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( `' g " { k } )  e.  _V
149148uniex 6601 . . . . . . . . . . . . . . . . . . . . 21  |-  U. ( `' g " {
k } )  e. 
_V
150145, 9, 149fvmpt 5964 . . . . . . . . . . . . . . . . . . . 20  |-  ( k  e.  ran  g  -> 
( ( u  e. 
ran  g  |->  U. ( `' g " {
u } ) ) `
 k )  = 
U. ( `' g
" { k } ) )
1511503ad2ant2 1027 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v  C_  (
g `  v )
)  /\  x  e.  X )  /\  v  e.  J )  /\  x  e.  v )  /\  {
j  e.  V  | 
( j  i^i  v
)  =/=  (/) }  e.  Fin )  /\  k  e.  ran  g  /\  w  =  ( ( u  e.  ran  g  |->  U. ( `' g " { u } ) ) `  k ) )  ->  ( (
u  e.  ran  g  |-> 
U. ( `' g
" { u }
) ) `  k
)  =  U. ( `' g " {
k } ) )
152142, 151eqtrd 2470 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v  C_  (
g `  v )
)  /\  x  e.  X )  /\  v  e.  J )  /\  x  e.  v )  /\  {
j  e.  V  | 
( j  i^i  v
)  =/=  (/) }  e.  Fin )  /\  k  e.  ran  g  /\  w  =  ( ( u  e.  ran  g  |->  U. ( `' g " { u } ) ) `  k ) )  ->  w  =  U. ( `' g " { k } ) )
153152ineq1d 3669 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v  C_  (
g `  v )
)  /\  x  e.  X )  /\  v  e.  J )  /\  x  e.  v )  /\  {
j  e.  V  | 
( j  i^i  v
)  =/=  (/) }  e.  Fin )  /\  k  e.  ran  g  /\  w  =  ( ( u  e.  ran  g  |->  U. ( `' g " { u } ) ) `  k ) )  ->  ( w  i^i  v )  =  ( U. ( `' g
" { k } )  i^i  v ) )
154153neeq1d 2708 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v  C_  (
g `  v )
)  /\  x  e.  X )  /\  v  e.  J )  /\  x  e.  v )  /\  {
j  e.  V  | 
( j  i^i  v
)  =/=  (/) }  e.  Fin )  /\  k  e.  ran  g  /\  w  =  ( ( u  e.  ran  g  |->  U. ( `' g " { u } ) ) `  k ) )  ->  ( (
w  i^i  v )  =/=  (/)  <->  ( U. ( `' g " {
k } )  i^i  v )  =/=  (/) ) )
155123a1i 11 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v 
C_  ( g `  v ) )  /\  x  e.  X )  /\  v  e.  J
)  /\  x  e.  v )  /\  {
j  e.  V  | 
( j  i^i  v
)  =/=  (/) }  e.  Fin )  ->  ran  g  e.  _V )
156 imaexg 6744 . . . . . . . . . . . . . . . . . . . . 21  |-  ( `' g  e.  _V  ->  ( `' g " {
u } )  e. 
_V )
157146, 156ax-mp 5 . . . . . . . . . . . . . . . . . . . 20  |-  ( `' g " { u } )  e.  _V
158157uniex 6601 . . . . . . . . . . . . . . . . . . 19  |-  U. ( `' g " {
u } )  e. 
_V
159158, 9fnmpti 5724 . . . . . . . . . . . . . . . . . 18  |-  ( u  e.  ran  g  |->  U. ( `' g " { u } ) )  Fn  ran  g
160 dffn4 5816 . . . . . . . . . . . . . . . . . 18  |-  ( ( u  e.  ran  g  |-> 
U. ( `' g
" { u }
) )  Fn  ran  g 
<->  ( u  e.  ran  g  |->  U. ( `' g
" { u }
) ) : ran  g -onto-> ran  ( u  e. 
ran  g  |->  U. ( `' g " {
u } ) ) )
161159, 160mpbi 211 . . . . . . . . . . . . . . . . 17  |-  ( u  e.  ran  g  |->  U. ( `' g " { u } ) ) : ran  g -onto-> ran  ( u  e.  ran  g  |->  U. ( `' g
" { u }
) )
162161a1i 11 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v 
C_  ( g `  v ) )  /\  x  e.  X )  /\  v  e.  J
)  /\  x  e.  v )  /\  {
j  e.  V  | 
( j  i^i  v
)  =/=  (/) }  e.  Fin )  ->  ( u  e.  ran  g  |->  U. ( `' g " { u } ) ) : ran  g -onto-> ran  ( u  e.  ran  g  |->  U. ( `' g
" { u }
) ) )
163154, 155, 162rabfodom 27967 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v 
C_  ( g `  v ) )  /\  x  e.  X )  /\  v  e.  J
)  /\  x  e.  v )  /\  {
j  e.  V  | 
( j  i^i  v
)  =/=  (/) }  e.  Fin )  ->  { w  e.  ran  ( u  e. 
ran  g  |->  U. ( `' g " {
u } ) )  |  ( w  i^i  v )  =/=  (/) }  ~<_  { k  e.  ran  g  |  ( U. ( `' g " { k } )  i^i  v
)  =/=  (/) } )
164 sneq 4012 . . . . . . . . . . . . . . . . . . . 20  |-  ( k  =  u  ->  { k }  =  { u } )
165164imaeq2d 5188 . . . . . . . . . . . . . . . . . . 19  |-  ( k  =  u  ->  ( `' g " {
k } )  =  ( `' g " { u } ) )
166165unieqd 4232 . . . . . . . . . . . . . . . . . 18  |-  ( k  =  u  ->  U. ( `' g " {
k } )  = 
U. ( `' g
" { u }
) )
167166ineq1d 3669 . . . . . . . . . . . . . . . . 17  |-  ( k  =  u  ->  ( U. ( `' g " { k } )  i^i  v )  =  ( U. ( `' g " { u } )  i^i  v
) )
168167neeq1d 2708 . . . . . . . . . . . . . . . 16  |-  ( k  =  u  ->  (
( U. ( `' g " { k } )  i^i  v
)  =/=  (/)  <->  ( U. ( `' g " {
u } )  i^i  v )  =/=  (/) ) )
169168cbvrabv 3086 . . . . . . . . . . . . . . 15  |-  { k  e.  ran  g  |  ( U. ( `' g " { k } )  i^i  v
)  =/=  (/) }  =  { u  e.  ran  g  |  ( U. ( `' g " {
u } )  i^i  v )  =/=  (/) }
170163, 169syl6breq 4465 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v 
C_  ( g `  v ) )  /\  x  e.  X )  /\  v  e.  J
)  /\  x  e.  v )  /\  {
j  e.  V  | 
( j  i^i  v
)  =/=  (/) }  e.  Fin )  ->  { w  e.  ran  ( u  e. 
ran  g  |->  U. ( `' g " {
u } ) )  |  ( w  i^i  v )  =/=  (/) }  ~<_  { u  e.  ran  g  |  ( U. ( `' g
" { u }
)  i^i  v )  =/=  (/) } )
171123rabex 4576 . . . . . . . . . . . . . . 15  |-  { u  e.  ran  g  |  E. k  e.  { j  e.  V  |  (
j  i^i  v )  =/=  (/) }  ( g `
 k )  =  u }  e.  _V
172 nfv 1754 . . . . . . . . . . . . . . . . . . . . 21  |-  F/ j ( ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v 
C_  ( g `  v ) )  /\  x  e.  X )  /\  v  e.  J
)  /\  x  e.  v )
173 nfrab1 3016 . . . . . . . . . . . . . . . . . . . . . 22  |-  F/_ j { j  e.  V  |  ( j  i^i  v )  =/=  (/) }
174173nfel1 2607 . . . . . . . . . . . . . . . . . . . . 21  |-  F/ j { j  e.  V  |  ( j  i^i  v )  =/=  (/) }  e.  Fin
175172, 174nfan 1986 . . . . . . . . . . . . . . . . . . . 20  |-  F/ j ( ( ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v  C_  (
g `  v )
)  /\  x  e.  X )  /\  v  e.  J )  /\  x  e.  v )  /\  {
j  e.  V  | 
( j  i^i  v
)  =/=  (/) }  e.  Fin )
176 nfv 1754 . . . . . . . . . . . . . . . . . . . 20  |-  F/ j  u  e.  ran  g
177175, 176nfan 1986 . . . . . . . . . . . . . . . . . . 19  |-  F/ j ( ( ( ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v  C_  (
g `  v )
)  /\  x  e.  X )  /\  v  e.  J )  /\  x  e.  v )  /\  {
j  e.  V  | 
( j  i^i  v
)  =/=  (/) }  e.  Fin )  /\  u  e.  ran  g )
178 nfv 1754 . . . . . . . . . . . . . . . . . . 19  |-  F/ j ( U. ( `' g " { u } )  i^i  v
)  =/=  (/)
179177, 178nfan 1986 . . . . . . . . . . . . . . . . . 18  |-  F/ j ( ( ( ( ( ( ( (
ph  /\  g : V
--> U )  /\  A. v  e.  V  v  C_  ( g `  v
) )  /\  x  e.  X )  /\  v  e.  J )  /\  x  e.  v )  /\  {
j  e.  V  | 
( j  i^i  v
)  =/=  (/) }  e.  Fin )  /\  u  e.  ran  g )  /\  ( U. ( `' g
" { u }
)  i^i  v )  =/=  (/) )
180 nfv 1754 . . . . . . . . . . . . . . . . . . 19  |-  F/ j ( g `  k
)  =  u
181173, 180nfrex 2895 . . . . . . . . . . . . . . . . . 18  |-  F/ j E. k  e.  {
j  e.  V  | 
( j  i^i  v
)  =/=  (/) }  (
g `  k )  =  u
18239ad5antlr 739 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( (
ph  /\  g : V
--> U )  /\  A. v  e.  V  v  C_  ( g `  v
) )  /\  x  e.  X )  /\  v  e.  J )  /\  x  e.  v )  ->  g  Fn  V )
183182ad5antr 738 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ( ( ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v 
C_  ( g `  v ) )  /\  x  e.  X )  /\  v  e.  J
)  /\  x  e.  v )  /\  {
j  e.  V  | 
( j  i^i  v
)  =/=  (/) }  e.  Fin )  /\  u  e.  ran  g )  /\  ( U. ( `' g
" { u }
)  i^i  v )  =/=  (/) )  /\  j  e.  ( `' g " { u } ) )  /\  ( j  i^i  v )  =/=  (/) )  ->  g  Fn  V )
184 simplr 760 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ( ( ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v 
C_  ( g `  v ) )  /\  x  e.  X )  /\  v  e.  J
)  /\  x  e.  v )  /\  {
j  e.  V  | 
( j  i^i  v
)  =/=  (/) }  e.  Fin )  /\  u  e.  ran  g )  /\  ( U. ( `' g
" { u }
)  i^i  v )  =/=  (/) )  /\  j  e.  ( `' g " { u } ) )  /\  ( j  i^i  v )  =/=  (/) )  ->  j  e.  ( `' g " { u } ) )
185 fniniseg 6018 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( g  Fn  V  ->  (
j  e.  ( `' g " { u } )  <->  ( j  e.  V  /\  (
g `  j )  =  u ) ) )
186185biimpa 486 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( g  Fn  V  /\  j  e.  ( `' g " { u }
) )  ->  (
j  e.  V  /\  ( g `  j
)  =  u ) )
187183, 184, 186syl2anc 665 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ( ( ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v 
C_  ( g `  v ) )  /\  x  e.  X )  /\  v  e.  J
)  /\  x  e.  v )  /\  {
j  e.  V  | 
( j  i^i  v
)  =/=  (/) }  e.  Fin )  /\  u  e.  ran  g )  /\  ( U. ( `' g
" { u }
)  i^i  v )  =/=  (/) )  /\  j  e.  ( `' g " { u } ) )  /\  ( j  i^i  v )  =/=  (/) )  ->  ( j  e.  V  /\  (
g `  j )  =  u ) )
188187simpld 460 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ( ( ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v 
C_  ( g `  v ) )  /\  x  e.  X )  /\  v  e.  J
)  /\  x  e.  v )  /\  {
j  e.  V  | 
( j  i^i  v
)  =/=  (/) }  e.  Fin )  /\  u  e.  ran  g )  /\  ( U. ( `' g
" { u }
)  i^i  v )  =/=  (/) )  /\  j  e.  ( `' g " { u } ) )  /\  ( j  i^i  v )  =/=  (/) )  ->  j  e.  V )
189 simpr 462 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ( ( ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v 
C_  ( g `  v ) )  /\  x  e.  X )  /\  v  e.  J
)  /\  x  e.  v )  /\  {
j  e.  V  | 
( j  i^i  v
)  =/=  (/) }  e.  Fin )  /\  u  e.  ran  g )  /\  ( U. ( `' g
" { u }
)  i^i  v )  =/=  (/) )  /\  j  e.  ( `' g " { u } ) )  /\  ( j  i^i  v )  =/=  (/) )  ->  ( j  i^i  v )  =/=  (/) )
190 rabid 3012 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  e.  { j  e.  V  |  ( j  i^i  v )  =/=  (/) }  <->  ( j  e.  V  /\  ( j  i^i  v )  =/=  (/) ) )
191188, 189, 190sylanbrc 668 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ( ( ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v 
C_  ( g `  v ) )  /\  x  e.  X )  /\  v  e.  J
)  /\  x  e.  v )  /\  {
j  e.  V  | 
( j  i^i  v
)  =/=  (/) }  e.  Fin )  /\  u  e.  ran  g )  /\  ( U. ( `' g
" { u }
)  i^i  v )  =/=  (/) )  /\  j  e.  ( `' g " { u } ) )  /\  ( j  i^i  v )  =/=  (/) )  ->  j  e. 
{ j  e.  V  |  ( j  i^i  v )  =/=  (/) } )
192187simprd 464 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ( ( ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v 
C_  ( g `  v ) )  /\  x  e.  X )  /\  v  e.  J
)  /\  x  e.  v )  /\  {
j  e.  V  | 
( j  i^i  v
)  =/=  (/) }  e.  Fin )  /\  u  e.  ran  g )  /\  ( U. ( `' g
" { u }
)  i^i  v )  =/=  (/) )  /\  j  e.  ( `' g " { u } ) )  /\  ( j  i^i  v )  =/=  (/) )  ->  ( g `
 j )  =  u )
193 fveq2 5881 . . . . . . . . . . . . . . . . . . . . 21  |-  ( k  =  j  ->  (
g `  k )  =  ( g `  j ) )
194193eqeq1d 2431 . . . . . . . . . . . . . . . . . . . 20  |-  ( k  =  j  ->  (
( g `  k
)  =  u  <->  ( g `  j )  =  u ) )
195194rspcev 3188 . . . . . . . . . . . . . . . . . . 19  |-  ( ( j  e.  { j  e.  V  |  ( j  i^i  v )  =/=  (/) }  /\  (
g `  j )  =  u )  ->  E. k  e.  { j  e.  V  |  ( j  i^i  v )  =/=  (/) }  (
g `  k )  =  u )
196191, 192, 195syl2anc 665 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v 
C_  ( g `  v ) )  /\  x  e.  X )  /\  v  e.  J
)  /\  x  e.  v )  /\  {
j  e.  V  | 
( j  i^i  v
)  =/=  (/) }  e.  Fin )  /\  u  e.  ran  g )  /\  ( U. ( `' g
" { u }
)  i^i  v )  =/=  (/) )  /\  j  e.  ( `' g " { u } ) )  /\  ( j  i^i  v )  =/=  (/) )  ->  E. k  e.  { j  e.  V  |  ( j  i^i  v )  =/=  (/) }  (
g `  k )  =  u )
197 uniinn0 27993 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( U. ( `' g
" { u }
)  i^i  v )  =/=  (/)  <->  E. j  e.  ( `' g " {
u } ) ( j  i^i  v )  =/=  (/) )
198197biimpi 197 . . . . . . . . . . . . . . . . . . 19  |-  ( ( U. ( `' g
" { u }
)  i^i  v )  =/=  (/)  ->  E. j  e.  ( `' g " { u } ) ( j  i^i  v
)  =/=  (/) )
199198adantl 467 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v  C_  (
g `  v )
)  /\  x  e.  X )  /\  v  e.  J )  /\  x  e.  v )  /\  {
j  e.  V  | 
( j  i^i  v
)  =/=  (/) }  e.  Fin )  /\  u  e.  ran  g )  /\  ( U. ( `' g
" { u }
)  i^i  v )  =/=  (/) )  ->  E. j  e.  ( `' g " { u } ) ( j  i^i  v
)  =/=  (/) )
200179, 181, 196, 199r19.29af2 2973 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v  C_  (
g `  v )
)  /\  x  e.  X )  /\  v  e.  J )  /\  x  e.  v )  /\  {
j  e.  V  | 
( j  i^i  v
)  =/=  (/) }  e.  Fin )  /\  u  e.  ran  g )  /\  ( U. ( `' g
" { u }
)  i^i  v )  =/=  (/) )  ->  E. k  e.  { j  e.  V  |  ( j  i^i  v )  =/=  (/) }  (
g `  k )  =  u )
201200ex 435 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v  C_  (
g `  v )
)  /\  x  e.  X )  /\  v  e.  J )  /\  x  e.  v )  /\  {
j  e.  V  | 
( j  i^i  v
)  =/=  (/) }  e.  Fin )  /\  u  e.  ran  g )  -> 
( ( U. ( `' g " {
u } )  i^i  v )  =/=  (/)  ->  E. k  e.  { j  e.  V  |  ( j  i^i  v )  =/=  (/) }  (
g `  k )  =  u ) )
202201ss2rabdv 3548 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v 
C_  ( g `  v ) )  /\  x  e.  X )  /\  v  e.  J
)  /\  x  e.  v )  /\  {
j  e.  V  | 
( j  i^i  v
)  =/=  (/) }  e.  Fin )  ->  { u  e.  ran  g  |  ( U. ( `' g
" { u }
)  i^i  v )  =/=  (/) }  C_  { u  e.  ran  g  |  E. k  e.  { j  e.  V  |  (
j  i^i  v )  =/=  (/) }  ( g `
 k )  =  u } )
203 ssdomg 7622 . . . . . . . . . . . . . . 15  |-  ( { u  e.  ran  g  |  E. k  e.  {
j  e.  V  | 
( j  i^i  v
)  =/=  (/) }  (
g `  k )  =  u }  e.  _V  ->  ( { u  e. 
ran  g  |  ( U. ( `' g
" { u }
)  i^i  v )  =/=  (/) }  C_  { u  e.  ran  g  |  E. k  e.  { j  e.  V  |  (
j  i^i  v )  =/=  (/) }  ( g `
 k )  =  u }  ->  { u  e.  ran  g  |  ( U. ( `' g
" { u }
)  i^i  v )  =/=  (/) }  ~<_  { u  e.  ran  g  |  E. k  e.  { j  e.  V  |  (
j  i^i  v )  =/=  (/) }  ( g `
 k )  =  u } ) )
204171, 202, 203mpsyl 65 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v 
C_  ( g `  v ) )  /\  x  e.  X )  /\  v  e.  J
)  /\  x  e.  v )  /\  {
j  e.  V  | 
( j  i^i  v
)  =/=  (/) }  e.  Fin )  ->  { u  e.  ran  g  |  ( U. ( `' g
" { u }
)  i^i  v )  =/=  (/) }  ~<_  { u  e.  ran  g  |  E. k  e.  { j  e.  V  |  (
j  i^i  v )  =/=  (/) }  ( g `
 k )  =  u } )
205 domtr 7629 . . . . . . . . . . . . . 14  |-  ( ( { w  e.  ran  ( u  e.  ran  g  |->  U. ( `' g
" { u }
) )  |  ( w  i^i  v )  =/=  (/) }  ~<_  { u  e.  ran  g  |  ( U. ( `' g
" { u }
)  i^i  v )  =/=  (/) }  /\  {
u  e.  ran  g  |  ( U. ( `' g " {
u } )  i^i  v )  =/=  (/) }  ~<_  { u  e.  ran  g  |  E. k  e.  { j  e.  V  |  (
j  i^i  v )  =/=  (/) }  ( g `
 k )  =  u } )  ->  { w  e.  ran  ( u  e.  ran  g  |->  U. ( `' g
" { u }
) )  |  ( w  i^i  v )  =/=  (/) }  ~<_  { u  e.  ran  g  |  E. k  e.  { j  e.  V  |  (
j  i^i  v )  =/=  (/) }  ( g `
 k )  =  u } )
206170, 204, 205syl2anc 665 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v 
C_  ( g `  v ) )  /\  x  e.  X )  /\  v  e.  J
)  /\  x  e.  v )  /\  {
j  e.  V  | 
( j  i^i  v
)  =/=  (/) }  e.  Fin )  ->  { w  e.  ran  ( u  e. 
ran  g  |->  U. ( `' g " {
u } ) )  |  ( w  i^i  v )  =/=  (/) }  ~<_  { u  e.  ran  g  |  E. k  e.  { j  e.  V  |  (
j  i^i  v )  =/=  (/) }  ( g `
 k )  =  u } )
207182adantr 466 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v 
C_  ( g `  v ) )  /\  x  e.  X )  /\  v  e.  J
)  /\  x  e.  v )  /\  {
j  e.  V  | 
( j  i^i  v
)  =/=  (/) }  e.  Fin )  ->  g  Fn  V )
208 dffn3 5753 . . . . . . . . . . . . . . 15  |-  ( g  Fn  V  <->  g : V
--> ran  g )
209208biimpi 197 . . . . . . . . . . . . . 14  |-  ( g  Fn  V  ->  g : V --> ran  g )
210 ssrab2 3552 . . . . . . . . . . . . . . 15  |-  { j  e.  V  |  ( j  i^i  v )  =/=  (/) }  C_  V
211 fimarab 28075 . . . . . . . . . . . . . . 15  |-  ( ( g : V --> ran  g  /\  { j  e.  V  |  ( j  i^i  v )  =/=  (/) }  C_  V )  ->  (
g " { j  e.  V  |  ( j  i^i  v )  =/=  (/) } )  =  { u  e.  ran  g  |  E. k  e.  { j  e.  V  |  ( j  i^i  v )  =/=  (/) }  (
g `  k )  =  u } )
212210, 211mpan2 675 . . . . . . . . . . . . . 14  |-  ( g : V --> ran  g  ->  ( g " {
j  e.  V  | 
( j  i^i  v
)  =/=  (/) } )  =  { u  e. 
ran  g  |  E. k  e.  { j  e.  V  |  (
j  i^i  v )  =/=  (/) }  ( g `
 k )  =  u } )
213207, 209, 2123syl 18 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v 
C_  ( g `  v ) )  /\  x  e.  X )  /\  v  e.  J
)  /\  x  e.  v )  /\  {
j  e.  V  | 
( j  i^i  v
)  =/=  (/) }  e.  Fin )  ->  ( g
" { j  e.  V  |  ( j  i^i  v )  =/=  (/) } )  =  {
u  e.  ran  g  |  E. k  e.  {
j  e.  V  | 
( j  i^i  v
)  =/=  (/) }  (
g `  k )  =  u } )
214206, 213breqtrrd 4452 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v 
C_  ( g `  v ) )  /\  x  e.  X )  /\  v  e.  J
)  /\  x  e.  v )  /\  {
j  e.  V  | 
( j  i^i  v
)  =/=  (/) }  e.  Fin )  ->  { w  e.  ran  ( u  e. 
ran  g  |->  U. ( `' g " {
u } ) )  |  ( w  i^i  v )  =/=  (/) }  ~<_  ( g
" { j  e.  V  |  ( j  i^i  v )  =/=  (/) } ) )
215 domfi 7799 . . . . . . . . . . . 12  |-  ( ( ( g " {
j  e.  V  | 
( j  i^i  v
)  =/=  (/) } )  e.  Fin  /\  {
w  e.  ran  (
u  e.  ran  g  |-> 
U. ( `' g
" { u }
) )  |  ( w  i^i  v )  =/=  (/) }  ~<_  ( g
" { j  e.  V  |  ( j  i^i  v )  =/=  (/) } ) )  ->  { w  e.  ran  ( u  e.  ran  g  |->  U. ( `' g
" { u }
) )  |  ( w  i^i  v )  =/=  (/) }  e.  Fin )
216141, 214, 215syl2anc 665 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v 
C_  ( g `  v ) )  /\  x  e.  X )  /\  v  e.  J
)  /\  x  e.  v )  /\  {
j  e.  V  | 
( j  i^i  v
)  =/=  (/) }  e.  Fin )  ->  { w  e.  ran  ( u  e. 
ran  g  |->  U. ( `' g " {
u } ) )  |  ( w  i^i  v )  =/=  (/) }  e.  Fin )
217216ex 435 . . . . . . . . . 10  |-  ( ( ( ( ( (
ph  /\  g : V
--> U )  /\  A. v  e.  V  v  C_  ( g `  v
) )  /\  x  e.  X )  /\  v  e.  J )  /\  x  e.  v )  ->  ( { j  e.  V  |  ( j  i^i  v )  =/=  (/) }  e.  Fin  ->  { w  e. 
ran  ( u  e. 
ran  g  |->  U. ( `' g " {
u } ) )  |  ( w  i^i  v )  =/=  (/) }  e.  Fin ) )
218217imdistanda 697 . . . . . . . . 9  |-  ( ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v  C_  (
g `  v )
)  /\  x  e.  X )  /\  v  e.  J )  ->  (
( x  e.  v  /\  { j  e.  V  |  ( j  i^i  v )  =/=  (/) }  e.  Fin )  ->  ( x  e.  v  /\  { w  e. 
ran  ( u  e. 
ran  g  |->  U. ( `' g " {
u } ) )  |  ( w  i^i  v )  =/=  (/) }  e.  Fin ) ) )
219218imp 430 . . . . . . . 8  |-  ( ( ( ( ( (
ph  /\  g : V
--> U )  /\  A. v  e.  V  v  C_  ( g `  v
) )  /\  x  e.  X )  /\  v  e.  J )  /\  (
x  e.  v  /\  { j  e.  V  | 
( j  i^i  v
)  =/=  (/) }  e.  Fin ) )  ->  (
x  e.  v  /\  { w  e.  ran  (
u  e.  ran  g  |-> 
U. ( `' g
" { u }
) )  |  ( w  i^i  v )  =/=  (/) }  e.  Fin ) )
220 simplll 766 . . . . . . . . 9  |-  ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v  C_  (
g `  v )
)  /\  x  e.  X )  ->  ph )
221 locfinref.x . . . . . . . . . . . . 13  |-  X  = 
U. J
222221, 29islocfin 20454 . . . . . . . . . . . 12  |-  ( V  e.  ( LocFin `  J
)  <->  ( J  e. 
Top  /\  X  =  U. V  /\  A. x  e.  X  E. v  e.  J  ( x  e.  v  /\  { j  e.  V  |  ( j  i^i  v )  =/=  (/) }  e.  Fin ) ) )
2232, 222sylib 199 . . . . . . . . . . 11  |-  ( ph  ->  ( J  e.  Top  /\  X  =  U. V  /\  A. x  e.  X  E. v  e.  J  ( x  e.  v  /\  { j  e.  V  |  ( j  i^i  v )  =/=  (/) }  e.  Fin ) ) )
224223simp3d 1019 . . . . . . . . . 10  |-  ( ph  ->  A. x  e.  X  E. v  e.  J  ( x  e.  v  /\  { j  e.  V  |  ( j  i^i  v )  =/=  (/) }  e.  Fin ) )
225224r19.21bi 2801 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  X )  ->  E. v  e.  J  ( x  e.  v  /\  { j  e.  V  |  ( j  i^i  v )  =/=  (/) }  e.  Fin ) )
226220, 225sylancom 671 . . . . . . . 8  |-  ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v  C_  (
g `  v )
)  /\  x  e.  X )  ->  E. v  e.  J  ( x  e.  v  /\  { j  e.  V  |  ( j  i^i  v )  =/=  (/) }  e.  Fin ) )
227136, 137, 219, 226reximd2a 2902 . . . . . . 7  |-  ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v  C_  (
g `  v )
)  /\  x  e.  X )  ->  E. v  e.  J  ( x  e.  v  /\  { w  e.  ran  ( u  e. 
ran  g  |->  U. ( `' g " {
u } ) )  |  ( w  i^i  v )  =/=  (/) }  e.  Fin ) )
228227ralrimiva 2846 . . . . . 6  |-  ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v 
C_  ( g `  v ) )  ->  A. x  e.  X  E. v  e.  J  ( x  e.  v  /\  { w  e.  ran  ( u  e.  ran  g  |->  U. ( `' g
" { u }
) )  |  ( w  i^i  v )  =/=  (/) }  e.  Fin ) )
229221, 127islocfin 20454 . . . . . 6  |-  ( ran  ( u  e.  ran  g  |->  U. ( `' g
" { u }
) )  e.  (
LocFin `  J )  <->  ( J  e.  Top  /\  X  = 
U. ran  ( u  e.  ran  g  |->  U. ( `' g " {
u } ) )  /\  A. x  e.  X  E. v  e.  J  ( x  e.  v  /\  { w  e.  ran  ( u  e. 
ran  g  |->  U. ( `' g " {
u } ) )  |  ( w  i^i  v )  =/=  (/) }  e.  Fin ) ) )
230131, 134, 228, 229syl3anbrc 1189 . . . . 5  |-  ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v 
C_  ( g `  v ) )  ->  ran  ( u  e.  ran  g  |->  U. ( `' g
" { u }
) )  e.  (
LocFin `  J ) )
231 funeq 5620 . . . . . . . 8  |-  ( f  =  ( u  e. 
ran  g  |->  U. ( `' g " {
u } ) )  ->  ( Fun  f  <->  Fun  ( u  e.  ran  g  |->  U. ( `' g
" { u }
) ) ) )
232 dmeq 5055 . . . . . . . . 9  |-  ( f  =  ( u  e. 
ran  g  |->  U. ( `' g " {
u } ) )  ->  dom  f  =  dom  ( u  e.  ran  g  |->  U. ( `' g
" { u }
) ) )
233232sseq1d 3497 . . . . . . . 8  |-  ( f  =  ( u  e. 
ran  g  |->  U. ( `' g " {
u } ) )  ->  ( dom  f  C_  U  <->  dom  ( u  e. 
ran  g  |->  U. ( `' g " {
u } ) ) 
C_  U ) )
234 rneq 5080 . . . . . . . . 9  |-  ( f  =  ( u  e. 
ran  g  |->  U. ( `' g " {
u } ) )  ->  ran  f  =  ran  ( u  e.  ran  g  |->  U. ( `' g
" { u }
) ) )
235234sseq1d 3497 . . . . . . . 8  |-  ( f  =  ( u  e. 
ran  g  |->  U. ( `' g " {
u } ) )  ->  ( ran  f  C_  J  <->  ran  ( u  e. 
ran  g  |->  U. ( `' g " {
u } ) ) 
C_  J ) )
236231, 233, 2353anbi123d 1335 . . . . . . 7  |-  ( f  =  ( u  e. 
ran  g  |->  U. ( `' g " {
u } ) )  ->  ( ( Fun  f  /\  dom  f  C_  U  /\  ran  f  C_  J )  <->  ( Fun  ( u  e.  ran  g  |->  U. ( `' g
" { u }
) )  /\  dom  ( u  e.  ran  g  |->  U. ( `' g
" { u }
) )  C_  U  /\  ran  ( u  e. 
ran  g  |->  U. ( `' g " {
u } ) ) 
C_  J ) ) )
237234breq1d 4436 . . . . . . . 8  |-  ( f  =  ( u  e. 
ran  g  |->  U. ( `' g " {
u } ) )  ->  ( ran  f Ref U  <->  ran  ( u  e. 
ran  g  |->  U. ( `' g " {
u } ) ) Ref U ) )
238234eleq1d 2498 . . . . . . . 8  |-  ( f  =  ( u  e. 
ran  g  |->  U. ( `' g " {
u } ) )  ->  ( ran  f  e.  ( LocFin `  J )  <->  ran  ( u  e.  ran  g  |->  U. ( `' g
" { u }
) )  e.  (
LocFin `  J ) ) )
239237, 238anbi12d 715 . . . . . . 7  |-  ( f  =  ( u  e. 
ran  g  |->  U. ( `' g " {
u } ) )  ->  ( ( ran  f Ref U  /\  ran  f  e.  ( LocFin `
 J ) )  <-> 
( ran  ( u  e.  ran  g  |->  U. ( `' g " {
u } ) ) Ref U  /\  ran  ( u  e.  ran  g  |->  U. ( `' g
" { u }
) )  e.  (
LocFin `  J ) ) ) )
240236, 239anbi12d 715 . . . . . 6  |-  ( f  =  ( u  e. 
ran  g  |->  U. ( `' g " {
u } ) )  ->  ( ( ( Fun  f  /\  dom  f  C_  U  /\  ran  f  C_  J )  /\  ( ran  f Ref U  /\  ran  f  e.  (
LocFin `  J ) ) )  <->  ( ( Fun  ( u  e.  ran  g  |->  U. ( `' g
" { u }
) )  /\  dom  ( u  e.  ran  g  |->  U. ( `' g
" { u }
) )  C_  U  /\  ran  ( u  e. 
ran  g  |->  U. ( `' g " {
u } ) ) 
C_  J )  /\  ( ran  ( u  e. 
ran  g  |->  U. ( `' g " {
u } ) ) Ref U  /\  ran  ( u  e.  ran  g  |->  U. ( `' g
" { u }
) )  e.  (
LocFin `  J ) ) ) ) )
241124, 240spcev 3179 . . . . 5  |-  ( ( ( Fun  ( u  e.  ran  g  |->  U. ( `' g " { u } ) )  /\  dom  (
u  e.  ran  g  |-> 
U. ( `' g
" { u }
) )  C_  U  /\  ran  ( u  e. 
ran  g  |->  U. ( `' g " {
u } ) ) 
C_  J )  /\  ( ran  ( u  e. 
ran  g  |->  U. ( `' g " {
u } ) ) Ref U  /\  ran  ( u  e.  ran  g  |->  U. ( `' g
" { u }
) )  e.  (
LocFin `  J ) ) )  ->  E. f
( ( Fun  f  /\  dom  f  C_  U  /\  ran  f  C_  J
)  /\  ( ran  f Ref U  /\  ran  f  e.  ( LocFin `  J ) ) ) )
2428, 13, 28, 130, 230, 241syl32anc 1272 . . . 4  |-  ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v 
C_  ( g `  v ) )  ->  E. f ( ( Fun  f  /\  dom  f  C_  U  /\  ran  f  C_  J )  /\  ( ran  f Ref U  /\  ran  f  e.  ( LocFin `
 J ) ) ) )
243242expl 622 . . 3  |-  ( ph  ->  ( ( g : V --> U  /\  A. v  e.  V  v  C_  ( g `  v
) )  ->  E. f
( ( Fun  f  /\  dom  f  C_  U  /\  ran  f  C_  J
)  /\  ( ran  f Ref U  /\  ran  f  e.  ( LocFin `  J ) ) ) ) )
244243exlimdv 1771 . 2  |-  ( ph  ->  ( E. g ( g : V --> U  /\  A. v  e.  V  v 
C_  ( g `  v ) )  ->  E. f ( ( Fun  f  /\  dom  f  C_  U  /\  ran  f  C_  J )  /\  ( ran  f Ref U  /\  ran  f  e.  ( LocFin `
 J ) ) ) ) )
2456, 244mpd 15 1  |-  ( ph  ->  E. f ( ( Fun  f  /\  dom  f  C_  U  /\  ran  f  C_  J )  /\  ( ran  f Ref U  /\  ran  f  e.  (
LocFin `  J ) ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ wa 370    /\ w3a 982    = wceq 1437   E.wex 1659    e. wcel 1870    =/= wne 2625   A.wral 2782   E.wrex 2783   {crab 2786   _Vcvv 3087    i^i cin 3441    C_ wss 3442   (/)c0 3767   {csn 4002   U.cuni 4222   U_ciun 4302   class class class wbr 4426    |-> cmpt 4484   `'ccnv 4853   dom cdm 4854   ran crn 4855   "cima 4857   Fun wfun 5595    Fn wfn 5596   -->wf 5597   -onto->wfo 5599   ` cfv 5601    ~<_ cdom 7575   Fincfn 7577   Topctop 19839   Refcref 20439   LocFinclocfin 20441
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-8 1872  ax-9 1874  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-rep 4538  ax-sep 4548  ax-nul 4556  ax-pow 4603  ax-pr 4661  ax-un 6597  ax-reg 8107  ax-inf2 8146  ax-ac2 8891
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-eu 2270  df-mo 2271  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-ral 2787  df-rex 2788  df-reu 2789  df-rmo 2790  df-rab 2791  df-v 3089  df-sbc 3306  df-csb 3402  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-pss 3458  df-nul 3768  df-if 3916  df-pw 3987  df-sn 4003  df-pr 4005  df-tp 4007  df-op 4009  df-uni 4223  df-int 4259  df-iun 4304  df-iin 4305  df-br 4427  df-opab 4485  df-mpt 4486  df-tr 4521  df-eprel 4765  df-id 4769  df-po 4775  df-so 4776  df-fr 4813  df-se 4814  df-we 4815  df-xp 4860  df-rel 4861  df-cnv 4862  df-co 4863  df-dm 4864  df-rn 4865  df-res 4866  df-ima 4867  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-isom 5610  df-riota 6267  df-om 6707  df-wrecs 7036  df-recs 7098  df-rdg 7136  df-1o 7190  df-er 7371  df-en 7578  df-dom 7579  df-fin 7581  df-r1 8234  df-rank 8235  df-card 8372  df-ac 8545  df-top 19843  df-ref 20442  df-locfin 20444
This theorem is referenced by:  locfinref  28498
  Copyright terms: Public domain W3C validator