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

Theorem locfinreflem 28741
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 28740 . . . . 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 215 . . 3  |-  ( ph  ->  ( U. U  C_  U. V  /\  E. g
( g : V --> U  /\  A. v  e.  V  v  C_  (
g `  v )
) ) )
65simprd 470 . 2  |-  ( ph  ->  E. g ( g : V --> U  /\  A. v  e.  V  v 
C_  ( g `  v ) ) )
7 funmpt 5625 . . . . . 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 2471 . . . . . . 7  |-  ( u  e.  ran  g  |->  U. ( `' g " { u } ) )  =  ( u  e.  ran  g  |->  U. ( `' g " { u } ) )
109dmmptss 5338 . . . . . 6  |-  dom  (
u  e.  ran  g  |-> 
U. ( `' g
" { u }
) )  C_  ran  g
11 frn 5747 . . . . . . 7  |-  ( g : V --> U  ->  ran  g  C_  U )
1211ad2antlr 741 . . . . . 6  |-  ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v 
C_  ( g `  v ) )  ->  ran  g  C_  U )
1310, 12syl5ss 3429 . . . . 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 20613 . . . . . . . . . 10  |-  ( V  e.  ( LocFin `  J
)  ->  J  e.  Top )
152, 14syl 17 . . . . . . . . 9  |-  ( ph  ->  J  e.  Top )
1615ad3antrrr 744 . . . . . . . 8  |-  ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v  C_  (
g `  v )
)  /\  u  e.  ran  g )  ->  J  e.  Top )
17 cnvimass 5194 . . . . . . . . . 10  |-  ( `' g " { u } )  C_  dom  g
18 fdm 5745 . . . . . . . . . . 11  |-  ( g : V --> U  ->  dom  g  =  V
)
1918ad3antlr 745 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v  C_  (
g `  v )
)  /\  u  e.  ran  g )  ->  dom  g  =  V )
2017, 19syl5sseq 3466 . . . . . . . . 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 744 . . . . . . . . 9  |-  ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v  C_  (
g `  v )
)  /\  u  e.  ran  g )  ->  V  C_  J )
2320, 22sstrd 3428 . . . . . . . 8  |-  ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v  C_  (
g `  v )
)  /\  u  e.  ran  g )  ->  ( `' g " {
u } )  C_  J )
24 uniopn 20004 . . . . . . . 8  |-  ( ( J  e.  Top  /\  ( `' g " {
u } )  C_  J )  ->  U. ( `' g " {
u } )  e.  J )
2516, 23, 24syl2anc 673 . . . . . . 7  |-  ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v  C_  (
g `  v )
)  /\  u  e.  ran  g )  ->  U. ( `' g " {
u } )  e.  J )
2625ralrimiva 2809 . . . . . 6  |-  ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v 
C_  ( g `  v ) )  ->  A. u  e.  ran  g U. ( `' g
" { u }
)  e.  J )
279rnmptss 6068 . . . . . 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 2471 . . . . . . . . . 10  |-  U. V  =  U. V
30 eqid 2471 . . . . . . . . . 10  |-  U. U  =  U. U
3129, 30refbas 20602 . . . . . . . . 9  |-  ( V Ref U  ->  U. U  =  U. V )
321, 31syl 17 . . . . . . . 8  |-  ( ph  ->  U. U  =  U. V )
3332ad2antrr 740 . . . . . . 7  |-  ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v 
C_  ( g `  v ) )  ->  U. U  =  U. V )
34 nfv 1769 . . . . . . . . . . . . 13  |-  F/ v ( ph  /\  g : V --> U )
35 nfra1 2785 . . . . . . . . . . . . 13  |-  F/ v A. v  e.  V  v  C_  ( g `  v )
3634, 35nfan 2031 . . . . . . . . . . . 12  |-  F/ v ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v  C_  (
g `  v )
)
37 nfre1 2846 . . . . . . . . . . . 12  |-  F/ v E. v  e.  V  x  e.  v
3836, 37nfan 2031 . . . . . . . . . . 11  |-  F/ v ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v  C_  (
g `  v )
)  /\  E. v  e.  V  x  e.  v )
39 ffn 5739 . . . . . . . . . . . . . . 15  |-  ( g : V --> U  -> 
g  Fn  V )
4039ad4antlr 747 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v  C_  (
g `  v )
)  /\  v  e.  V )  /\  x  e.  v )  ->  g  Fn  V )
41 simplr 770 . . . . . . . . . . . . . 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 673 . . . . . . . . . . . . 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 3437 . . . . . . . . . . . . . . 15  |-  v  C_  v
4539ad3antlr 745 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v  C_  (
g `  v )
)  /\  v  e.  V )  ->  g  Fn  V )
46 eqid 2471 . . . . . . . . . . . . . . . . 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 493 . . . . . . . . . . . . . . . . 17  |-  ( ( g  Fn  V  /\  ( v  e.  V  /\  ( g `  v
)  =  ( g `
 v ) ) )  ->  v  e.  ( `' g " {
( g `  v
) } ) )
4946, 48mpanr2 698 . . . . . . . . . . . . . . . 16  |-  ( ( g  Fn  V  /\  v  e.  V )  ->  v  e.  ( `' g " { ( g `  v ) } ) )
5045, 49sylancom 680 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v  C_  (
g `  v )
)  /\  v  e.  V )  ->  v  e.  ( `' g " { ( g `  v ) } ) )
51 ssuni 4212 . . . . . . . . . . . . . . 15  |-  ( ( v  C_  v  /\  v  e.  ( `' g " { ( g `
 v ) } ) )  ->  v  C_ 
U. ( `' g
" { ( g `
 v ) } ) )
5244, 50, 51sylancr 676 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v  C_  (
g `  v )
)  /\  v  e.  V )  ->  v  C_ 
U. ( `' g
" { ( g `
 v ) } ) )
5352sselda 3418 . . . . . . . . . . . . 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 3969 . . . . . . . . . . . . . . . . 17  |-  ( u  =  ( g `  v )  ->  { u }  =  { (
g `  v ) } )
5554imaeq2d 5174 . . . . . . . . . . . . . . . 16  |-  ( u  =  ( g `  v )  ->  ( `' g " {
u } )  =  ( `' g " { ( g `  v ) } ) )
5655unieqd 4200 . . . . . . . . . . . . . . 15  |-  ( u  =  ( g `  v )  ->  U. ( `' g " {
u } )  = 
U. ( `' g
" { ( g `
 v ) } ) )
5756eleq2d 2534 . . . . . . . . . . . . . 14  |-  ( u  =  ( g `  v )  ->  (
x  e.  U. ( `' g " {
u } )  <->  x  e.  U. ( `' g " { ( g `  v ) } ) ) )
5857rspcev 3136 . . . . . . . . . . . . 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 673 . . . . . . . . . . . 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 733 . . . . . . . . . . 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 468 . . . . . . . . . . 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 2916 . . . . . . . . . 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 1769 . . . . . . . . . . . . . 14  |-  F/ v  u  e.  ran  g
6436, 63nfan 2031 . . . . . . . . . . . . 13  |-  F/ v ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v  C_  (
g `  v )
)  /\  u  e.  ran  g )
65 nfv 1769 . . . . . . . . . . . . 13  |-  F/ v  x  e.  U. ( `' g " {
u } )
6664, 65nfan 2031 . . . . . . . . . . . 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 744 . . . . . . . . . . . . 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 770 . . . . . . . . . . . . 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 3419 . . . . . . . . . . . 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 468 . . . . . . . . . . . 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 468 . . . . . . . . . . . . 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 4194 . . . . . . . . . . . . 13  |-  ( x  e.  U. ( `' g " { u } )  <->  E. v  e.  ( `' g " { u } ) x  e.  v )
7371, 72sylib 201 . . . . . . . . . . . 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 2854 . . . . . . . . . . 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 2917 . . . . . . . . . 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 850 . . . . . . . . 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 4194 . . . . . . . . 9  |-  ( x  e.  U. V  <->  E. v  e.  V  x  e.  v )
78 eliun 4274 . . . . . . . . 9  |-  ( x  e.  U_ u  e. 
ran  g U. ( `' g " {
u } )  <->  E. u  e.  ran  g  x  e. 
U. ( `' g
" { u }
) )
7976, 77, 783bitr4g 296 . . . . . . . 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 2469 . . . . . . 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 5093 . . . . . . . 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 2509 . . . . . 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 745 . . . . . . . . 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 3034 . . . . . . . . . . 11  |-  w  e. 
_V
869elrnmpt 5087 . . . . . . . . . . 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 492 . . . . . . . . 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 3480 . . . . . . . . 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 61 . . . . . . . 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 1769 . . . . . . . . . 10  |-  F/ u
( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v  C_  (
g `  v )
)
92 nfmpt1 4485 . . . . . . . . . . . 12  |-  F/_ u
( u  e.  ran  g  |->  U. ( `' g
" { u }
) )
9392nfrn 5083 . . . . . . . . . . 11  |-  F/_ u ran  ( u  e.  ran  g  |->  U. ( `' g
" { u }
) )
9493nfcri 2606 . . . . . . . . . 10  |-  F/ u  w  e.  ran  ( u  e.  ran  g  |->  U. ( `' g " { u } ) )
9591, 94nfan 2031 . . . . . . . . 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 468 . . . . . . . . . . 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 1769 . . . . . . . . . . . . . . . 16  |-  F/ v  w  e.  ran  (
u  e.  ran  g  |-> 
U. ( `' g
" { u }
) )
9836, 97nfan 2031 . . . . . . . . . . . . . . 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 1769 . . . . . . . . . . . . . . 15  |-  F/ v  u  e.  U
10098, 99nfan 2031 . . . . . . . . . . . . . 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 1769 . . . . . . . . . . . . . 14  |-  F/ v  w  =  U. ( `' g " {
u } )
102100, 101nfan 2031 . . . . . . . . . . . . 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 787 . . . . . . . . . . . . . . . 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 749 . . . . . . . . . . . . . . . . . . 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 492 . . . . . . . . . . . . . . . . 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 466 . . . . . . . . . . . . . . . 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 2774 . . . . . . . . . . . . . . . 16  |-  ( ( A. v  e.  V  v  C_  ( g `  v )  /\  v  e.  V )  ->  v  C_  ( g `  v
) )
110103, 108, 109syl2anc 673 . . . . . . . . . . . . . . 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 470 . . . . . . . . . . . . . . 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 3454 . . . . . . . . . . . . . 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 441 . . . . . . . . . . . . 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 2800 . . . . . . . . . . . 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 4221 . . . . . . . . . . . 12  |-  ( U. ( `' g " {
u } )  C_  u 
<-> 
A. v  e.  ( `' g " {
u } ) v 
C_  u )
116114, 115sylibr 217 . . . . . . . . . . 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 3452 . . . . . . . . . 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 615 . . . . . . . . 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 2853 . . . . . . . 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 2809 . . . . . 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 3034 . . . . . . . . . 10  |-  g  e. 
_V
123122rnex 6746 . . . . . . . . 9  |-  ran  g  e.  _V
124123mptex 6152 . . . . . . . 8  |-  ( u  e.  ran  g  |->  U. ( `' g " { u } ) )  e.  _V
125 rnexg 6744 . . . . . . . 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 2471 . . . . . . . 8  |-  U. ran  ( u  e.  ran  g  |->  U. ( `' g
" { u }
) )  =  U. ran  ( u  e.  ran  g  |->  U. ( `' g
" { u }
) )
128127, 30isref 20601 . . . . . . 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 936 . . . . 5  |-  ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v 
C_  ( g `  v ) )  ->  ran  ( u  e.  ran  g  |->  U. ( `' g
" { u }
) ) Ref U
)
13115ad2antrr 740 . . . . . 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 740 . . . . . . 7  |-  ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v 
C_  ( g `  v ) )  ->  X  =  U. U )
134133, 83eqtrd 2505 . . . . . 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 1769 . . . . . . . . 9  |-  F/ v  x  e.  X
13636, 135nfan 2031 . . . . . . . 8  |-  F/ v ( ( ( ph  /\  g : V --> U )  /\  A. v  e.  V  v  C_  (
g `  v )
)  /\  x  e.  X )
137 simplr 770 . . . . . . . 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 5742 . . . . . . . . . . . . . 14  |-  ( g : V --> U  ->  Fun  g )
139138ad6antlr 751 . . . . . . . . . . . . 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 7885 . . . . . . . . . . . . 13  |-  ( ( Fun  g  /\  {
j  e.  V  | 
( j  i^i  v
)  =/=  (/) }  e.  Fin )  ->  ( g
" { j  e.  V  |  ( j  i^i  v )  =/=  (/) } )  e.  Fin )
141139, 140sylancom 680 . . . . . . . . . . . 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 1032 . . . . . . . . . . . . . . . . . . 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 3969 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( u  =  k  ->  { u }  =  { k } )
144143imaeq2d 5174 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( u  =  k  ->  ( `' g " {
u } )  =  ( `' g " { k } ) )
145144unieqd 4200 . . . . . . . . . . . . . . . . . . . . 21  |-  ( u  =  k  ->  U. ( `' g " {
u } )  = 
U. ( `' g
" { k } ) )
146122cnvex 6759 . . . . . . . . . . . . . . . . . . . . . . 23  |-  `' g  e.  _V
147 imaexg 6749 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( `' g  e.  _V  ->  ( `' g " {
k } )  e. 
_V )
148146, 147ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( `' g " { k } )  e.  _V
149148uniex 6606 . . . . . . . . . . . . . . . . . . . . 21  |-  U. ( `' g " {
k } )  e. 
_V
150145, 9, 149fvmpt 5963 . . . . . . . . . . . . . . . . . . . 20  |-  ( k  e.  ran  g  -> 
( ( u  e. 
ran  g  |->  U. ( `' g " {
u } ) ) `
 k )  = 
U. ( `' g
" { k } ) )
1511503ad2ant2 1052 . . . . . . . . . . . . . . . . . . 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 2505 . . . . . . . . . . . . . . . . . 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 3624 . . . . . . . . . . . . . . . . 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 2702 . . . . . . . . . . . . . . . 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 6749 . . . . . . . . . . . . . . . . . . . . 21  |-  ( `' g  e.  _V  ->  ( `' g " {
u } )  e. 
_V )
157146, 156ax-mp 5 . . . . . . . . . . . . . . . . . . . 20  |-  ( `' g " { u } )  e.  _V
158157uniex 6606 . . . . . . . . . . . . . . . . . . 19  |-  U. ( `' g " {
u } )  e. 
_V
159158, 9fnmpti 5716 . . . . . . . . . . . . . . . . . 18  |-  ( u  e.  ran  g  |->  U. ( `' g " { u } ) )  Fn  ran  g
160 dffn4 5812 . . . . . . . . . . . . . . . . . 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 213 . . . . . . . . . . . . . . . . 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 28219 . . . . . . . . . . . . . . 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 3969 . . . . . . . . . . . . . . . . . . . 20  |-  ( k  =  u  ->  { k }  =  { u } )
165164imaeq2d 5174 . . . . . . . . . . . . . . . . . . 19  |-  ( k  =  u  ->  ( `' g " {
k } )  =  ( `' g " { u } ) )
166165unieqd 4200 . . . . . . . . . . . . . . . . . 18  |-  ( k  =  u  ->  U. ( `' g " {
k } )  = 
U. ( `' g
" { u }
) )
167166ineq1d 3624 . . . . . . . . . . . . . . . . 17  |-  ( k  =  u  ->  ( U. ( `' g " { k } )  i^i  v )  =  ( U. ( `' g " { u } )  i^i  v
) )
168167neeq1d 2702 . . . . . . . . . . . . . . . 16  |-  ( k  =  u  ->  (
( U. ( `' g " { k } )  i^i  v
)  =/=  (/)  <->  ( U. ( `' g " {
u } )  i^i  v )  =/=  (/) ) )
169168cbvrabv 3030 . . . . . . . . . . . . . . 15  |-  { k  e.  ran  g  |  ( U. ( `' g " { k } )  i^i  v
)  =/=  (/) }  =  { u  e.  ran  g  |  ( U. ( `' g " {
u } )  i^i  v )  =/=  (/) }
170163, 169syl6breq 4435 . . . . . . . . . . . . . 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 4550 . . . . . . . . . . . . . . 15  |-  { u  e.  ran  g  |  E. k  e.  { j  e.  V  |  (
j  i^i  v )  =/=  (/) }  ( g `
 k )  =  u }  e.  _V
172 nfv 1769 . . . . . . . . . . . . . . . . . . . . 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 2957 . . . . . . . . . . . . . . . . . . . . . 22  |-  F/_ j { j  e.  V  |  ( j  i^i  v )  =/=  (/) }
174173nfel1 2626 . . . . . . . . . . . . . . . . . . . . 21  |-  F/ j { j  e.  V  |  ( j  i^i  v )  =/=  (/) }  e.  Fin
175172, 174nfan 2031 . . . . . . . . . . . . . . . . . . . 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 1769 . . . . . . . . . . . . . . . . . . . 20  |-  F/ j  u  e.  ran  g
177175, 176nfan 2031 . . . . . . . . . . . . . . . . . . 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 1769 . . . . . . . . . . . . . . . . . . 19  |-  F/ j ( U. ( `' g " { u } )  i^i  v
)  =/=  (/)
179177, 178nfan 2031 . . . . . . . . . . . . . . . . . 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 1769 . . . . . . . . . . . . . . . . . . 19  |-  F/ j ( g `  k
)  =  u
181173, 180nfrex 2848 . . . . . . . . . . . . . . . . . 18  |-  F/ j E. k  e.  {
j  e.  V  | 
( j  i^i  v
)  =/=  (/) }  (
g `  k )  =  u
18239ad5antlr 749 . . . . . . . . . . . . . . . . . . . . . . 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 748 . . . . . . . . . . . . . . . . . . . . . 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 770 . . . . . . . . . . . . . . . . . . . . . 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 492 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( g  Fn  V  /\  j  e.  ( `' g " { u }
) )  ->  (
j  e.  V  /\  ( g `  j
)  =  u ) )
187183, 184, 186syl2anc 673 . . . . . . . . . . . . . . . . . . . . 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 466 . . . . . . . . . . . . . . . . . . . 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 468 . . . . . . . . . . . . . . . . . . . 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 2953 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  e.  { j  e.  V  |  ( j  i^i  v )  =/=  (/) }  <->  ( j  e.  V  /\  ( j  i^i  v )  =/=  (/) ) )
191188, 189, 190sylanbrc 677 . . . . . . . . . . . . . . . . . . 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 470 . . . . . . . . . . . . . . . . . . 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 5879 . . . . . . . . . . . . . . . . . . . . 21  |-  ( k  =  j  ->  (
g `  k )  =  ( g `  j ) )
194193eqeq1d 2473 . . . . . . . . . . . . . . . . . . . 20  |-  ( k  =  j  ->  (
( g `  k
)  =  u  <->  ( g `  j )  =  u ) )
195194rspcev 3136 . . . . . . . . . . . . . . . . . . 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 673 . . . . . . . . . . . . . . . . . 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 28241 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( U. ( `' g
" { u }
)  i^i  v )  =/=  (/)  <->  E. j  e.  ( `' g " {
u } ) ( j  i^i  v )  =/=  (/) )
198197biimpi 199 . . . . . . . . . . . . . . . . . . 19  |-  ( ( U. ( `' g
" { u }
)  i^i  v )  =/=  (/)  ->  E. j  e.  ( `' g " { u } ) ( j  i^i  v
)  =/=  (/) )
199198adantl 473 . . . . . . . . . . . . . . . . . 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 2915 . . . . . . . . . . . . . . . . 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 441 . . . . . . . . . . . . . . . 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 3496 . . . . . . . . . . . . . . 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 7633 . . . . . . . . . . . . . . 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 64 . . . . . . . . . . . . . 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 7640 . . . . . . . . . . . . . 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 673 . . . . . . . . . . . . 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 472 . . . . . . . . . . . . . 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 5748 . . . . . . . . . . . . . . 15  |-  ( g  Fn  V  <->  g : V
--> ran  g )
209208biimpi 199 . . . . . . . . . . . . . 14  |-  ( g  Fn  V  ->  g : V --> ran  g )
210 ssrab2 3500 . . . . . . . . . . . . . . 15  |-  { j  e.  V  |  ( j  i^i  v )  =/=  (/) }  C_  V
211 fimarab 28320 . . . . . . . . . . . . . . 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 685 . . . . . . . . . . . . . 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 4422 . . . . . . . . . . . 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 7811 . . . . . . . . . . . 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 673 . . . . . . . . . . 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 441 . . . . . . . . . 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 707 . . . . . . . . 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 436 . . . . . . . 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 776 . . . . . . . . 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 20609 . . . . . . . . . . . 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 201 . . . . . . . . . . 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 1044 . . . . . . . . . 10  |-  ( ph  ->  A. x  e.  X  E. v  e.  J  ( x  e.  v  /\  { j  e.  V  |  ( j  i^i  v )  =/=  (/) }  e.  Fin ) )
225224r19.21bi 2776 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  X )  ->  E. v  e.  J  ( x  e.  v  /\  { j  e.  V  |  ( j  i^i  v )  =/=  (/) }  e.  Fin ) )
226220, 225sylancom 680 . . . . . . . 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 2854 . . . . . . 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 2809 . . . . . 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 20609 . . . . . 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 1214 . . . . 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 5608 . . . . . . . 8  |-  ( f  =  ( u  e. 
ran  g  |->  U. ( `' g " {
u } ) )  ->  ( Fun  f  <->  Fun  ( u  e.  ran  g  |->  U. ( `' g
" { u }
) ) ) )
232 dmeq 5040 . . . . . . . . 9  |-  ( f  =  ( u  e. 
ran  g  |->  U. ( `' g " {
u } ) )  ->  dom  f  =  dom  ( u  e.  ran  g  |->  U. ( `' g
" { u }
) ) )
233232sseq1d 3445 . . . . . . . 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 5066 . . . . . . . . 9  |-  ( f  =  ( u  e. 
ran  g  |->  U. ( `' g " {
u } ) )  ->  ran  f  =  ran  ( u  e.  ran  g  |->  U. ( `' g
" { u }
) ) )
235234sseq1d 3445 . . . . . . . 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 1365 . . . . . . 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 4405 . . . . . . . 8  |-  ( f  =  ( u  e. 
ran  g  |->  U. ( `' g " {
u } ) )  ->  ( ran  f Ref U  <->  ran  ( u  e. 
ran  g  |->  U. ( `' g " {
u } ) ) Ref U ) )
238234eleq1d 2533 . . . . . . . 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 725 . . . . . . 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 725 . . . . . 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 3127 . . . . 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 1300 . . . 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 630 . . 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 1787 . 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 189    /\ wa 376    /\ w3a 1007    = wceq 1452   E.wex 1671    e. wcel 1904    =/= wne 2641   A.wral 2756   E.wrex 2757   {crab 2760   _Vcvv 3031    i^i cin 3389    C_ wss 3390   (/)c0 3722   {csn 3959   U.cuni 4190   U_ciun 4269   class class class wbr 4395    |-> cmpt 4454   `'ccnv 4838   dom cdm 4839   ran crn 4840   "cima 4842   Fun wfun 5583    Fn wfn 5584   -->wf 5585   -onto->wfo 5587   ` cfv 5589    ~<_ cdom 7585   Fincfn 7587   Topctop 19994   Refcref 20594   LocFinclocfin 20596
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-rep 4508  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602  ax-reg 8125  ax-inf2 8164  ax-ac2 8911
This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3or 1008  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-ral 2761  df-rex 2762  df-reu 2763  df-rmo 2764  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-pss 3406  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-tp 3964  df-op 3966  df-uni 4191  df-int 4227  df-iun 4271  df-iin 4272  df-br 4396  df-opab 4455  df-mpt 4456  df-tr 4491  df-eprel 4750  df-id 4754  df-po 4760  df-so 4761  df-fr 4798  df-se 4799  df-we 4800  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-pred 5387  df-ord 5433  df-on 5434  df-lim 5435  df-suc 5436  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-fv 5597  df-isom 5598  df-riota 6270  df-om 6712  df-wrecs 7046  df-recs 7108  df-rdg 7146  df-1o 7200  df-er 7381  df-en 7588  df-dom 7589  df-fin 7591  df-r1 8253  df-rank 8254  df-card 8391  df-ac 8565  df-top 19998  df-ref 20597  df-locfin 20599
This theorem is referenced by:  locfinref  28742
  Copyright terms: Public domain W3C validator