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

Theorem locfinreflem 27997
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 27996 . . . . 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 16 . . . 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 210 . . 3  |-  ( ph  ->  ( U. U  C_  U. V  /\  E. g
( g : V --> U  /\  A. v  e.  V  v  C_  (
g `  v )
) ) )
65simprd 461 . 2  |-  ( ph  ->  E. g ( g : V --> U  /\  A. v  e.  V  v 
C_  ( g `  v ) ) )
7 funmpt 5532 . . . . . 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 2382 . . . . . . 7  |-  ( u  e.  ran  g  |->  U. ( `' g " { u } ) )  =  ( u  e.  ran  g  |->  U. ( `' g " { u } ) )
109dmmptss 5411 . . . . . 6  |-  dom  (
u  e.  ran  g  |-> 
U. ( `' g
" { u }
) )  C_  ran  g
11 frn 5645 . . . . . . 7  |-  ( g : V --> U  ->  ran  g  C_  U )
1211ad2antlr 724 . . . . . 6  |-  ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v 
C_  ( g `  v ) )  ->  ran  g  C_  U )
1310, 12syl5ss 3428 . . . . 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 20107 . . . . . . . . . 10  |-  ( V  e.  ( LocFin `  J
)  ->  J  e.  Top )
152, 14syl 16 . . . . . . . . 9  |-  ( ph  ->  J  e.  Top )
1615ad3antrrr 727 . . . . . . . 8  |-  ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v  C_  (
g `  v )
)  /\  u  e.  ran  g )  ->  J  e.  Top )
17 cnvimass 5269 . . . . . . . . . 10  |-  ( `' g " { u } )  C_  dom  g
18 fdm 5643 . . . . . . . . . . 11  |-  ( g : V --> U  ->  dom  g  =  V
)
1918ad3antlr 728 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v  C_  (
g `  v )
)  /\  u  e.  ran  g )  ->  dom  g  =  V )
2017, 19syl5sseq 3465 . . . . . . . . 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 727 . . . . . . . . 9  |-  ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v  C_  (
g `  v )
)  /\  u  e.  ran  g )  ->  V  C_  J )
2320, 22sstrd 3427 . . . . . . . 8  |-  ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v  C_  (
g `  v )
)  /\  u  e.  ran  g )  ->  ( `' g " {
u } )  C_  J )
24 uniopn 19491 . . . . . . . 8  |-  ( ( J  e.  Top  /\  ( `' g " {
u } )  C_  J )  ->  U. ( `' g " {
u } )  e.  J )
2516, 23, 24syl2anc 659 . . . . . . 7  |-  ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v  C_  (
g `  v )
)  /\  u  e.  ran  g )  ->  U. ( `' g " {
u } )  e.  J )
2625ralrimiva 2796 . . . . . 6  |-  ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v 
C_  ( g `  v ) )  ->  A. u  e.  ran  g U. ( `' g
" { u }
)  e.  J )
279rnmptss 5962 . . . . . 6  |-  ( A. u  e.  ran  g U. ( `' g " {
u } )  e.  J  ->  ran  ( u  e.  ran  g  |->  U. ( `' g " { u } ) )  C_  J )
2826, 27syl 16 . . . . 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 2382 . . . . . . . . . 10  |-  U. V  =  U. V
30 eqid 2382 . . . . . . . . . 10  |-  U. U  =  U. U
3129, 30refbas 20096 . . . . . . . . 9  |-  ( V Ref U  ->  U. U  =  U. V )
321, 31syl 16 . . . . . . . 8  |-  ( ph  ->  U. U  =  U. V )
3332ad2antrr 723 . . . . . . 7  |-  ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v 
C_  ( g `  v ) )  ->  U. U  =  U. V )
34 nfv 1715 . . . . . . . . . . . . 13  |-  F/ v ( ph  /\  g : V --> U )
35 nfra1 2763 . . . . . . . . . . . . 13  |-  F/ v A. v  e.  V  v  C_  ( g `  v )
3634, 35nfan 1936 . . . . . . . . . . . 12  |-  F/ v ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v  C_  (
g `  v )
)
37 nfre1 2843 . . . . . . . . . . . 12  |-  F/ v E. v  e.  V  x  e.  v
3836, 37nfan 1936 . . . . . . . . . . 11  |-  F/ v ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v  C_  (
g `  v )
)  /\  E. v  e.  V  x  e.  v )
39 ffn 5639 . . . . . . . . . . . . . . 15  |-  ( g : V --> U  -> 
g  Fn  V )
4039ad4antlr 730 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v  C_  (
g `  v )
)  /\  v  e.  V )  /\  x  e.  v )  ->  g  Fn  V )
41 simplr 753 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v  C_  (
g `  v )
)  /\  v  e.  V )  /\  x  e.  v )  ->  v  e.  V )
42 fnfvelrn 5930 . . . . . . . . . . . . . 14  |-  ( ( g  Fn  V  /\  v  e.  V )  ->  ( g `  v
)  e.  ran  g
)
4340, 41, 42syl2anc 659 . . . . . . . . . . . . 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 3436 . . . . . . . . . . . . . . 15  |-  v  C_  v
4539ad3antlr 728 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v  C_  (
g `  v )
)  /\  v  e.  V )  ->  g  Fn  V )
46 eqid 2382 . . . . . . . . . . . . . . . . 17  |-  ( g `
 v )  =  ( g `  v
)
47 fniniseg 5910 . . . . . . . . . . . . . . . . . 18  |-  ( g  Fn  V  ->  (
v  e.  ( `' g " { ( g `  v ) } )  <->  ( v  e.  V  /\  (
g `  v )  =  ( g `  v ) ) ) )
4847biimpar 483 . . . . . . . . . . . . . . . . 17  |-  ( ( g  Fn  V  /\  ( v  e.  V  /\  ( g `  v
)  =  ( g `
 v ) ) )  ->  v  e.  ( `' g " {
( g `  v
) } ) )
4946, 48mpanr2 682 . . . . . . . . . . . . . . . 16  |-  ( ( g  Fn  V  /\  v  e.  V )  ->  v  e.  ( `' g " { ( g `  v ) } ) )
5045, 49sylancom 665 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v  C_  (
g `  v )
)  /\  v  e.  V )  ->  v  e.  ( `' g " { ( g `  v ) } ) )
51 ssuni 4185 . . . . . . . . . . . . . . 15  |-  ( ( v  C_  v  /\  v  e.  ( `' g " { ( g `
 v ) } ) )  ->  v  C_ 
U. ( `' g
" { ( g `
 v ) } ) )
5244, 50, 51sylancr 661 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v  C_  (
g `  v )
)  /\  v  e.  V )  ->  v  C_ 
U. ( `' g
" { ( g `
 v ) } ) )
5352sselda 3417 . . . . . . . . . . . . 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 3954 . . . . . . . . . . . . . . . . 17  |-  ( u  =  ( g `  v )  ->  { u }  =  { (
g `  v ) } )
5554imaeq2d 5249 . . . . . . . . . . . . . . . 16  |-  ( u  =  ( g `  v )  ->  ( `' g " {
u } )  =  ( `' g " { ( g `  v ) } ) )
5655unieqd 4173 . . . . . . . . . . . . . . 15  |-  ( u  =  ( g `  v )  ->  U. ( `' g " {
u } )  = 
U. ( `' g
" { ( g `
 v ) } ) )
5756eleq2d 2452 . . . . . . . . . . . . . 14  |-  ( u  =  ( g `  v )  ->  (
x  e.  U. ( `' g " {
u } )  <->  x  e.  U. ( `' g " { ( g `  v ) } ) ) )
5857rspcev 3135 . . . . . . . . . . . . 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 659 . . . . . . . . . . . 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 716 . . . . . . . . . . 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 459 . . . . . . . . . . 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 2922 . . . . . . . . . 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 1715 . . . . . . . . . . . . . 14  |-  F/ v  u  e.  ran  g
6436, 63nfan 1936 . . . . . . . . . . . . 13  |-  F/ v ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v  C_  (
g `  v )
)  /\  u  e.  ran  g )
65 nfv 1715 . . . . . . . . . . . . 13  |-  F/ v  x  e.  U. ( `' g " {
u } )
6664, 65nfan 1936 . . . . . . . . . . . 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 727 . . . . . . . . . . . . 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 753 . . . . . . . . . . . . 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 3418 . . . . . . . . . . . 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 459 . . . . . . . . . . . 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 459 . . . . . . . . . . . . 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 4167 . . . . . . . . . . . . 13  |-  ( x  e.  U. ( `' g " { u } )  <->  E. v  e.  ( `' g " { u } ) x  e.  v )
7371, 72sylib 196 . . . . . . . . . . . 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 2852 . . . . . . . . . . 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 2923 . . . . . . . . . 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 830 . . . . . . . . 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 4167 . . . . . . . . 9  |-  ( x  e.  U. V  <->  E. v  e.  V  x  e.  v )
78 eliun 4248 . . . . . . . . 9  |-  ( x  e.  U_ u  e. 
ran  g U. ( `' g " {
u } )  <->  E. u  e.  ran  g  x  e. 
U. ( `' g
" { u }
) )
7976, 77, 783bitr4g 288 . . . . . . . 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 2379 . . . . . . 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 5168 . . . . . . . 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 16 . . . . . . 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 2427 . . . . . 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 728 . . . . . . . . 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 3037 . . . . . . . . . . 11  |-  w  e. 
_V
869elrnmpt 5162 . . . . . . . . . . 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 12 . . . . . . . . . 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 482 . . . . . . . . 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 3479 . . . . . . . . 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 60 . . . . . . . 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 1715 . . . . . . . . . 10  |-  F/ u
( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v  C_  (
g `  v )
)
92 nfmpt1 4456 . . . . . . . . . . . 12  |-  F/_ u
( u  e.  ran  g  |->  U. ( `' g
" { u }
) )
9392nfrn 5158 . . . . . . . . . . 11  |-  F/_ u ran  ( u  e.  ran  g  |->  U. ( `' g
" { u }
) )
9493nfcri 2537 . . . . . . . . . 10  |-  F/ u  w  e.  ran  ( u  e.  ran  g  |->  U. ( `' g " { u } ) )
9591, 94nfan 1936 . . . . . . . . 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 459 . . . . . . . . . . 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 1715 . . . . . . . . . . . . . . . 16  |-  F/ v  w  e.  ran  (
u  e.  ran  g  |-> 
U. ( `' g
" { u }
) )
9836, 97nfan 1936 . . . . . . . . . . . . . . 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 1715 . . . . . . . . . . . . . . 15  |-  F/ v  u  e.  U
10098, 99nfan 1936 . . . . . . . . . . . . . 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 1715 . . . . . . . . . . . . . 14  |-  F/ v  w  =  U. ( `' g " {
u } )
102100, 101nfan 1936 . . . . . . . . . . . . 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 768 . . . . . . . . . . . . . . . 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 732 . . . . . . . . . . . . . . . . . . 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 5910 . . . . . . . . . . . . . . . . . . 19  |-  ( g  Fn  V  ->  (
v  e.  ( `' g " { u } )  <->  ( v  e.  V  /\  (
g `  v )  =  u ) ) )
106104, 105syl 16 . . . . . . . . . . . . . . . . . 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 482 . . . . . . . . . . . . . . . . 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 457 . . . . . . . . . . . . . . . 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 2749 . . . . . . . . . . . . . . . 16  |-  ( ( A. v  e.  V  v  C_  ( g `  v )  /\  v  e.  V )  ->  v  C_  ( g `  v
) )
110103, 108, 109syl2anc 659 . . . . . . . . . . . . . . 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 461 . . . . . . . . . . . . . . 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 3453 . . . . . . . . . . . . . 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 432 . . . . . . . . . . . . 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 2782 . . . . . . . . . . . 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 4194 . . . . . . . . . . . 12  |-  ( U. ( `' g " {
u } )  C_  u 
<-> 
A. v  e.  ( `' g " {
u } ) v 
C_  u )
116114, 115sylibr 212 . . . . . . . . . . 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 3451 . . . . . . . . . 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 602 . . . . . . . . 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 2851 . . . . . . . 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 2796 . . . . . 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 3037 . . . . . . . . . 10  |-  g  e. 
_V
123122rnex 6633 . . . . . . . . 9  |-  ran  g  e.  _V
124123mptex 6044 . . . . . . . 8  |-  ( u  e.  ran  g  |->  U. ( `' g " { u } ) )  e.  _V
125 rnexg 6631 . . . . . . . 8  |-  ( ( u  e.  ran  g  |-> 
U. ( `' g
" { u }
) )  e.  _V  ->  ran  ( u  e. 
ran  g  |->  U. ( `' g " {
u } ) )  e.  _V )
126124, 125mp1i 12 . . . . . . 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 2382 . . . . . . . 8  |-  U. ran  ( u  e.  ran  g  |->  U. ( `' g
" { u }
) )  =  U. ran  ( u  e.  ran  g  |->  U. ( `' g
" { u }
) )
128127, 30isref 20095 . . . . . . 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 16 . . . . . 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 920 . . . . 5  |-  ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v 
C_  ( g `  v ) )  ->  ran  ( u  e.  ran  g  |->  U. ( `' g
" { u }
) ) Ref U
)
13115ad2antrr 723 . . . . . 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 723 . . . . . . 7  |-  ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v 
C_  ( g `  v ) )  ->  X  =  U. U )
134133, 83eqtrd 2423 . . . . . 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 1715 . . . . . . . . 9  |-  F/ v  x  e.  X
13636, 135nfan 1936 . . . . . . . 8  |-  F/ v ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v  C_  (
g `  v )
)  /\  x  e.  X )
137 simplr 753 . . . . . . . 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 5641 . . . . . . . . . . . . . 14  |-  ( g : V --> U  ->  Fun  g )
139138ad6antlr 734 . . . . . . . . . . . . 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 7728 . . . . . . . . . . . . 13  |-  ( ( Fun  g  /\  {
j  e.  V  | 
( j  i^i  v
)  =/=  (/) }  e.  Fin )  ->  ( g
" { j  e.  V  |  ( j  i^i  v )  =/=  (/) } )  e.  Fin )
141139, 140sylancom 665 . . . . . . . . . . . 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 996 . . . . . . . . . . . . . . . . . . 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 3954 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( u  =  k  ->  { u }  =  { k } )
144143imaeq2d 5249 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( u  =  k  ->  ( `' g " {
u } )  =  ( `' g " { k } ) )
145144unieqd 4173 . . . . . . . . . . . . . . . . . . . . 21  |-  ( u  =  k  ->  U. ( `' g " {
u } )  = 
U. ( `' g
" { k } ) )
146122cnvex 6646 . . . . . . . . . . . . . . . . . . . . . . 23  |-  `' g  e.  _V
147 imaexg 6636 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( `' g  e.  _V  ->  ( `' g " {
k } )  e. 
_V )
148146, 147ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( `' g " { k } )  e.  _V
149148uniex 6495 . . . . . . . . . . . . . . . . . . . . 21  |-  U. ( `' g " {
k } )  e. 
_V
150145, 9, 149fvmpt 5857 . . . . . . . . . . . . . . . . . . . 20  |-  ( k  e.  ran  g  -> 
( ( u  e. 
ran  g  |->  U. ( `' g " {
u } ) ) `
 k )  = 
U. ( `' g
" { k } ) )
1511503ad2ant2 1016 . . . . . . . . . . . . . . . . . . 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 2423 . . . . . . . . . . . . . . . . . 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 3613 . . . . . . . . . . . . . . . . 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 2659 . . . . . . . . . . . . . . . 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 6636 . . . . . . . . . . . . . . . . . . . . 21  |-  ( `' g  e.  _V  ->  ( `' g " {
u } )  e. 
_V )
157146, 156ax-mp 5 . . . . . . . . . . . . . . . . . . . 20  |-  ( `' g " { u } )  e.  _V
158157uniex 6495 . . . . . . . . . . . . . . . . . . 19  |-  U. ( `' g " {
u } )  e. 
_V
159158, 9fnmpti 5617 . . . . . . . . . . . . . . . . . 18  |-  ( u  e.  ran  g  |->  U. ( `' g " { u } ) )  Fn  ran  g
160 dffn4 5709 . . . . . . . . . . . . . . . . . 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 208 . . . . . . . . . . . . . . . . 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 27522 . . . . . . . . . . . . . . 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 3954 . . . . . . . . . . . . . . . . . . . 20  |-  ( k  =  u  ->  { k }  =  { u } )
165164imaeq2d 5249 . . . . . . . . . . . . . . . . . . 19  |-  ( k  =  u  ->  ( `' g " {
k } )  =  ( `' g " { u } ) )
166165unieqd 4173 . . . . . . . . . . . . . . . . . 18  |-  ( k  =  u  ->  U. ( `' g " {
k } )  = 
U. ( `' g
" { u }
) )
167166ineq1d 3613 . . . . . . . . . . . . . . . . 17  |-  ( k  =  u  ->  ( U. ( `' g " { k } )  i^i  v )  =  ( U. ( `' g " { u } )  i^i  v
) )
168167neeq1d 2659 . . . . . . . . . . . . . . . 16  |-  ( k  =  u  ->  (
( U. ( `' g " { k } )  i^i  v
)  =/=  (/)  <->  ( U. ( `' g " {
u } )  i^i  v )  =/=  (/) ) )
169168cbvrabv 3033 . . . . . . . . . . . . . . 15  |-  { k  e.  ran  g  |  ( U. ( `' g " { k } )  i^i  v
)  =/=  (/) }  =  { u  e.  ran  g  |  ( U. ( `' g " {
u } )  i^i  v )  =/=  (/) }
170163, 169syl6breq 4406 . . . . . . . . . . . . . 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 4516 . . . . . . . . . . . . . . 15  |-  { u  e.  ran  g  |  E. k  e.  { j  e.  V  |  (
j  i^i  v )  =/=  (/) }  ( g `
 k )  =  u }  e.  _V
172 nfv 1715 . . . . . . . . . . . . . . . . . . . . 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 2963 . . . . . . . . . . . . . . . . . . . . . 22  |-  F/_ j { j  e.  V  |  ( j  i^i  v )  =/=  (/) }
174173nfel1 2560 . . . . . . . . . . . . . . . . . . . . 21  |-  F/ j { j  e.  V  |  ( j  i^i  v )  =/=  (/) }  e.  Fin
175172, 174nfan 1936 . . . . . . . . . . . . . . . . . . . 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 1715 . . . . . . . . . . . . . . . . . . . 20  |-  F/ j  u  e.  ran  g
177175, 176nfan 1936 . . . . . . . . . . . . . . . . . . 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 1715 . . . . . . . . . . . . . . . . . . 19  |-  F/ j ( U. ( `' g " { u } )  i^i  v
)  =/=  (/)
179177, 178nfan 1936 . . . . . . . . . . . . . . . . . 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 1715 . . . . . . . . . . . . . . . . . . 19  |-  F/ j ( g `  k
)  =  u
181173, 180nfrex 2845 . . . . . . . . . . . . . . . . . 18  |-  F/ j E. k  e.  {
j  e.  V  | 
( j  i^i  v
)  =/=  (/) }  (
g `  k )  =  u
18239ad5antlr 732 . . . . . . . . . . . . . . . . . . . . . . 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 731 . . . . . . . . . . . . . . . . . . . . . 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 753 . . . . . . . . . . . . . . . . . . . . . 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 5910 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( g  Fn  V  ->  (
j  e.  ( `' g " { u } )  <->  ( j  e.  V  /\  (
g `  j )  =  u ) ) )
186185biimpa 482 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( g  Fn  V  /\  j  e.  ( `' g " { u }
) )  ->  (
j  e.  V  /\  ( g `  j
)  =  u ) )
187183, 184, 186syl2anc 659 . . . . . . . . . . . . . . . . . . . . 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 457 . . . . . . . . . . . . . . . . . . . 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 459 . . . . . . . . . . . . . . . . . . . 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 2959 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  e.  { j  e.  V  |  ( j  i^i  v )  =/=  (/) }  <->  ( j  e.  V  /\  ( j  i^i  v )  =/=  (/) ) )
191188, 189, 190sylanbrc 662 . . . . . . . . . . . . . . . . . . 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 461 . . . . . . . . . . . . . . . . . . 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 5774 . . . . . . . . . . . . . . . . . . . . 21  |-  ( k  =  j  ->  (
g `  k )  =  ( g `  j ) )
194193eqeq1d 2384 . . . . . . . . . . . . . . . . . . . 20  |-  ( k  =  j  ->  (
( g `  k
)  =  u  <->  ( g `  j )  =  u ) )
195194rspcev 3135 . . . . . . . . . . . . . . . . . . 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 659 . . . . . . . . . . . . . . . . . 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 27549 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( U. ( `' g
" { u }
)  i^i  v )  =/=  (/)  <->  E. j  e.  ( `' g " {
u } ) ( j  i^i  v )  =/=  (/) )
198197biimpi 194 . . . . . . . . . . . . . . . . . . 19  |-  ( ( U. ( `' g
" { u }
)  i^i  v )  =/=  (/)  ->  E. j  e.  ( `' g " { u } ) ( j  i^i  v
)  =/=  (/) )
199198adantl 464 . . . . . . . . . . . . . . . . . 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 2920 . . . . . . . . . . . . . . . . 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 432 . . . . . . . . . . . . . . . 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 3495 . . . . . . . . . . . . . . 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 7480 . . . . . . . . . . . . . . 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 63 . . . . . . . . . . . . . 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 7487 . . . . . . . . . . . . . 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 659 . . . . . . . . . . . . 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 463 . . . . . . . . . . . . . 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 5646 . . . . . . . . . . . . . . 15  |-  ( g  Fn  V  <->  g : V
--> ran  g )
209208biimpi 194 . . . . . . . . . . . . . 14  |-  ( g  Fn  V  ->  g : V --> ran  g )
210 ssrab2 3499 . . . . . . . . . . . . . . 15  |-  { j  e.  V  |  ( j  i^i  v )  =/=  (/) }  C_  V
211 fimarab 27623 . . . . . . . . . . . . . . 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 669 . . . . . . . . . . . . . 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 20 . . . . . . . . . . . . 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 4393 . . . . . . . . . . . 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 7657 . . . . . . . . . . . 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 659 . . . . . . . . . . 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 432 . . . . . . . . . 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 691 . . . . . . . . 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 427 . . . . . . . 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 757 . . . . . . . . 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 20103 . . . . . . . . . . . 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 196 . . . . . . . . . . 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 1008 . . . . . . . . . 10  |-  ( ph  ->  A. x  e.  X  E. v  e.  J  ( x  e.  v  /\  { j  e.  V  |  ( j  i^i  v )  =/=  (/) }  e.  Fin ) )
225224r19.21bi 2751 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  X )  ->  E. v  e.  J  ( x  e.  v  /\  { j  e.  V  |  ( j  i^i  v )  =/=  (/) }  e.  Fin ) )
226220, 225sylancom 665 . . . . . . . 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 2852 . . . . . . 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 2796 . . . . . 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 20103 . . . . . 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 1178 . . . . 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 5515 . . . . . . . 8  |-  ( f  =  ( u  e. 
ran  g  |->  U. ( `' g " {
u } ) )  ->  ( Fun  f  <->  Fun  ( u  e.  ran  g  |->  U. ( `' g
" { u }
) ) ) )
232 dmeq 5116 . . . . . . . . 9  |-  ( f  =  ( u  e. 
ran  g  |->  U. ( `' g " {
u } ) )  ->  dom  f  =  dom  ( u  e.  ran  g  |->  U. ( `' g
" { u }
) ) )
233232sseq1d 3444 . . . . . . . 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 5141 . . . . . . . . 9  |-  ( f  =  ( u  e. 
ran  g  |->  U. ( `' g " {
u } ) )  ->  ran  f  =  ran  ( u  e.  ran  g  |->  U. ( `' g
" { u }
) ) )
235234sseq1d 3444 . . . . . . . 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 1297 . . . . . . 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 4377 . . . . . . . 8  |-  ( f  =  ( u  e. 
ran  g  |->  U. ( `' g " {
u } ) )  ->  ( ran  f Ref U  <->  ran  ( u  e. 
ran  g  |->  U. ( `' g " {
u } ) ) Ref U ) )
238234eleq1d 2451 . . . . . . . 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 708 . . . . . . 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 708 . . . . . 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 3126 . . . . 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 1234 . . . 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 616 . . 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 1732 . 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 184    /\ wa 367    /\ w3a 971    = wceq 1399   E.wex 1620    e. wcel 1826    =/= wne 2577   A.wral 2732   E.wrex 2733   {crab 2736   _Vcvv 3034    i^i cin 3388    C_ wss 3389   (/)c0 3711   {csn 3944   U.cuni 4163   U_ciun 4243   class class class wbr 4367    |-> cmpt 4425   `'ccnv 4912   dom cdm 4913   ran crn 4914   "cima 4916   Fun wfun 5490    Fn wfn 5491   -->wf 5492   -onto->wfo 5494   ` cfv 5496    ~<_ cdom 7433   Fincfn 7435   Topctop 19479   Refcref 20088   LocFinclocfin 20090
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-8 1828  ax-9 1830  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360  ax-rep 4478  ax-sep 4488  ax-nul 4496  ax-pow 4543  ax-pr 4601  ax-un 6491  ax-reg 7933  ax-inf2 7972  ax-ac2 8756
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-eu 2222  df-mo 2223  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ne 2579  df-ral 2737  df-rex 2738  df-reu 2739  df-rmo 2740  df-rab 2741  df-v 3036  df-sbc 3253  df-csb 3349  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-pss 3405  df-nul 3712  df-if 3858  df-pw 3929  df-sn 3945  df-pr 3947  df-tp 3949  df-op 3951  df-uni 4164  df-int 4200  df-iun 4245  df-iin 4246  df-br 4368  df-opab 4426  df-mpt 4427  df-tr 4461  df-eprel 4705  df-id 4709  df-po 4714  df-so 4715  df-fr 4752  df-se 4753  df-we 4754  df-ord 4795  df-on 4796  df-lim 4797  df-suc 4798  df-xp 4919  df-rel 4920  df-cnv 4921  df-co 4922  df-dm 4923  df-rn 4924  df-res 4925  df-ima 4926  df-iota 5460  df-fun 5498  df-fn 5499  df-f 5500  df-f1 5501  df-fo 5502  df-f1o 5503  df-fv 5504  df-isom 5505  df-riota 6158  df-om 6600  df-recs 6960  df-rdg 6994  df-1o 7048  df-er 7229  df-en 7436  df-dom 7437  df-fin 7439  df-r1 8095  df-rank 8096  df-card 8233  df-ac 8410  df-top 19484  df-ref 20091  df-locfin 20093
This theorem is referenced by:  locfinref  27998
  Copyright terms: Public domain W3C validator