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 ⊢ 𝑋 = ∪ 𝐽
locfinref.1 ⊢ ( 𝜑 → 𝑈 ⊆ 𝐽 )
locfinref.2 ⊢ ( 𝜑 → 𝑋 = ∪ 𝑈 )
locfinref.3 ⊢ ( 𝜑 → 𝑉 ⊆ 𝐽 )
locfinref.4 ⊢ ( 𝜑 → 𝑉 Ref 𝑈 )
locfinref.5 ⊢ ( 𝜑 → 𝑉 ∈ ( LocFin ‘ 𝐽 ) )
Assertion locfinref ( 𝜑 → ∃ 𝑓 ( 𝑓 : 𝑈 ⟶ 𝐽 ∧ ran 𝑓 Ref 𝑈 ∧ ran 𝑓 ∈ ( LocFin ‘ 𝐽 ) ) )

Proof

Step Hyp Ref Expression
1 locfinref.x ⊢ 𝑋 = ∪ 𝐽
2 locfinref.1 ⊢ ( 𝜑 → 𝑈 ⊆ 𝐽 )
3 locfinref.2 ⊢ ( 𝜑 → 𝑋 = ∪ 𝑈 )
4 locfinref.3 ⊢ ( 𝜑 → 𝑉 ⊆ 𝐽 )
5 locfinref.4 ⊢ ( 𝜑 → 𝑉 Ref 𝑈 )
6 locfinref.5 ⊢ ( 𝜑 → 𝑉 ∈ ( LocFin ‘ 𝐽 ) )
7 f0 ⊢ ∅ : ∅ ⟶ 𝐽
8 simpr ⊢ ( ( 𝜑 ∧ 𝑈 = ∅ ) → 𝑈 = ∅ )
9 8 feq2d ⊢ ( ( 𝜑 ∧ 𝑈 = ∅ ) → ( ∅ : 𝑈 ⟶ 𝐽 ↔ ∅ : ∅ ⟶ 𝐽 ) )
10 7 9 mpbiri ⊢ ( ( 𝜑 ∧ 𝑈 = ∅ ) → ∅ : 𝑈 ⟶ 𝐽 )
11 rn0 ⊢ ran ∅ = ∅
12 0ex ⊢ ∅ ∈ V
13 refref ⊢ ( ∅ ∈ V → ∅ Ref ∅ )
14 12 13 ax-mp ⊢ ∅ Ref ∅
15 11 14 eqbrtri ⊢ ran ∅ Ref ∅
16 15 8 breqtrrid ⊢ ( ( 𝜑 ∧ 𝑈 = ∅ ) → ran ∅ Ref 𝑈 )
17 sn0top ⊢ { ∅ } ∈ Top
18 17 a1i ⊢ ( ( 𝜑 ∧ 𝑈 = ∅ ) → { ∅ } ∈ Top )
19 eqidd ⊢ ( ( 𝜑 ∧ 𝑈 = ∅ ) → ∅ = ∅ )
20 ral0 ⊢ ∀ 𝑥 ∈ ∅ ∃ 𝑛 ∈ { ∅ } ( 𝑥 ∈ 𝑛 ∧ { 𝑠 ∈ ran ∅ ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin )
21 20 a1i ⊢ ( ( 𝜑 ∧ 𝑈 = ∅ ) → ∀ 𝑥 ∈ ∅ ∃ 𝑛 ∈ { ∅ } ( 𝑥 ∈ 𝑛 ∧ { 𝑠 ∈ ran ∅ ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) )
22 12 unisn ⊢ ∪ { ∅ } = ∅
23 22 eqcomi ⊢ ∅ = ∪ { ∅ }
24 11 unieqi ⊢ ∪ ran ∅ = ∪ ∅
25 uni0 ⊢ ∪ ∅ = ∅
26 24 25 eqtr2i ⊢ ∅ = ∪ ran ∅
27 23 26 islocfin ⊢ ( ran ∅ ∈ ( LocFin ‘ { ∅ } ) ↔ ( { ∅ } ∈ Top ∧ ∅ = ∅ ∧ ∀ 𝑥 ∈ ∅ ∃ 𝑛 ∈ { ∅ } ( 𝑥 ∈ 𝑛 ∧ { 𝑠 ∈ ran ∅ ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) ) )
28 18 19 21 27 syl3anbrc ⊢ ( ( 𝜑 ∧ 𝑈 = ∅ ) → ran ∅ ∈ ( LocFin ‘ { ∅ } ) )
29 3 adantr ⊢ ( ( 𝜑 ∧ 𝑈 = ∅ ) → 𝑋 = ∪ 𝑈 )
30 8 unieqd ⊢ ( ( 𝜑 ∧ 𝑈 = ∅ ) → ∪ 𝑈 = ∪ ∅ )
31 29 30 eqtrd ⊢ ( ( 𝜑 ∧ 𝑈 = ∅ ) → 𝑋 = ∪ ∅ )
32 31 1 25 3eqtr3g ⊢ ( ( 𝜑 ∧ 𝑈 = ∅ ) → ∪ 𝐽 = ∅ )
33 locfintop ⊢ ( 𝑉 ∈ ( LocFin ‘ 𝐽 ) → 𝐽 ∈ Top )
34 0top ⊢ ( 𝐽 ∈ Top → ( ∪ 𝐽 = ∅ ↔ 𝐽 = { ∅ } ) )
35 6 33 34 3syl ⊢ ( 𝜑 → ( ∪ 𝐽 = ∅ ↔ 𝐽 = { ∅ } ) )
36 35 adantr ⊢ ( ( 𝜑 ∧ 𝑈 = ∅ ) → ( ∪ 𝐽 = ∅ ↔ 𝐽 = { ∅ } ) )
37 32 36 mpbid ⊢ ( ( 𝜑 ∧ 𝑈 = ∅ ) → 𝐽 = { ∅ } )
38 37 fveq2d ⊢ ( ( 𝜑 ∧ 𝑈 = ∅ ) → ( LocFin ‘ 𝐽 ) = ( LocFin ‘ { ∅ } ) )
39 28 38 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑈 = ∅ ) → ran ∅ ∈ ( LocFin ‘ 𝐽 ) )
40 feq1 ⊢ ( 𝑓 = ∅ → ( 𝑓 : 𝑈 ⟶ 𝐽 ↔ ∅ : 𝑈 ⟶ 𝐽 ) )
41 rneq ⊢ ( 𝑓 = ∅ → ran 𝑓 = ran ∅ )
42 41 breq1d ⊢ ( 𝑓 = ∅ → ( ran 𝑓 Ref 𝑈 ↔ ran ∅ Ref 𝑈 ) )
43 41 eleq1d ⊢ ( 𝑓 = ∅ → ( ran 𝑓 ∈ ( LocFin ‘ 𝐽 ) ↔ ran ∅ ∈ ( LocFin ‘ 𝐽 ) ) )
44 40 42 43 3anbi123d ⊢ ( 𝑓 = ∅ → ( ( 𝑓 : 𝑈 ⟶ 𝐽 ∧ ran 𝑓 Ref 𝑈 ∧ ran 𝑓 ∈ ( LocFin ‘ 𝐽 ) ) ↔ ( ∅ : 𝑈 ⟶ 𝐽 ∧ ran ∅ Ref 𝑈 ∧ ran ∅ ∈ ( LocFin ‘ 𝐽 ) ) ) )
45 12 44 spcev ⊢ ( ( ∅ : 𝑈 ⟶ 𝐽 ∧ ran ∅ Ref 𝑈 ∧ ran ∅ ∈ ( LocFin ‘ 𝐽 ) ) → ∃ 𝑓 ( 𝑓 : 𝑈 ⟶ 𝐽 ∧ ran 𝑓 Ref 𝑈 ∧ ran 𝑓 ∈ ( LocFin ‘ 𝐽 ) ) )
46 10 16 39 45 syl3anc ⊢ ( ( 𝜑 ∧ 𝑈 = ∅ ) → ∃ 𝑓 ( 𝑓 : 𝑈 ⟶ 𝐽 ∧ ran 𝑓 Ref 𝑈 ∧ ran 𝑓 ∈ ( LocFin ‘ 𝐽 ) ) )
47 1 2 3 4 5 6 locfinreflem ⊢ ( 𝜑 → ∃ 𝑔 ( ( Fun 𝑔 ∧ dom 𝑔 ⊆ 𝑈 ∧ ran 𝑔 ⊆ 𝐽 ) ∧ ( ran 𝑔 Ref 𝑈 ∧ ran 𝑔 ∈ ( LocFin ‘ 𝐽 ) ) ) )
48 47 adantr ⊢ ( ( 𝜑 ∧ 𝑈 ≠ ∅ ) → ∃ 𝑔 ( ( Fun 𝑔 ∧ dom 𝑔 ⊆ 𝑈 ∧ ran 𝑔 ⊆ 𝐽 ) ∧ ( ran 𝑔 Ref 𝑈 ∧ ran 𝑔 ∈ ( LocFin ‘ 𝐽 ) ) ) )
49 simpl ⊢ ( ( ( 𝜑 ∧ 𝑈 ≠ ∅ ) ∧ ( ( Fun 𝑔 ∧ dom 𝑔 ⊆ 𝑈 ∧ ran 𝑔 ⊆ 𝐽 ) ∧ ( ran 𝑔 Ref 𝑈 ∧ ran 𝑔 ∈ ( LocFin ‘ 𝐽 ) ) ) ) → ( 𝜑 ∧ 𝑈 ≠ ∅ ) )
50 simprl1 ⊢ ( ( ( 𝜑 ∧ 𝑈 ≠ ∅ ) ∧ ( ( Fun 𝑔 ∧ dom 𝑔 ⊆ 𝑈 ∧ ran 𝑔 ⊆ 𝐽 ) ∧ ( ran 𝑔 Ref 𝑈 ∧ ran 𝑔 ∈ ( LocFin ‘ 𝐽 ) ) ) ) → Fun 𝑔 )
51 fdmrn ⊢ ( Fun 𝑔 ↔ 𝑔 : dom 𝑔 ⟶ ran 𝑔 )
52 50 51 sylib ⊢ ( ( ( 𝜑 ∧ 𝑈 ≠ ∅ ) ∧ ( ( Fun 𝑔 ∧ dom 𝑔 ⊆ 𝑈 ∧ ran 𝑔 ⊆ 𝐽 ) ∧ ( ran 𝑔 Ref 𝑈 ∧ ran 𝑔 ∈ ( LocFin ‘ 𝐽 ) ) ) ) → 𝑔 : dom 𝑔 ⟶ ran 𝑔 )
53 simprl3 ⊢ ( ( ( 𝜑 ∧ 𝑈 ≠ ∅ ) ∧ ( ( Fun 𝑔 ∧ dom 𝑔 ⊆ 𝑈 ∧ ran 𝑔 ⊆ 𝐽 ) ∧ ( ran 𝑔 Ref 𝑈 ∧ ran 𝑔 ∈ ( LocFin ‘ 𝐽 ) ) ) ) → ran 𝑔 ⊆ 𝐽 )
54 52 53 fssd ⊢ ( ( ( 𝜑 ∧ 𝑈 ≠ ∅ ) ∧ ( ( Fun 𝑔 ∧ dom 𝑔 ⊆ 𝑈 ∧ ran 𝑔 ⊆ 𝐽 ) ∧ ( ran 𝑔 Ref 𝑈 ∧ ran 𝑔 ∈ ( LocFin ‘ 𝐽 ) ) ) ) → 𝑔 : dom 𝑔 ⟶ 𝐽 )
55 fconstg ⊢ ( ∅ ∈ V → ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) : ( 𝑈 ∖ dom 𝑔 ) ⟶ { ∅ } )
56 12 55 mp1i ⊢ ( ( ( 𝜑 ∧ 𝑈 ≠ ∅ ) ∧ ( ( Fun 𝑔 ∧ dom 𝑔 ⊆ 𝑈 ∧ ran 𝑔 ⊆ 𝐽 ) ∧ ( ran 𝑔 Ref 𝑈 ∧ ran 𝑔 ∈ ( LocFin ‘ 𝐽 ) ) ) ) → ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) : ( 𝑈 ∖ dom 𝑔 ) ⟶ { ∅ } )
57 0opn ⊢ ( 𝐽 ∈ Top → ∅ ∈ 𝐽 )
58 6 33 57 3syl ⊢ ( 𝜑 → ∅ ∈ 𝐽 )
59 58 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑈 ≠ ∅ ) ∧ ( ( Fun 𝑔 ∧ dom 𝑔 ⊆ 𝑈 ∧ ran 𝑔 ⊆ 𝐽 ) ∧ ( ran 𝑔 Ref 𝑈 ∧ ran 𝑔 ∈ ( LocFin ‘ 𝐽 ) ) ) ) → ∅ ∈ 𝐽 )
60 59 snssd ⊢ ( ( ( 𝜑 ∧ 𝑈 ≠ ∅ ) ∧ ( ( Fun 𝑔 ∧ dom 𝑔 ⊆ 𝑈 ∧ ran 𝑔 ⊆ 𝐽 ) ∧ ( ran 𝑔 Ref 𝑈 ∧ ran 𝑔 ∈ ( LocFin ‘ 𝐽 ) ) ) ) → { ∅ } ⊆ 𝐽 )
61 56 60 fssd ⊢ ( ( ( 𝜑 ∧ 𝑈 ≠ ∅ ) ∧ ( ( Fun 𝑔 ∧ dom 𝑔 ⊆ 𝑈 ∧ ran 𝑔 ⊆ 𝐽 ) ∧ ( ran 𝑔 Ref 𝑈 ∧ ran 𝑔 ∈ ( LocFin ‘ 𝐽 ) ) ) ) → ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) : ( 𝑈 ∖ dom 𝑔 ) ⟶ 𝐽 )
62 disjdif ⊢ ( dom 𝑔 ∩ ( 𝑈 ∖ dom 𝑔 ) ) = ∅
63 62 a1i ⊢ ( ( ( 𝜑 ∧ 𝑈 ≠ ∅ ) ∧ ( ( Fun 𝑔 ∧ dom 𝑔 ⊆ 𝑈 ∧ ran 𝑔 ⊆ 𝐽 ) ∧ ( ran 𝑔 Ref 𝑈 ∧ ran 𝑔 ∈ ( LocFin ‘ 𝐽 ) ) ) ) → ( dom 𝑔 ∩ ( 𝑈 ∖ dom 𝑔 ) ) = ∅ )
64 fun2 ⊢ ( ( ( 𝑔 : dom 𝑔 ⟶ 𝐽 ∧ ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) : ( 𝑈 ∖ dom 𝑔 ) ⟶ 𝐽 ) ∧ ( dom 𝑔 ∩ ( 𝑈 ∖ dom 𝑔 ) ) = ∅ ) → ( 𝑔 ∪ ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) ) : ( dom 𝑔 ∪ ( 𝑈 ∖ dom 𝑔 ) ) ⟶ 𝐽 )
65 54 61 63 64 syl21anc ⊢ ( ( ( 𝜑 ∧ 𝑈 ≠ ∅ ) ∧ ( ( Fun 𝑔 ∧ dom 𝑔 ⊆ 𝑈 ∧ ran 𝑔 ⊆ 𝐽 ) ∧ ( ran 𝑔 Ref 𝑈 ∧ ran 𝑔 ∈ ( LocFin ‘ 𝐽 ) ) ) ) → ( 𝑔 ∪ ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) ) : ( dom 𝑔 ∪ ( 𝑈 ∖ dom 𝑔 ) ) ⟶ 𝐽 )
66 simprl2 ⊢ ( ( ( 𝜑 ∧ 𝑈 ≠ ∅ ) ∧ ( ( Fun 𝑔 ∧ dom 𝑔 ⊆ 𝑈 ∧ ran 𝑔 ⊆ 𝐽 ) ∧ ( ran 𝑔 Ref 𝑈 ∧ ran 𝑔 ∈ ( LocFin ‘ 𝐽 ) ) ) ) → dom 𝑔 ⊆ 𝑈 )
67 undif ⊢ ( dom 𝑔 ⊆ 𝑈 ↔ ( dom 𝑔 ∪ ( 𝑈 ∖ dom 𝑔 ) ) = 𝑈 )
68 66 67 sylib ⊢ ( ( ( 𝜑 ∧ 𝑈 ≠ ∅ ) ∧ ( ( Fun 𝑔 ∧ dom 𝑔 ⊆ 𝑈 ∧ ran 𝑔 ⊆ 𝐽 ) ∧ ( ran 𝑔 Ref 𝑈 ∧ ran 𝑔 ∈ ( LocFin ‘ 𝐽 ) ) ) ) → ( dom 𝑔 ∪ ( 𝑈 ∖ dom 𝑔 ) ) = 𝑈 )
69 68 feq2d ⊢ ( ( ( 𝜑 ∧ 𝑈 ≠ ∅ ) ∧ ( ( Fun 𝑔 ∧ dom 𝑔 ⊆ 𝑈 ∧ ran 𝑔 ⊆ 𝐽 ) ∧ ( ran 𝑔 Ref 𝑈 ∧ ran 𝑔 ∈ ( LocFin ‘ 𝐽 ) ) ) ) → ( ( 𝑔 ∪ ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) ) : ( dom 𝑔 ∪ ( 𝑈 ∖ dom 𝑔 ) ) ⟶ 𝐽 ↔ ( 𝑔 ∪ ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) ) : 𝑈 ⟶ 𝐽 ) )
70 65 69 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑈 ≠ ∅ ) ∧ ( ( Fun 𝑔 ∧ dom 𝑔 ⊆ 𝑈 ∧ ran 𝑔 ⊆ 𝐽 ) ∧ ( ran 𝑔 Ref 𝑈 ∧ ran 𝑔 ∈ ( LocFin ‘ 𝐽 ) ) ) ) → ( 𝑔 ∪ ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) ) : 𝑈 ⟶ 𝐽 )
71 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑈 ≠ ∅ ) ∧ ( ( Fun 𝑔 ∧ dom 𝑔 ⊆ 𝑈 ∧ ran 𝑔 ⊆ 𝐽 ) ∧ ( ran 𝑔 Ref 𝑈 ∧ ran 𝑔 ∈ ( LocFin ‘ 𝐽 ) ) ) ) ∧ ran ( 𝑔 ∪ ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) ) = ran 𝑔 ) → ran ( 𝑔 ∪ ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) ) = ran 𝑔 )
72 simprrl ⊢ ( ( ( 𝜑 ∧ 𝑈 ≠ ∅ ) ∧ ( ( Fun 𝑔 ∧ dom 𝑔 ⊆ 𝑈 ∧ ran 𝑔 ⊆ 𝐽 ) ∧ ( ran 𝑔 Ref 𝑈 ∧ ran 𝑔 ∈ ( LocFin ‘ 𝐽 ) ) ) ) → ran 𝑔 Ref 𝑈 )
73 72 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑈 ≠ ∅ ) ∧ ( ( Fun 𝑔 ∧ dom 𝑔 ⊆ 𝑈 ∧ ran 𝑔 ⊆ 𝐽 ) ∧ ( ran 𝑔 Ref 𝑈 ∧ ran 𝑔 ∈ ( LocFin ‘ 𝐽 ) ) ) ) ∧ ran ( 𝑔 ∪ ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) ) = ran 𝑔 ) → ran 𝑔 Ref 𝑈 )
74 71 73 eqbrtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑈 ≠ ∅ ) ∧ ( ( Fun 𝑔 ∧ dom 𝑔 ⊆ 𝑈 ∧ ran 𝑔 ⊆ 𝐽 ) ∧ ( ran 𝑔 Ref 𝑈 ∧ ran 𝑔 ∈ ( LocFin ‘ 𝐽 ) ) ) ) ∧ ran ( 𝑔 ∪ ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) ) = ran 𝑔 ) → ran ( 𝑔 ∪ ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) ) Ref 𝑈 )
75 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑈 ≠ ∅ ) ∧ ( ( Fun 𝑔 ∧ dom 𝑔 ⊆ 𝑈 ∧ ran 𝑔 ⊆ 𝐽 ) ∧ ( ran 𝑔 Ref 𝑈 ∧ ran 𝑔 ∈ ( LocFin ‘ 𝐽 ) ) ) ) ∧ ran ( 𝑔 ∪ ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) ) = ( ran 𝑔 ∪ { ∅ } ) ) → ran ( 𝑔 ∪ ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) ) = ( ran 𝑔 ∪ { ∅ } ) )
76 49 simprd ⊢ ( ( ( 𝜑 ∧ 𝑈 ≠ ∅ ) ∧ ( ( Fun 𝑔 ∧ dom 𝑔 ⊆ 𝑈 ∧ ran 𝑔 ⊆ 𝐽 ) ∧ ( ran 𝑔 Ref 𝑈 ∧ ran 𝑔 ∈ ( LocFin ‘ 𝐽 ) ) ) ) → 𝑈 ≠ ∅ )
77 refun0 ⊢ ( ( ran 𝑔 Ref 𝑈 ∧ 𝑈 ≠ ∅ ) → ( ran 𝑔 ∪ { ∅ } ) Ref 𝑈 )
78 72 76 77 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑈 ≠ ∅ ) ∧ ( ( Fun 𝑔 ∧ dom 𝑔 ⊆ 𝑈 ∧ ran 𝑔 ⊆ 𝐽 ) ∧ ( ran 𝑔 Ref 𝑈 ∧ ran 𝑔 ∈ ( LocFin ‘ 𝐽 ) ) ) ) → ( ran 𝑔 ∪ { ∅ } ) Ref 𝑈 )
79 78 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑈 ≠ ∅ ) ∧ ( ( Fun 𝑔 ∧ dom 𝑔 ⊆ 𝑈 ∧ ran 𝑔 ⊆ 𝐽 ) ∧ ( ran 𝑔 Ref 𝑈 ∧ ran 𝑔 ∈ ( LocFin ‘ 𝐽 ) ) ) ) ∧ ran ( 𝑔 ∪ ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) ) = ( ran 𝑔 ∪ { ∅ } ) ) → ( ran 𝑔 ∪ { ∅ } ) Ref 𝑈 )
80 75 79 eqbrtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑈 ≠ ∅ ) ∧ ( ( Fun 𝑔 ∧ dom 𝑔 ⊆ 𝑈 ∧ ran 𝑔 ⊆ 𝐽 ) ∧ ( ran 𝑔 Ref 𝑈 ∧ ran 𝑔 ∈ ( LocFin ‘ 𝐽 ) ) ) ) ∧ ran ( 𝑔 ∪ ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) ) = ( ran 𝑔 ∪ { ∅ } ) ) → ran ( 𝑔 ∪ ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) ) Ref 𝑈 )
81 rnxpss ⊢ ran ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) ⊆ { ∅ }
82 sssn ⊢ ( ran ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) ⊆ { ∅ } ↔ ( ran ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) = ∅ ∨ ran ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) = { ∅ } ) )
83 81 82 mpbi ⊢ ( ran ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) = ∅ ∨ ran ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) = { ∅ } )
84 rnun ⊢ ran ( 𝑔 ∪ ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) ) = ( ran 𝑔 ∪ ran ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) )
85 uneq2 ⊢ ( ran ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) = ∅ → ( ran 𝑔 ∪ ran ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) ) = ( ran 𝑔 ∪ ∅ ) )
86 84 85 eqtrid ⊢ ( ran ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) = ∅ → ran ( 𝑔 ∪ ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) ) = ( ran 𝑔 ∪ ∅ ) )
87 un0 ⊢ ( ran 𝑔 ∪ ∅ ) = ran 𝑔
88 86 87 eqtrdi ⊢ ( ran ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) = ∅ → ran ( 𝑔 ∪ ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) ) = ran 𝑔 )
89 uneq2 ⊢ ( ran ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) = { ∅ } → ( ran 𝑔 ∪ ran ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) ) = ( ran 𝑔 ∪ { ∅ } ) )
90 84 89 eqtrid ⊢ ( ran ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) = { ∅ } → ran ( 𝑔 ∪ ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) ) = ( ran 𝑔 ∪ { ∅ } ) )
91 88 90 orim12i ⊢ ( ( ran ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) = ∅ ∨ ran ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) = { ∅ } ) → ( ran ( 𝑔 ∪ ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) ) = ran 𝑔 ∨ ran ( 𝑔 ∪ ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) ) = ( ran 𝑔 ∪ { ∅ } ) ) )
92 83 91 mp1i ⊢ ( ( ( 𝜑 ∧ 𝑈 ≠ ∅ ) ∧ ( ( Fun 𝑔 ∧ dom 𝑔 ⊆ 𝑈 ∧ ran 𝑔 ⊆ 𝐽 ) ∧ ( ran 𝑔 Ref 𝑈 ∧ ran 𝑔 ∈ ( LocFin ‘ 𝐽 ) ) ) ) → ( ran ( 𝑔 ∪ ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) ) = ran 𝑔 ∨ ran ( 𝑔 ∪ ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) ) = ( ran 𝑔 ∪ { ∅ } ) ) )
93 74 80 92 mpjaodan ⊢ ( ( ( 𝜑 ∧ 𝑈 ≠ ∅ ) ∧ ( ( Fun 𝑔 ∧ dom 𝑔 ⊆ 𝑈 ∧ ran 𝑔 ⊆ 𝐽 ) ∧ ( ran 𝑔 Ref 𝑈 ∧ ran 𝑔 ∈ ( LocFin ‘ 𝐽 ) ) ) ) → ran ( 𝑔 ∪ ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) ) Ref 𝑈 )
94 simprrr ⊢ ( ( ( 𝜑 ∧ 𝑈 ≠ ∅ ) ∧ ( ( Fun 𝑔 ∧ dom 𝑔 ⊆ 𝑈 ∧ ran 𝑔 ⊆ 𝐽 ) ∧ ( ran 𝑔 Ref 𝑈 ∧ ran 𝑔 ∈ ( LocFin ‘ 𝐽 ) ) ) ) → ran 𝑔 ∈ ( LocFin ‘ 𝐽 ) )
95 94 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑈 ≠ ∅ ) ∧ ( ( Fun 𝑔 ∧ dom 𝑔 ⊆ 𝑈 ∧ ran 𝑔 ⊆ 𝐽 ) ∧ ( ran 𝑔 Ref 𝑈 ∧ ran 𝑔 ∈ ( LocFin ‘ 𝐽 ) ) ) ) ∧ ran ( 𝑔 ∪ ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) ) = ran 𝑔 ) → ran 𝑔 ∈ ( LocFin ‘ 𝐽 ) )
96 71 95 eqeltrd ⊢ ( ( ( ( 𝜑 ∧ 𝑈 ≠ ∅ ) ∧ ( ( Fun 𝑔 ∧ dom 𝑔 ⊆ 𝑈 ∧ ran 𝑔 ⊆ 𝐽 ) ∧ ( ran 𝑔 Ref 𝑈 ∧ ran 𝑔 ∈ ( LocFin ‘ 𝐽 ) ) ) ) ∧ ran ( 𝑔 ∪ ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) ) = ran 𝑔 ) → ran ( 𝑔 ∪ ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) ) ∈ ( LocFin ‘ 𝐽 ) )
97 94 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑈 ≠ ∅ ) ∧ ( ( Fun 𝑔 ∧ dom 𝑔 ⊆ 𝑈 ∧ ran 𝑔 ⊆ 𝐽 ) ∧ ( ran 𝑔 Ref 𝑈 ∧ ran 𝑔 ∈ ( LocFin ‘ 𝐽 ) ) ) ) ∧ ran ( 𝑔 ∪ ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) ) = ( ran 𝑔 ∪ { ∅ } ) ) → ran 𝑔 ∈ ( LocFin ‘ 𝐽 ) )
98 snfi ⊢ { ∅ } ∈ Fin
99 98 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑈 ≠ ∅ ) ∧ ( ( Fun 𝑔 ∧ dom 𝑔 ⊆ 𝑈 ∧ ran 𝑔 ⊆ 𝐽 ) ∧ ( ran 𝑔 Ref 𝑈 ∧ ran 𝑔 ∈ ( LocFin ‘ 𝐽 ) ) ) ) ∧ ran ( 𝑔 ∪ ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) ) = ( ran 𝑔 ∪ { ∅ } ) ) → { ∅ } ∈ Fin )
100 59 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑈 ≠ ∅ ) ∧ ( ( Fun 𝑔 ∧ dom 𝑔 ⊆ 𝑈 ∧ ran 𝑔 ⊆ 𝐽 ) ∧ ( ran 𝑔 Ref 𝑈 ∧ ran 𝑔 ∈ ( LocFin ‘ 𝐽 ) ) ) ) ∧ ran ( 𝑔 ∪ ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) ) = ( ran 𝑔 ∪ { ∅ } ) ) → ∅ ∈ 𝐽 )
101 100 snssd ⊢ ( ( ( ( 𝜑 ∧ 𝑈 ≠ ∅ ) ∧ ( ( Fun 𝑔 ∧ dom 𝑔 ⊆ 𝑈 ∧ ran 𝑔 ⊆ 𝐽 ) ∧ ( ran 𝑔 Ref 𝑈 ∧ ran 𝑔 ∈ ( LocFin ‘ 𝐽 ) ) ) ) ∧ ran ( 𝑔 ∪ ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) ) = ( ran 𝑔 ∪ { ∅ } ) ) → { ∅ } ⊆ 𝐽 )
102 101 unissd ⊢ ( ( ( ( 𝜑 ∧ 𝑈 ≠ ∅ ) ∧ ( ( Fun 𝑔 ∧ dom 𝑔 ⊆ 𝑈 ∧ ran 𝑔 ⊆ 𝐽 ) ∧ ( ran 𝑔 Ref 𝑈 ∧ ran 𝑔 ∈ ( LocFin ‘ 𝐽 ) ) ) ) ∧ ran ( 𝑔 ∪ ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) ) = ( ran 𝑔 ∪ { ∅ } ) ) → ∪ { ∅ } ⊆ ∪ 𝐽 )
103 lfinun ⊢ ( ( ran 𝑔 ∈ ( LocFin ‘ 𝐽 ) ∧ { ∅ } ∈ Fin ∧ ∪ { ∅ } ⊆ ∪ 𝐽 ) → ( ran 𝑔 ∪ { ∅ } ) ∈ ( LocFin ‘ 𝐽 ) )
104 97 99 102 103 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑈 ≠ ∅ ) ∧ ( ( Fun 𝑔 ∧ dom 𝑔 ⊆ 𝑈 ∧ ran 𝑔 ⊆ 𝐽 ) ∧ ( ran 𝑔 Ref 𝑈 ∧ ran 𝑔 ∈ ( LocFin ‘ 𝐽 ) ) ) ) ∧ ran ( 𝑔 ∪ ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) ) = ( ran 𝑔 ∪ { ∅ } ) ) → ( ran 𝑔 ∪ { ∅ } ) ∈ ( LocFin ‘ 𝐽 ) )
105 75 104 eqeltrd ⊢ ( ( ( ( 𝜑 ∧ 𝑈 ≠ ∅ ) ∧ ( ( Fun 𝑔 ∧ dom 𝑔 ⊆ 𝑈 ∧ ran 𝑔 ⊆ 𝐽 ) ∧ ( ran 𝑔 Ref 𝑈 ∧ ran 𝑔 ∈ ( LocFin ‘ 𝐽 ) ) ) ) ∧ ran ( 𝑔 ∪ ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) ) = ( ran 𝑔 ∪ { ∅ } ) ) → ran ( 𝑔 ∪ ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) ) ∈ ( LocFin ‘ 𝐽 ) )
106 96 105 92 mpjaodan ⊢ ( ( ( 𝜑 ∧ 𝑈 ≠ ∅ ) ∧ ( ( Fun 𝑔 ∧ dom 𝑔 ⊆ 𝑈 ∧ ran 𝑔 ⊆ 𝐽 ) ∧ ( ran 𝑔 Ref 𝑈 ∧ ran 𝑔 ∈ ( LocFin ‘ 𝐽 ) ) ) ) → ran ( 𝑔 ∪ ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) ) ∈ ( LocFin ‘ 𝐽 ) )
107 refrel ⊢ Rel Ref
108 107 brrelex2i ⊢ ( 𝑉 Ref 𝑈 → 𝑈 ∈ V )
109 difexg ⊢ ( 𝑈 ∈ V → ( 𝑈 ∖ dom 𝑔 ) ∈ V )
110 5 108 109 3syl ⊢ ( 𝜑 → ( 𝑈 ∖ dom 𝑔 ) ∈ V )
111 110 adantr ⊢ ( ( 𝜑 ∧ 𝑈 ≠ ∅ ) → ( 𝑈 ∖ dom 𝑔 ) ∈ V )
112 p0ex ⊢ { ∅ } ∈ V
113 xpexg ⊢ ( ( ( 𝑈 ∖ dom 𝑔 ) ∈ V ∧ { ∅ } ∈ V ) → ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) ∈ V )
114 112 113 mpan2 ⊢ ( ( 𝑈 ∖ dom 𝑔 ) ∈ V → ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) ∈ V )
115 vex ⊢ 𝑔 ∈ V
116 unexg ⊢ ( ( 𝑔 ∈ V ∧ ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) ∈ V ) → ( 𝑔 ∪ ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) ) ∈ V )
117 115 116 mpan ⊢ ( ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) ∈ V → ( 𝑔 ∪ ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) ) ∈ V )
118 feq1 ⊢ ( 𝑓 = ( 𝑔 ∪ ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) ) → ( 𝑓 : 𝑈 ⟶ 𝐽 ↔ ( 𝑔 ∪ ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) ) : 𝑈 ⟶ 𝐽 ) )
119 rneq ⊢ ( 𝑓 = ( 𝑔 ∪ ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) ) → ran 𝑓 = ran ( 𝑔 ∪ ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) ) )
120 119 breq1d ⊢ ( 𝑓 = ( 𝑔 ∪ ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) ) → ( ran 𝑓 Ref 𝑈 ↔ ran ( 𝑔 ∪ ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) ) Ref 𝑈 ) )
121 119 eleq1d ⊢ ( 𝑓 = ( 𝑔 ∪ ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) ) → ( ran 𝑓 ∈ ( LocFin ‘ 𝐽 ) ↔ ran ( 𝑔 ∪ ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) ) ∈ ( LocFin ‘ 𝐽 ) ) )
122 118 120 121 3anbi123d ⊢ ( 𝑓 = ( 𝑔 ∪ ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) ) → ( ( 𝑓 : 𝑈 ⟶ 𝐽 ∧ ran 𝑓 Ref 𝑈 ∧ ran 𝑓 ∈ ( LocFin ‘ 𝐽 ) ) ↔ ( ( 𝑔 ∪ ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) ) : 𝑈 ⟶ 𝐽 ∧ ran ( 𝑔 ∪ ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) ) Ref 𝑈 ∧ ran ( 𝑔 ∪ ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) ) ∈ ( LocFin ‘ 𝐽 ) ) ) )
123 122 spcegv ⊢ ( ( 𝑔 ∪ ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) ) ∈ V → ( ( ( 𝑔 ∪ ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) ) : 𝑈 ⟶ 𝐽 ∧ ran ( 𝑔 ∪ ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) ) Ref 𝑈 ∧ ran ( 𝑔 ∪ ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) ) ∈ ( LocFin ‘ 𝐽 ) ) → ∃ 𝑓 ( 𝑓 : 𝑈 ⟶ 𝐽 ∧ ran 𝑓 Ref 𝑈 ∧ ran 𝑓 ∈ ( LocFin ‘ 𝐽 ) ) ) )
124 111 114 117 123 4syl ⊢ ( ( 𝜑 ∧ 𝑈 ≠ ∅ ) → ( ( ( 𝑔 ∪ ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) ) : 𝑈 ⟶ 𝐽 ∧ ran ( 𝑔 ∪ ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) ) Ref 𝑈 ∧ ran ( 𝑔 ∪ ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) ) ∈ ( LocFin ‘ 𝐽 ) ) → ∃ 𝑓 ( 𝑓 : 𝑈 ⟶ 𝐽 ∧ ran 𝑓 Ref 𝑈 ∧ ran 𝑓 ∈ ( LocFin ‘ 𝐽 ) ) ) )
125 124 imp ⊢ ( ( ( 𝜑 ∧ 𝑈 ≠ ∅ ) ∧ ( ( 𝑔 ∪ ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) ) : 𝑈 ⟶ 𝐽 ∧ ran ( 𝑔 ∪ ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) ) Ref 𝑈 ∧ ran ( 𝑔 ∪ ( ( 𝑈 ∖ dom 𝑔 ) × { ∅ } ) ) ∈ ( LocFin ‘ 𝐽 ) ) ) → ∃ 𝑓 ( 𝑓 : 𝑈 ⟶ 𝐽 ∧ ran 𝑓 Ref 𝑈 ∧ ran 𝑓 ∈ ( LocFin ‘ 𝐽 ) ) )
126 49 70 93 106 125 syl13anc ⊢ ( ( ( 𝜑 ∧ 𝑈 ≠ ∅ ) ∧ ( ( Fun 𝑔 ∧ dom 𝑔 ⊆ 𝑈 ∧ ran 𝑔 ⊆ 𝐽 ) ∧ ( ran 𝑔 Ref 𝑈 ∧ ran 𝑔 ∈ ( LocFin ‘ 𝐽 ) ) ) ) → ∃ 𝑓 ( 𝑓 : 𝑈 ⟶ 𝐽 ∧ ran 𝑓 Ref 𝑈 ∧ ran 𝑓 ∈ ( LocFin ‘ 𝐽 ) ) )
127 48 126 exlimddv ⊢ ( ( 𝜑 ∧ 𝑈 ≠ ∅ ) → ∃ 𝑓 ( 𝑓 : 𝑈 ⟶ 𝐽 ∧ ran 𝑓 Ref 𝑈 ∧ ran 𝑓 ∈ ( LocFin ‘ 𝐽 ) ) )
128 46 127 pm2.61dane ⊢ ( 𝜑 → ∃ 𝑓 ( 𝑓 : 𝑈 ⟶ 𝐽 ∧ ran 𝑓 Ref 𝑈 ∧ ran 𝑓 ∈ ( LocFin ‘ 𝐽 ) ) )