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

Theorem locfinreflem 28675
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 28674 . . . . 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 2422 . . . . . . 7  |-  ( u  e.  ran  g  |->  U. ( `' g " { u } ) )  =  ( u  e.  ran  g  |->  U. ( `' g " { u } ) )
109dmmptss 5350 . . . . . 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 3475 . . . . 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 20534 . . . . . . . . . 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 5207 . . . . . . . . . 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 3512 . . . . . . . . 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 3474 . . . . . . . 8  |-  ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v  C_  (
g `  v )
)  /\  u  e.  ran  g )  ->  ( `' g " {
u } )  C_  J )
24 uniopn 19925 . . . . . . . 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 2836 . . . . . 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 2422 . . . . . . . . . 10  |-  U. V  =  U. V
30 eqid 2422 . . . . . . . . . 10  |-  U. U  =  U. U
3129, 30refbas 20523 . . . . . . . . 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 1755 . . . . . . . . . . . . 13  |-  F/ v ( ph  /\  g : V --> U )
35 nfra1 2803 . . . . . . . . . . . . 13  |-  F/ v A. v  e.  V  v  C_  ( g `  v )
3634, 35nfan 1988 . . . . . . . . . . . 12  |-  F/ v ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v  C_  (
g `  v )
)
37 nfre1 2883 . . . . . . . . . . . 12  |-  F/ v E. v  e.  V  x  e.  v
3836, 37nfan 1988 . . . . . . . . . . 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 3483 . . . . . . . . . . . . . . 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 2422 . . . . . . . . . . . . . . . . 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 4241 . . . . . . . . . . . . . . 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 3464 . . . . . . . . . . . . 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 4008 . . . . . . . . . . . . . . . . 17  |-  ( u  =  ( g `  v )  ->  { u }  =  { (
g `  v ) } )
5554imaeq2d 5187 . . . . . . . . . . . . . . . 16  |-  ( u  =  ( g `  v )  ->  ( `' g " {
u } )  =  ( `' g " { ( g `  v ) } ) )
5655unieqd 4229 . . . . . . . . . . . . . . 15  |-  ( u  =  ( g `  v )  ->  U. ( `' g " {
u } )  = 
U. ( `' g
" { ( g `
 v ) } ) )
5756eleq2d 2492 . . . . . . . . . . . . . 14  |-  ( u  =  ( g `  v )  ->  (
x  e.  U. ( `' g " {
u } )  <->  x  e.  U. ( `' g " { ( g `  v ) } ) ) )
5857rspcev 3182 . . . . . . . . . . . . 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 2965 . . . . . . . . . 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 1755 . . . . . . . . . . . . . 14  |-  F/ v  u  e.  ran  g
6436, 63nfan 1988 . . . . . . . . . . . . 13  |-  F/ v ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v  C_  (
g `  v )
)  /\  u  e.  ran  g )
65 nfv 1755 . . . . . . . . . . . . 13  |-  F/ v  x  e.  U. ( `' g " {
u } )
6664, 65nfan 1988 . . . . . . . . . . . 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 3465 . . . . . . . . . . . 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 4223 . . . . . . . . . . . . 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 2892 . . . . . . . . . . 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 2966 . . . . . . . . . 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 4223 . . . . . . . . 9  |-  ( x  e.  U. V  <->  E. v  e.  V  x  e.  v )
78 eliun 4304 . . . . . . . . 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 2419 . . . . . . 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 5106 . . . . . . . 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 2467 . . . . . 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 3083 . . . . . . . . . . 11  |-  w  e. 
_V
869elrnmpt 5100 . . . . . . . . . . 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 3526 . . . . . . . . 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 1755 . . . . . . . . . 10  |-  F/ u
( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v  C_  (
g `  v )
)
92 nfmpt1 4513 . . . . . . . . . . . 12  |-  F/_ u
( u  e.  ran  g  |->  U. ( `' g
" { u }
) )
9392nfrn 5096 . . . . . . . . . . 11  |-  F/_ u ran  ( u  e.  ran  g  |->  U. ( `' g
" { u }
) )
9493nfcri 2573 . . . . . . . . . 10  |-  F/ u  w  e.  ran  ( u  e.  ran  g  |->  U. ( `' g " { u } ) )
9591, 94nfan 1988 . . . . . . . . 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 1755 . . . . . . . . . . . . . . . 16  |-  F/ v  w  e.  ran  (
u  e.  ran  g  |-> 
U. ( `' g
" { u }
) )
9836, 97nfan 1988 . . . . . . . . . . . . . . 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 1755 . . . . . . . . . . . . . . 15  |-  F/ v  u  e.  U
10098, 99nfan 1988 . . . . . . . . . . . . . 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 1755 . . . . . . . . . . . . . 14  |-  F/ v  w  =  U. ( `' g " {
u } )
102100, 101nfan 1988 . . . . . . . . . . . . 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 2789 . . . . . . . . . . . . . . . 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 3500 . . . . . . . . . . . . . 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 2822 . . . . . . . . . . . 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 4250 . . . . . . . . . . . 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 3498 . . . . . . . . . 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 2891 . . . . . . . 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 2836 . . . . . 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 3083 . . . . . . . . . 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 2422 . . . . . . . 8  |-  U. ran  ( u  e.  ran  g  |->  U. ( `' g
" { u }
) )  =  U. ran  ( u  e.  ran  g  |->  U. ( `' g
" { u }
) )
128127, 30isref 20522 . . . . . . 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 2463 . . . . . 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 1755 . . . . . . . . 9  |-  F/ v  x  e.  X
13636, 135nfan 1988 . . . . . . . 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 7876 . . . . . . . . . . . . 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 4008 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( u  =  k  ->  { u }  =  { k } )
144143imaeq2d 5187 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( u  =  k  ->  ( `' g " {
u } )  =  ( `' g " { k } ) )
145144unieqd 4229 . . . . . . . . . . . . . . . . . . . . 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 2463 . . . . . . . . . . . . . . . . . 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 3663 . . . . . . . . . . . . . . . . 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 2697 . . . . . . . . . . . . . . . 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 28139 . . . . . . . . . . . . . . 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 4008 . . . . . . . . . . . . . . . . . . . 20  |-  ( k  =  u  ->  { k }  =  { u } )
165164imaeq2d 5187 . . . . . . . . . . . . . . . . . . 19  |-  ( k  =  u  ->  ( `' g " {
k } )  =  ( `' g " { u } ) )
166165unieqd 4229 . . . . . . . . . . . . . . . . . 18  |-  ( k  =  u  ->  U. ( `' g " {
k } )  = 
U. ( `' g
" { u }
) )
167166ineq1d 3663 . . . . . . . . . . . . . . . . 17  |-  ( k  =  u  ->  ( U. ( `' g " { k } )  i^i  v )  =  ( U. ( `' g " { u } )  i^i  v
) )
168167neeq1d 2697 . . . . . . . . . . . . . . . 16  |-  ( k  =  u  ->  (
( U. ( `' g " { k } )  i^i  v
)  =/=  (/)  <->  ( U. ( `' g " {
u } )  i^i  v )  =/=  (/) ) )
169168cbvrabv 3079 . . . . . . . . . . . . . . 15  |-  { k  e.  ran  g  |  ( U. ( `' g " { k } )  i^i  v
)  =/=  (/) }  =  { u  e.  ran  g  |  ( U. ( `' g " {
u } )  i^i  v )  =/=  (/) }
170163, 169syl6breq 4463 . . . . . . . . . . . . . 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 4575 . . . . . . . . . . . . . . 15  |-  { u  e.  ran  g  |  E. k  e.  { j  e.  V  |  (
j  i^i  v )  =/=  (/) }  ( g `
 k )  =  u }  e.  _V
172 nfv 1755 . . . . . . . . . . . . . . . . . . . . 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 3006 . . . . . . . . . . . . . . . . . . . . . 22  |-  F/_ j { j  e.  V  |  ( j  i^i  v )  =/=  (/) }
174173nfel1 2596 . . . . . . . . . . . . . . . . . . . . 21  |-  F/ j { j  e.  V  |  ( j  i^i  v )  =/=  (/) }  e.  Fin
175172, 174nfan 1988 . . . . . . . . . . . . . . . . . . . 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 1755 . . . . . . . . . . . . . . . . . . . 20  |-  F/ j  u  e.  ran  g
177175, 176nfan 1988 . . . . . . . . . . . . . . . . . . 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 1755 . . . . . . . . . . . . . . . . . . 19  |-  F/ j ( U. ( `' g " { u } )  i^i  v
)  =/=  (/)
179177, 178nfan 1988 . . . . . . . . . . . . . . . . . 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 1755 . . . . . . . . . . . . . . . . . . 19  |-  F/ j ( g `  k
)  =  u
181173, 180nfrex 2885 . . . . . . . . . . . . . . . . . 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 3002 . . . . . . . . . . . . . . . . . . . 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 2424 . . . . . . . . . . . . . . . . . . . 20  |-  ( k  =  j  ->  (
( g `  k
)  =  u  <->  ( g `  j )  =  u ) )
195194rspcev 3182 . . . . . . . . . . . . . . . . . . 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 28165 . . . . . . . . . . . . . . . . . . . 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 2963 . . . . . . . . . . . . . . . . 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 3542 . . . . . . . . . . . . . . 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 7625 . . . . . . . . . . . . . . 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 7632 . . . . . . . . . . . . . 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 3546 . . . . . . . . . . . . . . 15  |-  { j  e.  V  |  ( j  i^i  v )  =/=  (/) }  C_  V
211 fimarab 28246 . . . . . . . . . . . . . . 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 4450 . . . . . . . . . . . 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 7802 . . . . . . . . . . . 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 20530 . . . . . . . . . . . 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 2791 . . . . . . . . 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 2892 . . . . . . 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 2836 . . . . . 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 20530 . . . . . 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 5054 . . . . . . . . 9  |-  ( f  =  ( u  e. 
ran  g  |->  U. ( `' g " {
u } ) )  ->  dom  f  =  dom  ( u  e.  ran  g  |->  U. ( `' g
" { u }
) ) )
233232sseq1d 3491 . . . . . . . 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 5079 . . . . . . . . 9  |-  ( f  =  ( u  e. 
ran  g  |->  U. ( `' g " {
u } ) )  ->  ran  f  =  ran  ( u  e.  ran  g  |->  U. ( `' g
" { u }
) ) )
235234sseq1d 3491 . . . . . . . 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 4433 . . . . . . . 8  |-  ( f  =  ( u  e. 
ran  g  |->  U. ( `' g " {
u } ) )  ->  ( ran  f Ref U  <->  ran  ( u  e. 
ran  g  |->  U. ( `' g " {
u } ) ) Ref U ) )
238234eleq1d 2491 . . . . . . . 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 3173 . . . . 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 1772 . 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 1657    e. wcel 1872    =/= wne 2614   A.wral 2771   E.wrex 2772   {crab 2775   _Vcvv 3080    i^i cin 3435    C_ wss 3436   (/)c0 3761   {csn 3998   U.cuni 4219   U_ciun 4299   class class class wbr 4423    |-> cmpt 4482   `'ccnv 4852   dom cdm 4853   ran crn 4854   "cima 4856   Fun wfun 5595    Fn wfn 5596   -->wf 5597   -onto->wfo 5599   ` cfv 5601    ~<_ cdom 7578   Fincfn 7580   Topctop 19915   Refcref 20515   LocFinclocfin 20517
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-rep 4536  ax-sep 4546  ax-nul 4555  ax-pow 4602  ax-pr 4660  ax-un 6597  ax-reg 8116  ax-inf2 8155  ax-ac2 8900
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 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-ral 2776  df-rex 2777  df-reu 2778  df-rmo 2779  df-rab 2780  df-v 3082  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3912  df-pw 3983  df-sn 3999  df-pr 4001  df-tp 4003  df-op 4005  df-uni 4220  df-int 4256  df-iun 4301  df-iin 4302  df-br 4424  df-opab 4483  df-mpt 4484  df-tr 4519  df-eprel 4764  df-id 4768  df-po 4774  df-so 4775  df-fr 4812  df-se 4813  df-we 4814  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  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 7039  df-recs 7101  df-rdg 7139  df-1o 7193  df-er 7374  df-en 7581  df-dom 7582  df-fin 7584  df-r1 8243  df-rank 8244  df-card 8381  df-ac 8554  df-top 19919  df-ref 20518  df-locfin 20520
This theorem is referenced by:  locfinref  28676
  Copyright terms: Public domain W3C validator