Metamath Proof Explorer

Theorem locfinreflem

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)

Ref Expression
Hypotheses 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 locfinreflem 
|- ( ph -> E. f ( ( Fun f /\ dom f C_ U /\ ran f C_ J ) /\ ( ran f Ref U /\ ran f e. ( LocFin ` J ) ) ) )

Proof

Step Hyp Ref Expression
1 locfinref.x 
 |-  X = U. J
2 locfinref.1 
 |-  ( ph -> U C_ J )
3 locfinref.2 
 |-  ( ph -> X = U. U )
4 locfinref.3 
 |-  ( ph -> V C_ J )
5 locfinref.4 
 |-  ( ph -> V Ref U )
6 locfinref.5 
 |-  ( ph -> V e. ( LocFin ` J ) )
7 reff 
 |-  ( 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 ) ) ) ) )
8 6 7 syl 
 |-  ( ph -> ( V Ref U <-> ( U. U C_ U. V /\ E. g ( g : V --> U /\ A. v e. V v C_ ( g ` v ) ) ) ) )
9 5 8 mpbid 
 |-  ( ph -> ( U. U C_ U. V /\ E. g ( g : V --> U /\ A. v e. V v C_ ( g ` v ) ) ) )
10 9 simprd 
 |-  ( ph -> E. g ( g : V --> U /\ A. v e. V v C_ ( g ` v ) ) )
11 funmpt 
 |-  Fun ( u e. ran g |-> U. ( `' g " { u } ) )
12 11 a1i 
 |-  ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) -> Fun ( u e. ran g |-> U. ( `' g " { u } ) ) )
13 eqid 
 |-  ( u e. ran g |-> U. ( `' g " { u } ) ) = ( u e. ran g |-> U. ( `' g " { u } ) )
14 13 dmmptss 
 |-  dom ( u e. ran g |-> U. ( `' g " { u } ) ) C_ ran g
15 frn 
 |-  ( g : V --> U -> ran g C_ U )
16 15 ad2antlr 
 |-  ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) -> ran g C_ U )
17 14 16 sstrid 
 |-  ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) -> dom ( u e. ran g |-> U. ( `' g " { u } ) ) C_ U )
18 locfintop 
 |-  ( V e. ( LocFin ` J ) -> J e. Top )
19 6 18 syl 
 |-  ( ph -> J e. Top )
20 19 ad3antrrr 
 |-  ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ u e. ran g ) -> J e. Top )
21 cnvimass 
 |-  ( `' g " { u } ) C_ dom g
22 fdm 
 |-  ( g : V --> U -> dom g = V )
23 22 ad3antlr 
 |-  ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ u e. ran g ) -> dom g = V )
24 21 23 sseqtrid 
 |-  ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ u e. ran g ) -> ( `' g " { u } ) C_ V )
25 4 ad3antrrr 
 |-  ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ u e. ran g ) -> V C_ J )
26 24 25 sstrd 
 |-  ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ u e. ran g ) -> ( `' g " { u } ) C_ J )
27 uniopn 
 |-  ( ( J e. Top /\ ( `' g " { u } ) C_ J ) -> U. ( `' g " { u } ) e. J )
28 20 26 27 syl2anc 
 |-  ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ u e. ran g ) -> U. ( `' g " { u } ) e. J )
29 28 ralrimiva 
 |-  ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) -> A. u e. ran g U. ( `' g " { u } ) e. J )
30 13 rnmptss 
 |-  ( A. u e. ran g U. ( `' g " { u } ) e. J -> ran ( u e. ran g |-> U. ( `' g " { u } ) ) C_ J )
31 29 30 syl 
 |-  ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) -> ran ( u e. ran g |-> U. ( `' g " { u } ) ) C_ J )
32 eqid 
 |-  U. V = U. V
33 eqid 
 |-  U. U = U. U
34 32 33 refbas 
 |-  ( V Ref U -> U. U = U. V )
35 5 34 syl 
 |-  ( ph -> U. U = U. V )
36 35 ad2antrr 
 |-  ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) -> U. U = U. V )
37 nfv 
 |-  F/ v ( ph /\ g : V --> U )
38 nfra1 
 |-  F/ v A. v e. V v C_ ( g ` v )
39 37 38 nfan 
 |-  F/ v ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) )
40 nfre1 
 |-  F/ v E. v e. V x e. v
41 39 40 nfan 
 |-  F/ v ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ E. v e. V x e. v )
42 ffn 
 |-  ( g : V --> U -> g Fn V )
43 42 ad4antlr 
 |-  ( ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ v e. V ) /\ x e. v ) -> g Fn V )
44 simplr 
 |-  ( ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ v e. V ) /\ x e. v ) -> v e. V )
45 fnfvelrn 
 |-  ( ( g Fn V /\ v e. V ) -> ( g ` v ) e. ran g )
46 43 44 45 syl2anc 
 |-  ( ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ v e. V ) /\ x e. v ) -> ( g ` v ) e. ran g )
47 ssid 
 |-  v C_ v
48 42 ad3antlr 
 |-  ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ v e. V ) -> g Fn V )
49 eqid 
 |-  ( g ` v ) = ( g ` v )
50 fniniseg 
 |-  ( g Fn V -> ( v e. ( `' g " { ( g ` v ) } ) <-> ( v e. V /\ ( g ` v ) = ( g ` v ) ) ) )
51 50 biimpar 
 |-  ( ( g Fn V /\ ( v e. V /\ ( g ` v ) = ( g ` v ) ) ) -> v e. ( `' g " { ( g ` v ) } ) )
52 49 51 mpanr2 
 |-  ( ( g Fn V /\ v e. V ) -> v e. ( `' g " { ( g ` v ) } ) )
53 48 52 sylancom 
 |-  ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ v e. V ) -> v e. ( `' g " { ( g ` v ) } ) )
54 ssuni 
 |-  ( ( v C_ v /\ v e. ( `' g " { ( g ` v ) } ) ) -> v C_ U. ( `' g " { ( g ` v ) } ) )
55 47 53 54 sylancr 
 |-  ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ v e. V ) -> v C_ U. ( `' g " { ( g ` v ) } ) )
56 55 sselda 
 |-  ( ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ v e. V ) /\ x e. v ) -> x e. U. ( `' g " { ( g ` v ) } ) )
57 sneq 
 |-  ( u = ( g ` v ) -> { u } = { ( g ` v ) } )
58 57 imaeq2d 
 |-  ( u = ( g ` v ) -> ( `' g " { u } ) = ( `' g " { ( g ` v ) } ) )
59 58 unieqd 
 |-  ( u = ( g ` v ) -> U. ( `' g " { u } ) = U. ( `' g " { ( g ` v ) } ) )
60 59 eleq2d 
 |-  ( u = ( g ` v ) -> ( x e. U. ( `' g " { u } ) <-> x e. U. ( `' g " { ( g ` v ) } ) ) )
61 60 rspcev 
 |-  ( ( ( g ` v ) e. ran g /\ x e. U. ( `' g " { ( g ` v ) } ) ) -> E. u e. ran g x e. U. ( `' g " { u } ) )
62 46 56 61 syl2anc 
 |-  ( ( ( ( ( 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 } ) )
63 62 adantllr 
 |-  ( ( ( ( ( ( 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 } ) )
64 simpr 
 |-  ( ( ( ( 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 )
65 41 63 64 r19.29af 
 |-  ( ( ( ( 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 } ) )
66 nfv 
 |-  F/ v u e. ran g
67 39 66 nfan 
 |-  F/ v ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ u e. ran g )
68 nfv 
 |-  F/ v x e. U. ( `' g " { u } )
69 67 68 nfan 
 |-  F/ v ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ u e. ran g ) /\ x e. U. ( `' g " { u } ) )
70 24 ad3antrrr 
 |-  ( ( ( ( ( ( ( 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 )
71 simplr 
 |-  ( ( ( ( ( ( ( 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 } ) )
72 70 71 sseldd 
 |-  ( ( ( ( ( ( ( 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 )
73 simpr 
 |-  ( ( ( ( ( ( ( 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 )
74 simpr 
 |-  ( ( ( ( ( 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 } ) )
75 eluni2 
 |-  ( x e. U. ( `' g " { u } ) <-> E. v e. ( `' g " { u } ) x e. v )
76 74 75 sylib 
 |-  ( ( ( ( ( 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 )
77 69 72 73 76 reximd2a 
 |-  ( ( ( ( ( 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 )
78 77 r19.29an 
 |-  ( ( ( ( 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 )
79 65 78 impbida 
 |-  ( ( ( 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 } ) ) )
80 eluni2 
 |-  ( x e. U. V <-> E. v e. V x e. v )
81 eliun 
 |-  ( x e. U_ u e. ran g U. ( `' g " { u } ) <-> E. u e. ran g x e. U. ( `' g " { u } ) )
82 79 80 81 3bitr4g 
 |-  ( ( ( 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 } ) ) )
83 82 eqrdv 
 |-  ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) -> U. V = U_ u e. ran g U. ( `' g " { u } ) )
84 dfiun3g 
 |-  ( 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 } ) ) )
85 29 84 syl 
 |-  ( ( ( 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 } ) ) )
86 36 83 85 3eqtrd 
 |-  ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) -> U. U = U. ran ( u e. ran g |-> U. ( `' g " { u } ) ) )
87 15 ad3antlr 
 |-  ( ( ( ( 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 )
88 vex 
 |-  w e. _V
89 13 elrnmpt 
 |-  ( w e. _V -> ( w e. ran ( u e. ran g |-> U. ( `' g " { u } ) ) <-> E. u e. ran g w = U. ( `' g " { u } ) ) )
90 88 89 mp1i 
 |-  ( ( ( 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 } ) ) )
91 90 biimpa 
 |-  ( ( ( ( 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 } ) )
92 ssrexv 
 |-  ( ran g C_ U -> ( E. u e. ran g w = U. ( `' g " { u } ) -> E. u e. U w = U. ( `' g " { u } ) ) )
93 87 91 92 sylc 
 |-  ( ( ( ( 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 } ) )
94 nfv 
 |-  F/ u ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) )
95 nfmpt1 
 |-  F/_ u ( u e. ran g |-> U. ( `' g " { u } ) )
96 95 nfrn 
 |-  F/_ u ran ( u e. ran g |-> U. ( `' g " { u } ) )
97 96 nfcri 
 |-  F/ u w e. ran ( u e. ran g |-> U. ( `' g " { u } ) )
98 94 97 nfan 
 |-  F/ u ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ w e. ran ( u e. ran g |-> U. ( `' g " { u } ) ) )
99 simpr 
 |-  ( ( ( ( ( ( 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 } ) )
100 nfv 
 |-  F/ v w e. ran ( u e. ran g |-> U. ( `' g " { u } ) )
101 39 100 nfan 
 |-  F/ v ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ w e. ran ( u e. ran g |-> U. ( `' g " { u } ) ) )
102 nfv 
 |-  F/ v u e. U
103 101 102 nfan 
 |-  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 )
104 nfv 
 |-  F/ v w = U. ( `' g " { u } )
105 103 104 nfan 
 |-  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 } ) )
106 simp-5r 
 |-  ( ( ( ( ( ( ( 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 ) )
107 42 ad5antlr 
 |-  ( ( ( ( ( ( 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 )
108 fniniseg 
 |-  ( g Fn V -> ( v e. ( `' g " { u } ) <-> ( v e. V /\ ( g ` v ) = u ) ) )
109 107 108 syl 
 |-  ( ( ( ( ( ( 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 ) ) )
110 109 biimpa 
 |-  ( ( ( ( ( ( ( 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 ) )
111 110 simpld 
 |-  ( ( ( ( ( ( ( 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 )
112 rspa 
 |-  ( ( A. v e. V v C_ ( g ` v ) /\ v e. V ) -> v C_ ( g ` v ) )
113 106 111 112 syl2anc 
 |-  ( ( ( ( ( ( ( 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 ) )
114 110 simprd 
 |-  ( ( ( ( ( ( ( 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 )
115 113 114 sseqtrd 
 |-  ( ( ( ( ( ( ( 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 )
116 115 ex 
 |-  ( ( ( ( ( ( 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 ) )
117 105 116 ralrimi 
 |-  ( ( ( ( ( ( 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 )
118 unissb 
 |-  ( U. ( `' g " { u } ) C_ u <-> A. v e. ( `' g " { u } ) v C_ u )
119 117 118 sylibr 
 |-  ( ( ( ( ( ( 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 )
120 99 119 eqsstrd 
 |-  ( ( ( ( ( ( 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 )
121 120 exp31 
 |-  ( ( ( ( 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 ) ) )
122 98 121 reximdai 
 |-  ( ( ( ( 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 ) )
123 93 122 mpd 
 |-  ( ( ( ( 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 )
124 123 ralrimiva 
 |-  ( ( ( 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 )
125 vex 
 |-  g e. _V
126 125 rnex 
 |-  ran g e. _V
127 126 mptex 
 |-  ( u e. ran g |-> U. ( `' g " { u } ) ) e. _V
128 rnexg 
 |-  ( ( u e. ran g |-> U. ( `' g " { u } ) ) e. _V -> ran ( u e. ran g |-> U. ( `' g " { u } ) ) e. _V )
129 127 128 mp1i 
 |-  ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) -> ran ( u e. ran g |-> U. ( `' g " { u } ) ) e. _V )
130 eqid 
 |-  U. ran ( u e. ran g |-> U. ( `' g " { u } ) ) = U. ran ( u e. ran g |-> U. ( `' g " { u } ) )
131 130 33 isref 
 |-  ( 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 ) ) )
132 129 131 syl 
 |-  ( ( ( 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 ) ) )
133 86 124 132 mpbir2and 
 |-  ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) -> ran ( u e. ran g |-> U. ( `' g " { u } ) ) Ref U )
134 19 ad2antrr 
 |-  ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) -> J e. Top )
135 3 ad2antrr 
 |-  ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) -> X = U. U )
136 135 86 eqtrd 
 |-  ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) -> X = U. ran ( u e. ran g |-> U. ( `' g " { u } ) ) )
137 nfv 
 |-  F/ v x e. X
138 39 137 nfan 
 |-  F/ v ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ x e. X )
139 simplr 
 |-  ( ( ( ( ( ( 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 )
140 ffun 
 |-  ( g : V --> U -> Fun g )
141 140 ad6antlr 
 |-  ( ( ( ( ( ( ( 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 )
142 imafi 
 |-  ( ( Fun g /\ { j e. V | ( j i^i v ) =/= (/) } e. Fin ) -> ( g " { j e. V | ( j i^i v ) =/= (/) } ) e. Fin )
143 141 142 sylancom 
 |-  ( ( ( ( ( ( ( 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 )
144 simp3 
 |-  ( ( ( ( ( ( ( ( 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 ) )
145 sneq 
 |-  ( u = k -> { u } = { k } )
146 145 imaeq2d 
 |-  ( u = k -> ( `' g " { u } ) = ( `' g " { k } ) )
147 146 unieqd 
 |-  ( u = k -> U. ( `' g " { u } ) = U. ( `' g " { k } ) )
148 125 cnvex 
 |-  `' g e. _V
149 imaexg 
 |-  ( `' g e. _V -> ( `' g " { k } ) e. _V )
150 148 149 ax-mp 
 |-  ( `' g " { k } ) e. _V
151 150 uniex 
 |-  U. ( `' g " { k } ) e. _V
152 147 13 151 fvmpt 
 |-  ( k e. ran g -> ( ( u e. ran g |-> U. ( `' g " { u } ) ) ` k ) = U. ( `' g " { k } ) )
153 152 3ad2ant2 
 |-  ( ( ( ( ( ( ( ( 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 } ) )
154 144 153 eqtrd 
 |-  ( ( ( ( ( ( ( ( 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 } ) )
155 154 ineq1d 
 |-  ( ( ( ( ( ( ( ( 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 ) )
156 155 neeq1d 
 |-  ( ( ( ( ( ( ( ( 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 ) =/= (/) ) )
157 126 a1i 
 |-  ( ( ( ( ( ( ( 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 )
158 imaexg 
 |-  ( `' g e. _V -> ( `' g " { u } ) e. _V )
159 148 158 ax-mp 
 |-  ( `' g " { u } ) e. _V
160 159 uniex 
 |-  U. ( `' g " { u } ) e. _V
161 160 13 fnmpti 
 |-  ( u e. ran g |-> U. ( `' g " { u } ) ) Fn ran g
162 dffn4 
 |-  ( ( 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 } ) ) )
163 161 162 mpbi 
 |-  ( u e. ran g |-> U. ( `' g " { u } ) ) : ran g -onto-> ran ( u e. ran g |-> U. ( `' g " { u } ) )
164 163 a1i 
 |-  ( ( ( ( ( ( ( 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 } ) ) )
165 156 157 164 rabfodom 
 |-  ( ( ( ( ( ( ( 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 ) =/= (/) } )
166 sneq 
 |-  ( k = u -> { k } = { u } )
167 166 imaeq2d 
 |-  ( k = u -> ( `' g " { k } ) = ( `' g " { u } ) )
168 167 unieqd 
 |-  ( k = u -> U. ( `' g " { k } ) = U. ( `' g " { u } ) )
169 168 ineq1d 
 |-  ( k = u -> ( U. ( `' g " { k } ) i^i v ) = ( U. ( `' g " { u } ) i^i v ) )
170 169 neeq1d 
 |-  ( k = u -> ( ( U. ( `' g " { k } ) i^i v ) =/= (/) <-> ( U. ( `' g " { u } ) i^i v ) =/= (/) ) )
171 170 cbvrabv 
 |-  { k e. ran g | ( U. ( `' g " { k } ) i^i v ) =/= (/) } = { u e. ran g | ( U. ( `' g " { u } ) i^i v ) =/= (/) }
172 165 171 breqtrdi 
 |-  ( ( ( ( ( ( ( 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 ) =/= (/) } )
173 126 rabex 
 |-  { u e. ran g | E. k e. { j e. V | ( j i^i v ) =/= (/) } ( g ` k ) = u } e. _V
174 nfv 
 |-  F/ j ( ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ x e. X ) /\ v e. J ) /\ x e. v )
175 nfrab1 
 |-  F/_ j { j e. V | ( j i^i v ) =/= (/) }
176 175 nfel1 
 |-  F/ j { j e. V | ( j i^i v ) =/= (/) } e. Fin
177 174 176 nfan 
 |-  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 )
178 nfv 
 |-  F/ j u e. ran g
179 177 178 nfan 
 |-  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 )
180 nfv 
 |-  F/ j ( U. ( `' g " { u } ) i^i v ) =/= (/)
181 179 180 nfan 
 |-  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 ) =/= (/) )
182 nfv 
 |-  F/ j ( g ` k ) = u
183 175 182 nfrex 
 |-  F/ j E. k e. { j e. V | ( j i^i v ) =/= (/) } ( g ` k ) = u
184 42 ad5antlr 
 |-  ( ( ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ x e. X ) /\ v e. J ) /\ x e. v ) -> g Fn V )
185 184 ad5antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( 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 )
186 simplr 
 |-  ( ( ( ( ( ( ( ( ( ( ( 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 } ) )
187 fniniseg 
 |-  ( g Fn V -> ( j e. ( `' g " { u } ) <-> ( j e. V /\ ( g ` j ) = u ) ) )
188 187 biimpa 
 |-  ( ( g Fn V /\ j e. ( `' g " { u } ) ) -> ( j e. V /\ ( g ` j ) = u ) )
189 185 186 188 syl2anc 
 |-  ( ( ( ( ( ( ( ( ( ( ( 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 ) )
190 189 simpld 
 |-  ( ( ( ( ( ( ( ( ( ( ( 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 )
191 simpr 
 |-  ( ( ( ( ( ( ( ( ( ( ( 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 ) =/= (/) )
192 rabid 
 |-  ( j e. { j e. V | ( j i^i v ) =/= (/) } <-> ( j e. V /\ ( j i^i v ) =/= (/) ) )
193 190 191 192 sylanbrc 
 |-  ( ( ( ( ( ( ( ( ( ( ( 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 ) =/= (/) } )
194 189 simprd 
 |-  ( ( ( ( ( ( ( ( ( ( ( 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 )
195 fveqeq2 
 |-  ( k = j -> ( ( g ` k ) = u <-> ( g ` j ) = u ) )
196 195 rspcev 
 |-  ( ( 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 )
197 193 194 196 syl2anc 
 |-  ( ( ( ( ( ( ( ( ( ( ( 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 )
198 uniinn0 
 |-  ( ( U. ( `' g " { u } ) i^i v ) =/= (/) <-> E. j e. ( `' g " { u } ) ( j i^i v ) =/= (/) )
199 198 biimpi 
 |-  ( ( U. ( `' g " { u } ) i^i v ) =/= (/) -> E. j e. ( `' g " { u } ) ( j i^i v ) =/= (/) )
200 199 adantl 
 |-  ( ( ( ( ( ( ( ( ( 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 ) =/= (/) )
201 181 183 197 200 r19.29af2 
 |-  ( ( ( ( ( ( ( ( ( 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 )
202 201 ex 
 |-  ( ( ( ( ( ( ( ( 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 ) )
203 202 ss2rabdv 
 |-  ( ( ( ( ( ( ( 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 } )
204 ssdomg 
 |-  ( { 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 } ) )
205 173 203 204 mpsyl 
 |-  ( ( ( ( ( ( ( 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 } )
206 domtr 
 |-  ( ( { 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 } )
207 172 205 206 syl2anc 
 |-  ( ( ( ( ( ( ( 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 } )
208 184 adantr 
 |-  ( ( ( ( ( ( ( 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 )
209 dffn3 
 |-  ( g Fn V <-> g : V --> ran g )
210 209 biimpi 
 |-  ( g Fn V -> g : V --> ran g )
211 ssrab2 
 |-  { j e. V | ( j i^i v ) =/= (/) } C_ V
212 fimarab 
 |-  ( ( 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 } )
213 211 212 mpan2 
 |-  ( 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 } )
214 208 210 213 3syl 
 |-  ( ( ( ( ( ( ( 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 } )
215 207 214 breqtrrd 
 |-  ( ( ( ( ( ( ( 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 ) =/= (/) } ) )
216 domfi 
 |-  ( ( ( 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 )
217 143 215 216 syl2anc 
 |-  ( ( ( ( ( ( ( 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 )
218 217 ex 
 |-  ( ( ( ( ( ( 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 ) )
219 218 imdistanda 
 |-  ( ( ( ( ( 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 219 imp 
 |-  ( ( ( ( ( ( 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 ) )
221 simplll 
 |-  ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ x e. X ) -> ph )
222 1 32 islocfin 
 |-  ( 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 ) ) )
223 6 222 sylib 
 |-  ( 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 ) ) )
224 223 simp3d 
 |-  ( ph -> A. x e. X E. v e. J ( x e. v /\ { j e. V | ( j i^i v ) =/= (/) } e. Fin ) )
225 224 r19.21bi 
 |-  ( ( ph /\ x e. X ) -> E. v e. J ( x e. v /\ { j e. V | ( j i^i v ) =/= (/) } e. Fin ) )
226 221 225 sylancom 
 |-  ( ( ( ( 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 ) )
227 138 139 220 226 reximd2a 
 |-  ( ( ( ( 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 ) )
228 227 ralrimiva 
 |-  ( ( ( 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 ) )
229 1 130 islocfin 
 |-  ( 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 ) ) )
230 134 136 228 229 syl3anbrc 
 |-  ( ( ( 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 
 |-  ( f = ( u e. ran g |-> U. ( `' g " { u } ) ) -> ( Fun f <-> Fun ( u e. ran g |-> U. ( `' g " { u } ) ) ) )
232 dmeq 
 |-  ( f = ( u e. ran g |-> U. ( `' g " { u } ) ) -> dom f = dom ( u e. ran g |-> U. ( `' g " { u } ) ) )
233 232 sseq1d 
 |-  ( f = ( u e. ran g |-> U. ( `' g " { u } ) ) -> ( dom f C_ U <-> dom ( u e. ran g |-> U. ( `' g " { u } ) ) C_ U ) )
234 rneq 
 |-  ( f = ( u e. ran g |-> U. ( `' g " { u } ) ) -> ran f = ran ( u e. ran g |-> U. ( `' g " { u } ) ) )
235 234 sseq1d 
 |-  ( f = ( u e. ran g |-> U. ( `' g " { u } ) ) -> ( ran f C_ J <-> ran ( u e. ran g |-> U. ( `' g " { u } ) ) C_ J ) )
236 231 233 235 3anbi123d 
 |-  ( 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 ) ) )
237 234 breq1d 
 |-  ( f = ( u e. ran g |-> U. ( `' g " { u } ) ) -> ( ran f Ref U <-> ran ( u e. ran g |-> U. ( `' g " { u } ) ) Ref U ) )
238 234 eleq1d 
 |-  ( f = ( u e. ran g |-> U. ( `' g " { u } ) ) -> ( ran f e. ( LocFin ` J ) <-> ran ( u e. ran g |-> U. ( `' g " { u } ) ) e. ( LocFin ` J ) ) )
239 237 238 anbi12d 
 |-  ( 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 ) ) ) )
240 236 239 anbi12d 
 |-  ( 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 ) ) ) ) )
241 127 240 spcev 
 |-  ( ( ( 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 ) ) ) )
242 12 17 31 133 230 241 syl32anc 
 |-  ( ( ( 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 ) ) ) )
243 242 expl 
 |-  ( 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 ) ) ) ) )
244 243 exlimdv 
 |-  ( 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 ) ) ) ) )
245 10 244 mpd 
 |-  ( ph -> E. f ( ( Fun f /\ dom f C_ U /\ ran f C_ J ) /\ ( ran f Ref U /\ ran f e. ( LocFin ` J ) ) ) )