Metamath Proof Explorer

Theorem locfinref

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. (Contributed by Thierry Arnoux, 31-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 locfinref 
|- ( ph -> E. f ( f : U --> 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 f0 
 |-  (/) : (/) --> J
8 simpr 
 |-  ( ( ph /\ U = (/) ) -> U = (/) )
9 8 feq2d 
 |-  ( ( ph /\ U = (/) ) -> ( (/) : U --> J <-> (/) : (/) --> J ) )
10 7 9 mpbiri 
 |-  ( ( ph /\ U = (/) ) -> (/) : U --> J )
11 rn0 
 |-  ran (/) = (/)
12 0ex 
 |-  (/) e. _V
13 refref 
 |-  ( (/) e. _V -> (/) Ref (/) )
14 12 13 ax-mp 
 |-  (/) Ref (/)
15 11 14 eqbrtri 
 |-  ran (/) Ref (/)
16 15 8 breqtrrid 
 |-  ( ( ph /\ U = (/) ) -> ran (/) Ref U )
17 sn0top 
 |-  { (/) } e. Top
18 17 a1i 
 |-  ( ( ph /\ U = (/) ) -> { (/) } e. Top )
19 eqidd 
 |-  ( ( ph /\ U = (/) ) -> (/) = (/) )
20 ral0 
 |-  A. x e. (/) E. n e. { (/) } ( x e. n /\ { s e. ran (/) | ( s i^i n ) =/= (/) } e. Fin )
21 20 a1i 
 |-  ( ( ph /\ U = (/) ) -> A. x e. (/) E. n e. { (/) } ( x e. n /\ { s e. ran (/) | ( s i^i n ) =/= (/) } e. Fin ) )
22 12 unisn 
 |-  U. { (/) } = (/)
23 22 eqcomi 
 |-  (/) = U. { (/) }
24 11 unieqi 
 |-  U. ran (/) = U. (/)
25 uni0 
 |-  U. (/) = (/)
26 24 25 eqtr2i 
 |-  (/) = U. ran (/)
27 23 26 islocfin 
 |-  ( ran (/) e. ( LocFin ` { (/) } ) <-> ( { (/) } e. Top /\ (/) = (/) /\ A. x e. (/) E. n e. { (/) } ( x e. n /\ { s e. ran (/) | ( s i^i n ) =/= (/) } e. Fin ) ) )
28 18 19 21 27 syl3anbrc 
 |-  ( ( ph /\ U = (/) ) -> ran (/) e. ( LocFin ` { (/) } ) )
29 3 adantr 
 |-  ( ( ph /\ U = (/) ) -> X = U. U )
30 8 unieqd 
 |-  ( ( ph /\ U = (/) ) -> U. U = U. (/) )
31 29 30 eqtrd 
 |-  ( ( ph /\ U = (/) ) -> X = U. (/) )
32 31 1 25 3eqtr3g 
 |-  ( ( ph /\ U = (/) ) -> U. J = (/) )
33 locfintop 
 |-  ( V e. ( LocFin ` J ) -> J e. Top )
34 0top 
 |-  ( J e. Top -> ( U. J = (/) <-> J = { (/) } ) )
35 6 33 34 3syl 
 |-  ( ph -> ( U. J = (/) <-> J = { (/) } ) )
36 35 adantr 
 |-  ( ( ph /\ U = (/) ) -> ( U. J = (/) <-> J = { (/) } ) )
37 32 36 mpbid 
 |-  ( ( ph /\ U = (/) ) -> J = { (/) } )
38 37 fveq2d 
 |-  ( ( ph /\ U = (/) ) -> ( LocFin ` J ) = ( LocFin ` { (/) } ) )
39 28 38 eleqtrrd 
 |-  ( ( ph /\ U = (/) ) -> ran (/) e. ( LocFin ` J ) )
40 feq1 
 |-  ( f = (/) -> ( f : U --> J <-> (/) : U --> J ) )
41 rneq 
 |-  ( f = (/) -> ran f = ran (/) )
42 41 breq1d 
 |-  ( f = (/) -> ( ran f Ref U <-> ran (/) Ref U ) )
43 41 eleq1d 
 |-  ( f = (/) -> ( ran f e. ( LocFin ` J ) <-> ran (/) e. ( LocFin ` J ) ) )
44 40 42 43 3anbi123d 
 |-  ( f = (/) -> ( ( f : U --> J /\ ran f Ref U /\ ran f e. ( LocFin ` J ) ) <-> ( (/) : U --> J /\ ran (/) Ref U /\ ran (/) e. ( LocFin ` J ) ) ) )
45 12 44 spcev 
 |-  ( ( (/) : U --> J /\ ran (/) Ref U /\ ran (/) e. ( LocFin ` J ) ) -> E. f ( f : U --> J /\ ran f Ref U /\ ran f e. ( LocFin ` J ) ) )
46 10 16 39 45 syl3anc 
 |-  ( ( ph /\ U = (/) ) -> E. f ( f : U --> J /\ ran f Ref U /\ ran f e. ( LocFin ` J ) ) )
47 1 2 3 4 5 6 locfinreflem 
 |-  ( ph -> E. g ( ( Fun g /\ dom g C_ U /\ ran g C_ J ) /\ ( ran g Ref U /\ ran g e. ( LocFin ` J ) ) ) )
48 47 adantr 
 |-  ( ( ph /\ U =/= (/) ) -> E. g ( ( Fun g /\ dom g C_ U /\ ran g C_ J ) /\ ( ran g Ref U /\ ran g e. ( LocFin ` J ) ) ) )
49 simpl 
 |-  ( ( ( ph /\ U =/= (/) ) /\ ( ( Fun g /\ dom g C_ U /\ ran g C_ J ) /\ ( ran g Ref U /\ ran g e. ( LocFin ` J ) ) ) ) -> ( ph /\ U =/= (/) ) )
50 simprl1 
 |-  ( ( ( ph /\ U =/= (/) ) /\ ( ( Fun g /\ dom g C_ U /\ ran g C_ J ) /\ ( ran g Ref U /\ ran g e. ( LocFin ` J ) ) ) ) -> Fun g )
51 fdmrn 
 |-  ( Fun g <-> g : dom g --> ran g )
52 50 51 sylib 
 |-  ( ( ( ph /\ U =/= (/) ) /\ ( ( Fun g /\ dom g C_ U /\ ran g C_ J ) /\ ( ran g Ref U /\ ran g e. ( LocFin ` J ) ) ) ) -> g : dom g --> ran g )
53 simprl3 
 |-  ( ( ( ph /\ U =/= (/) ) /\ ( ( Fun g /\ dom g C_ U /\ ran g C_ J ) /\ ( ran g Ref U /\ ran g e. ( LocFin ` J ) ) ) ) -> ran g C_ J )
54 52 53 fssd 
 |-  ( ( ( ph /\ U =/= (/) ) /\ ( ( Fun g /\ dom g C_ U /\ ran g C_ J ) /\ ( ran g Ref U /\ ran g e. ( LocFin ` J ) ) ) ) -> g : dom g --> J )
55 fconstg 
 |-  ( (/) e. _V -> ( ( U \ dom g ) X. { (/) } ) : ( U \ dom g ) --> { (/) } )
56 12 55 mp1i 
 |-  ( ( ( ph /\ U =/= (/) ) /\ ( ( Fun g /\ dom g C_ U /\ ran g C_ J ) /\ ( ran g Ref U /\ ran g e. ( LocFin ` J ) ) ) ) -> ( ( U \ dom g ) X. { (/) } ) : ( U \ dom g ) --> { (/) } )
57 0opn 
 |-  ( J e. Top -> (/) e. J )
58 6 33 57 3syl 
 |-  ( ph -> (/) e. J )
59 58 ad2antrr 
 |-  ( ( ( ph /\ U =/= (/) ) /\ ( ( Fun g /\ dom g C_ U /\ ran g C_ J ) /\ ( ran g Ref U /\ ran g e. ( LocFin ` J ) ) ) ) -> (/) e. J )
60 59 snssd 
 |-  ( ( ( ph /\ U =/= (/) ) /\ ( ( Fun g /\ dom g C_ U /\ ran g C_ J ) /\ ( ran g Ref U /\ ran g e. ( LocFin ` J ) ) ) ) -> { (/) } C_ J )
61 56 60 fssd 
 |-  ( ( ( ph /\ U =/= (/) ) /\ ( ( Fun g /\ dom g C_ U /\ ran g C_ J ) /\ ( ran g Ref U /\ ran g e. ( LocFin ` J ) ) ) ) -> ( ( U \ dom g ) X. { (/) } ) : ( U \ dom g ) --> J )
62 disjdif 
 |-  ( dom g i^i ( U \ dom g ) ) = (/)
63 62 a1i 
 |-  ( ( ( ph /\ U =/= (/) ) /\ ( ( Fun g /\ dom g C_ U /\ ran g C_ J ) /\ ( ran g Ref U /\ ran g e. ( LocFin ` J ) ) ) ) -> ( dom g i^i ( U \ dom g ) ) = (/) )
64 fun2 
 |-  ( ( ( g : dom g --> J /\ ( ( U \ dom g ) X. { (/) } ) : ( U \ dom g ) --> J ) /\ ( dom g i^i ( U \ dom g ) ) = (/) ) -> ( g u. ( ( U \ dom g ) X. { (/) } ) ) : ( dom g u. ( U \ dom g ) ) --> J )
65 54 61 63 64 syl21anc 
 |-  ( ( ( ph /\ U =/= (/) ) /\ ( ( Fun g /\ dom g C_ U /\ ran g C_ J ) /\ ( ran g Ref U /\ ran g e. ( LocFin ` J ) ) ) ) -> ( g u. ( ( U \ dom g ) X. { (/) } ) ) : ( dom g u. ( U \ dom g ) ) --> J )
66 simprl2 
 |-  ( ( ( ph /\ U =/= (/) ) /\ ( ( Fun g /\ dom g C_ U /\ ran g C_ J ) /\ ( ran g Ref U /\ ran g e. ( LocFin ` J ) ) ) ) -> dom g C_ U )
67 undif 
 |-  ( dom g C_ U <-> ( dom g u. ( U \ dom g ) ) = U )
68 66 67 sylib 
 |-  ( ( ( ph /\ U =/= (/) ) /\ ( ( Fun g /\ dom g C_ U /\ ran g C_ J ) /\ ( ran g Ref U /\ ran g e. ( LocFin ` J ) ) ) ) -> ( dom g u. ( U \ dom g ) ) = U )
69 68 feq2d 
 |-  ( ( ( ph /\ U =/= (/) ) /\ ( ( Fun g /\ dom g C_ U /\ ran g C_ J ) /\ ( ran g Ref U /\ ran g e. ( LocFin ` J ) ) ) ) -> ( ( g u. ( ( U \ dom g ) X. { (/) } ) ) : ( dom g u. ( U \ dom g ) ) --> J <-> ( g u. ( ( U \ dom g ) X. { (/) } ) ) : U --> J ) )
70 65 69 mpbid 
 |-  ( ( ( ph /\ U =/= (/) ) /\ ( ( Fun g /\ dom g C_ U /\ ran g C_ J ) /\ ( ran g Ref U /\ ran g e. ( LocFin ` J ) ) ) ) -> ( g u. ( ( U \ dom g ) X. { (/) } ) ) : U --> J )
71 simpr 
 |-  ( ( ( ( ph /\ U =/= (/) ) /\ ( ( Fun g /\ dom g C_ U /\ ran g C_ J ) /\ ( ran g Ref U /\ ran g e. ( LocFin ` J ) ) ) ) /\ ran ( g u. ( ( U \ dom g ) X. { (/) } ) ) = ran g ) -> ran ( g u. ( ( U \ dom g ) X. { (/) } ) ) = ran g )
72 simprrl 
 |-  ( ( ( ph /\ U =/= (/) ) /\ ( ( Fun g /\ dom g C_ U /\ ran g C_ J ) /\ ( ran g Ref U /\ ran g e. ( LocFin ` J ) ) ) ) -> ran g Ref U )
73 72 adantr 
 |-  ( ( ( ( ph /\ U =/= (/) ) /\ ( ( Fun g /\ dom g C_ U /\ ran g C_ J ) /\ ( ran g Ref U /\ ran g e. ( LocFin ` J ) ) ) ) /\ ran ( g u. ( ( U \ dom g ) X. { (/) } ) ) = ran g ) -> ran g Ref U )
74 71 73 eqbrtrd 
 |-  ( ( ( ( ph /\ U =/= (/) ) /\ ( ( Fun g /\ dom g C_ U /\ ran g C_ J ) /\ ( ran g Ref U /\ ran g e. ( LocFin ` J ) ) ) ) /\ ran ( g u. ( ( U \ dom g ) X. { (/) } ) ) = ran g ) -> ran ( g u. ( ( U \ dom g ) X. { (/) } ) ) Ref U )
75 simpr 
 |-  ( ( ( ( ph /\ U =/= (/) ) /\ ( ( Fun g /\ dom g C_ U /\ ran g C_ J ) /\ ( ran g Ref U /\ ran g e. ( LocFin ` J ) ) ) ) /\ ran ( g u. ( ( U \ dom g ) X. { (/) } ) ) = ( ran g u. { (/) } ) ) -> ran ( g u. ( ( U \ dom g ) X. { (/) } ) ) = ( ran g u. { (/) } ) )
76 49 simprd 
 |-  ( ( ( ph /\ U =/= (/) ) /\ ( ( Fun g /\ dom g C_ U /\ ran g C_ J ) /\ ( ran g Ref U /\ ran g e. ( LocFin ` J ) ) ) ) -> U =/= (/) )
77 refun0 
 |-  ( ( ran g Ref U /\ U =/= (/) ) -> ( ran g u. { (/) } ) Ref U )
78 72 76 77 syl2anc 
 |-  ( ( ( ph /\ U =/= (/) ) /\ ( ( Fun g /\ dom g C_ U /\ ran g C_ J ) /\ ( ran g Ref U /\ ran g e. ( LocFin ` J ) ) ) ) -> ( ran g u. { (/) } ) Ref U )
79 78 adantr 
 |-  ( ( ( ( ph /\ U =/= (/) ) /\ ( ( Fun g /\ dom g C_ U /\ ran g C_ J ) /\ ( ran g Ref U /\ ran g e. ( LocFin ` J ) ) ) ) /\ ran ( g u. ( ( U \ dom g ) X. { (/) } ) ) = ( ran g u. { (/) } ) ) -> ( ran g u. { (/) } ) Ref U )
80 75 79 eqbrtrd 
 |-  ( ( ( ( ph /\ U =/= (/) ) /\ ( ( Fun g /\ dom g C_ U /\ ran g C_ J ) /\ ( ran g Ref U /\ ran g e. ( LocFin ` J ) ) ) ) /\ ran ( g u. ( ( U \ dom g ) X. { (/) } ) ) = ( ran g u. { (/) } ) ) -> ran ( g u. ( ( U \ dom g ) X. { (/) } ) ) Ref U )
81 rnxpss 
 |-  ran ( ( U \ dom g ) X. { (/) } ) C_ { (/) }
82 sssn 
 |-  ( ran ( ( U \ dom g ) X. { (/) } ) C_ { (/) } <-> ( ran ( ( U \ dom g ) X. { (/) } ) = (/) \/ ran ( ( U \ dom g ) X. { (/) } ) = { (/) } ) )
83 81 82 mpbi 
 |-  ( ran ( ( U \ dom g ) X. { (/) } ) = (/) \/ ran ( ( U \ dom g ) X. { (/) } ) = { (/) } )
84 rnun 
 |-  ran ( g u. ( ( U \ dom g ) X. { (/) } ) ) = ( ran g u. ran ( ( U \ dom g ) X. { (/) } ) )
85 uneq2 
 |-  ( ran ( ( U \ dom g ) X. { (/) } ) = (/) -> ( ran g u. ran ( ( U \ dom g ) X. { (/) } ) ) = ( ran g u. (/) ) )
86 84 85 syl5eq 
 |-  ( ran ( ( U \ dom g ) X. { (/) } ) = (/) -> ran ( g u. ( ( U \ dom g ) X. { (/) } ) ) = ( ran g u. (/) ) )
87 un0 
 |-  ( ran g u. (/) ) = ran g
88 86 87 eqtrdi 
 |-  ( ran ( ( U \ dom g ) X. { (/) } ) = (/) -> ran ( g u. ( ( U \ dom g ) X. { (/) } ) ) = ran g )
89 uneq2 
 |-  ( ran ( ( U \ dom g ) X. { (/) } ) = { (/) } -> ( ran g u. ran ( ( U \ dom g ) X. { (/) } ) ) = ( ran g u. { (/) } ) )
90 84 89 syl5eq 
 |-  ( ran ( ( U \ dom g ) X. { (/) } ) = { (/) } -> ran ( g u. ( ( U \ dom g ) X. { (/) } ) ) = ( ran g u. { (/) } ) )
91 88 90 orim12i 
 |-  ( ( ran ( ( U \ dom g ) X. { (/) } ) = (/) \/ ran ( ( U \ dom g ) X. { (/) } ) = { (/) } ) -> ( ran ( g u. ( ( U \ dom g ) X. { (/) } ) ) = ran g \/ ran ( g u. ( ( U \ dom g ) X. { (/) } ) ) = ( ran g u. { (/) } ) ) )
92 83 91 mp1i 
 |-  ( ( ( ph /\ U =/= (/) ) /\ ( ( Fun g /\ dom g C_ U /\ ran g C_ J ) /\ ( ran g Ref U /\ ran g e. ( LocFin ` J ) ) ) ) -> ( ran ( g u. ( ( U \ dom g ) X. { (/) } ) ) = ran g \/ ran ( g u. ( ( U \ dom g ) X. { (/) } ) ) = ( ran g u. { (/) } ) ) )
93 74 80 92 mpjaodan 
 |-  ( ( ( ph /\ U =/= (/) ) /\ ( ( Fun g /\ dom g C_ U /\ ran g C_ J ) /\ ( ran g Ref U /\ ran g e. ( LocFin ` J ) ) ) ) -> ran ( g u. ( ( U \ dom g ) X. { (/) } ) ) Ref U )
94 simprrr 
 |-  ( ( ( ph /\ U =/= (/) ) /\ ( ( Fun g /\ dom g C_ U /\ ran g C_ J ) /\ ( ran g Ref U /\ ran g e. ( LocFin ` J ) ) ) ) -> ran g e. ( LocFin ` J ) )
95 94 adantr 
 |-  ( ( ( ( ph /\ U =/= (/) ) /\ ( ( Fun g /\ dom g C_ U /\ ran g C_ J ) /\ ( ran g Ref U /\ ran g e. ( LocFin ` J ) ) ) ) /\ ran ( g u. ( ( U \ dom g ) X. { (/) } ) ) = ran g ) -> ran g e. ( LocFin ` J ) )
96 71 95 eqeltrd 
 |-  ( ( ( ( ph /\ U =/= (/) ) /\ ( ( Fun g /\ dom g C_ U /\ ran g C_ J ) /\ ( ran g Ref U /\ ran g e. ( LocFin ` J ) ) ) ) /\ ran ( g u. ( ( U \ dom g ) X. { (/) } ) ) = ran g ) -> ran ( g u. ( ( U \ dom g ) X. { (/) } ) ) e. ( LocFin ` J ) )
97 94 adantr 
 |-  ( ( ( ( ph /\ U =/= (/) ) /\ ( ( Fun g /\ dom g C_ U /\ ran g C_ J ) /\ ( ran g Ref U /\ ran g e. ( LocFin ` J ) ) ) ) /\ ran ( g u. ( ( U \ dom g ) X. { (/) } ) ) = ( ran g u. { (/) } ) ) -> ran g e. ( LocFin ` J ) )
98 snfi 
 |-  { (/) } e. Fin
99 98 a1i 
 |-  ( ( ( ( ph /\ U =/= (/) ) /\ ( ( Fun g /\ dom g C_ U /\ ran g C_ J ) /\ ( ran g Ref U /\ ran g e. ( LocFin ` J ) ) ) ) /\ ran ( g u. ( ( U \ dom g ) X. { (/) } ) ) = ( ran g u. { (/) } ) ) -> { (/) } e. Fin )
100 59 adantr 
 |-  ( ( ( ( ph /\ U =/= (/) ) /\ ( ( Fun g /\ dom g C_ U /\ ran g C_ J ) /\ ( ran g Ref U /\ ran g e. ( LocFin ` J ) ) ) ) /\ ran ( g u. ( ( U \ dom g ) X. { (/) } ) ) = ( ran g u. { (/) } ) ) -> (/) e. J )
101 100 snssd 
 |-  ( ( ( ( ph /\ U =/= (/) ) /\ ( ( Fun g /\ dom g C_ U /\ ran g C_ J ) /\ ( ran g Ref U /\ ran g e. ( LocFin ` J ) ) ) ) /\ ran ( g u. ( ( U \ dom g ) X. { (/) } ) ) = ( ran g u. { (/) } ) ) -> { (/) } C_ J )
102 101 unissd 
 |-  ( ( ( ( ph /\ U =/= (/) ) /\ ( ( Fun g /\ dom g C_ U /\ ran g C_ J ) /\ ( ran g Ref U /\ ran g e. ( LocFin ` J ) ) ) ) /\ ran ( g u. ( ( U \ dom g ) X. { (/) } ) ) = ( ran g u. { (/) } ) ) -> U. { (/) } C_ U. J )
103 lfinun 
 |-  ( ( ran g e. ( LocFin ` J ) /\ { (/) } e. Fin /\ U. { (/) } C_ U. J ) -> ( ran g u. { (/) } ) e. ( LocFin ` J ) )
104 97 99 102 103 syl3anc 
 |-  ( ( ( ( ph /\ U =/= (/) ) /\ ( ( Fun g /\ dom g C_ U /\ ran g C_ J ) /\ ( ran g Ref U /\ ran g e. ( LocFin ` J ) ) ) ) /\ ran ( g u. ( ( U \ dom g ) X. { (/) } ) ) = ( ran g u. { (/) } ) ) -> ( ran g u. { (/) } ) e. ( LocFin ` J ) )
105 75 104 eqeltrd 
 |-  ( ( ( ( ph /\ U =/= (/) ) /\ ( ( Fun g /\ dom g C_ U /\ ran g C_ J ) /\ ( ran g Ref U /\ ran g e. ( LocFin ` J ) ) ) ) /\ ran ( g u. ( ( U \ dom g ) X. { (/) } ) ) = ( ran g u. { (/) } ) ) -> ran ( g u. ( ( U \ dom g ) X. { (/) } ) ) e. ( LocFin ` J ) )
106 96 105 92 mpjaodan 
 |-  ( ( ( ph /\ U =/= (/) ) /\ ( ( Fun g /\ dom g C_ U /\ ran g C_ J ) /\ ( ran g Ref U /\ ran g e. ( LocFin ` J ) ) ) ) -> ran ( g u. ( ( U \ dom g ) X. { (/) } ) ) e. ( LocFin ` J ) )
107 refrel 
 |-  Rel Ref
108 107 brrelex2i 
 |-  ( V Ref U -> U e. _V )
109 difexg 
 |-  ( U e. _V -> ( U \ dom g ) e. _V )
110 5 108 109 3syl 
 |-  ( ph -> ( U \ dom g ) e. _V )
111 110 adantr 
 |-  ( ( ph /\ U =/= (/) ) -> ( U \ dom g ) e. _V )
112 p0ex 
 |-  { (/) } e. _V
113 xpexg 
 |-  ( ( ( U \ dom g ) e. _V /\ { (/) } e. _V ) -> ( ( U \ dom g ) X. { (/) } ) e. _V )
114 112 113 mpan2 
 |-  ( ( U \ dom g ) e. _V -> ( ( U \ dom g ) X. { (/) } ) e. _V )
115 vex 
 |-  g e. _V
116 unexg 
 |-  ( ( g e. _V /\ ( ( U \ dom g ) X. { (/) } ) e. _V ) -> ( g u. ( ( U \ dom g ) X. { (/) } ) ) e. _V )
117 115 116 mpan 
 |-  ( ( ( U \ dom g ) X. { (/) } ) e. _V -> ( g u. ( ( U \ dom g ) X. { (/) } ) ) e. _V )
118 feq1 
 |-  ( f = ( g u. ( ( U \ dom g ) X. { (/) } ) ) -> ( f : U --> J <-> ( g u. ( ( U \ dom g ) X. { (/) } ) ) : U --> J ) )
119 rneq 
 |-  ( f = ( g u. ( ( U \ dom g ) X. { (/) } ) ) -> ran f = ran ( g u. ( ( U \ dom g ) X. { (/) } ) ) )
120 119 breq1d 
 |-  ( f = ( g u. ( ( U \ dom g ) X. { (/) } ) ) -> ( ran f Ref U <-> ran ( g u. ( ( U \ dom g ) X. { (/) } ) ) Ref U ) )
121 119 eleq1d 
 |-  ( f = ( g u. ( ( U \ dom g ) X. { (/) } ) ) -> ( ran f e. ( LocFin ` J ) <-> ran ( g u. ( ( U \ dom g ) X. { (/) } ) ) e. ( LocFin ` J ) ) )
122 118 120 121 3anbi123d 
 |-  ( f = ( g u. ( ( U \ dom g ) X. { (/) } ) ) -> ( ( f : U --> J /\ ran f Ref U /\ ran f e. ( LocFin ` J ) ) <-> ( ( g u. ( ( U \ dom g ) X. { (/) } ) ) : U --> J /\ ran ( g u. ( ( U \ dom g ) X. { (/) } ) ) Ref U /\ ran ( g u. ( ( U \ dom g ) X. { (/) } ) ) e. ( LocFin ` J ) ) ) )
123 122 spcegv 
 |-  ( ( g u. ( ( U \ dom g ) X. { (/) } ) ) e. _V -> ( ( ( g u. ( ( U \ dom g ) X. { (/) } ) ) : U --> J /\ ran ( g u. ( ( U \ dom g ) X. { (/) } ) ) Ref U /\ ran ( g u. ( ( U \ dom g ) X. { (/) } ) ) e. ( LocFin ` J ) ) -> E. f ( f : U --> J /\ ran f Ref U /\ ran f e. ( LocFin ` J ) ) ) )
124 111 114 117 123 4syl 
 |-  ( ( ph /\ U =/= (/) ) -> ( ( ( g u. ( ( U \ dom g ) X. { (/) } ) ) : U --> J /\ ran ( g u. ( ( U \ dom g ) X. { (/) } ) ) Ref U /\ ran ( g u. ( ( U \ dom g ) X. { (/) } ) ) e. ( LocFin ` J ) ) -> E. f ( f : U --> J /\ ran f Ref U /\ ran f e. ( LocFin ` J ) ) ) )
125 124 imp 
 |-  ( ( ( ph /\ U =/= (/) ) /\ ( ( g u. ( ( U \ dom g ) X. { (/) } ) ) : U --> J /\ ran ( g u. ( ( U \ dom g ) X. { (/) } ) ) Ref U /\ ran ( g u. ( ( U \ dom g ) X. { (/) } ) ) e. ( LocFin ` J ) ) ) -> E. f ( f : U --> J /\ ran f Ref U /\ ran f e. ( LocFin ` J ) ) )
126 49 70 93 106 125 syl13anc 
 |-  ( ( ( ph /\ U =/= (/) ) /\ ( ( Fun g /\ dom g C_ U /\ ran g C_ J ) /\ ( ran g Ref U /\ ran g e. ( LocFin ` J ) ) ) ) -> E. f ( f : U --> J /\ ran f Ref U /\ ran f e. ( LocFin ` J ) ) )
127 48 126 exlimddv 
 |-  ( ( ph /\ U =/= (/) ) -> E. f ( f : U --> J /\ ran f Ref U /\ ran f e. ( LocFin ` J ) ) )
128 46 127 pm2.61dane 
 |-  ( ph -> E. f ( f : U --> J /\ ran f Ref U /\ ran f e. ( LocFin ` J ) ) )