Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  locfinref Structured version   Visualization version   GIF version
Theorem locfinref 32821
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 𝑓 from the original cover π‘ˆ, which is taken as the index set. (Contributed by Thierry Arnoux, 31-Jan-2020.)
Hypotheses
Ref Expression
locfinref.x 𝑋 = βˆͺ 𝐽
locfinref.1 (πœ‘ β†’ π‘ˆ βŠ† 𝐽)
locfinref.2 (πœ‘ β†’ 𝑋 = βˆͺ π‘ˆ)
locfinref.3 (πœ‘ β†’ 𝑉 βŠ† 𝐽)
locfinref.4 (πœ‘ β†’ 𝑉Refπ‘ˆ)
locfinref.5 (πœ‘ β†’ 𝑉 ∈ (LocFinβ€˜π½))
Assertion
Ref Expression
locfinref (πœ‘ β†’ βˆƒπ‘“(𝑓:π‘ˆβŸΆπ½ ∧ ran 𝑓Refπ‘ˆ ∧ ran 𝑓 ∈ (LocFinβ€˜π½)))
Distinct variable groups:   𝑓,𝐽   π‘ˆ,𝑓   𝑓,𝑉   πœ‘,𝑓
Allowed substitution hint:   𝑋(𝑓)
Proof of Theorem locfinref
Dummy variables 𝑔 π‘₯ 𝑛 𝑠 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 f0 6773 . . . 4 βˆ…:βˆ…βŸΆπ½
2 simpr 486 . . . . 5 ((πœ‘ ∧ π‘ˆ = βˆ…) β†’ π‘ˆ = βˆ…)
32feq2d 6704 . . . 4 ((πœ‘ ∧ π‘ˆ = βˆ…) β†’ (βˆ…:π‘ˆβŸΆπ½ ↔ βˆ…:βˆ…βŸΆπ½))
41, 3mpbiri 258 . . 3 ((πœ‘ ∧ π‘ˆ = βˆ…) β†’ βˆ…:π‘ˆβŸΆπ½)
5 rn0 5926 . . . . 5 ran βˆ… = βˆ…
6 0ex 5308 . . . . . 6 βˆ… ∈ V
7 refref 23017 . . . . . 6 (βˆ… ∈ V β†’ βˆ…Refβˆ…)
86, 7ax-mp 5 . . . . 5 βˆ…Refβˆ…
95, 8eqbrtri 5170 . . . 4 ran βˆ…Refβˆ…
109, 2breqtrrid 5187 . . 3 ((πœ‘ ∧ π‘ˆ = βˆ…) β†’ ran βˆ…Refπ‘ˆ)
11 sn0top 22502 . . . . . 6 {βˆ…} ∈ Top
1211a1i 11 . . . . 5 ((πœ‘ ∧ π‘ˆ = βˆ…) β†’ {βˆ…} ∈ Top)
13 eqidd 2734 . . . . 5 ((πœ‘ ∧ π‘ˆ = βˆ…) β†’ βˆ… = βˆ…)
14 ral0 4513 . . . . . 6 βˆ€π‘₯ ∈ βˆ… βˆƒπ‘› ∈ {βˆ…} (π‘₯ ∈ 𝑛 ∧ {𝑠 ∈ ran βˆ… ∣ (𝑠 ∩ 𝑛) β‰  βˆ…} ∈ Fin)
1514a1i 11 . . . . 5 ((πœ‘ ∧ π‘ˆ = βˆ…) β†’ βˆ€π‘₯ ∈ βˆ… βˆƒπ‘› ∈ {βˆ…} (π‘₯ ∈ 𝑛 ∧ {𝑠 ∈ ran βˆ… ∣ (𝑠 ∩ 𝑛) β‰  βˆ…} ∈ Fin))
166unisn 4931 . . . . . . 7 βˆͺ {βˆ…} = βˆ…
1716eqcomi 2742 . . . . . 6 βˆ… = βˆͺ {βˆ…}
185unieqi 4922 . . . . . . 7 βˆͺ ran βˆ… = βˆͺ βˆ…
19 uni0 4940 . . . . . . 7 βˆͺ βˆ… = βˆ…
2018, 19eqtr2i 2762 . . . . . 6 βˆ… = βˆͺ ran βˆ…
2117, 20islocfin 23021 . . . . 5 (ran βˆ… ∈ (LocFinβ€˜{βˆ…}) ↔ ({βˆ…} ∈ Top ∧ βˆ… = βˆ… ∧ βˆ€π‘₯ ∈ βˆ… βˆƒπ‘› ∈ {βˆ…} (π‘₯ ∈ 𝑛 ∧ {𝑠 ∈ ran βˆ… ∣ (𝑠 ∩ 𝑛) β‰  βˆ…} ∈ Fin)))
2212, 13, 15, 21syl3anbrc 1344 . . . 4 ((πœ‘ ∧ π‘ˆ = βˆ…) β†’ ran βˆ… ∈ (LocFinβ€˜{βˆ…}))
23 locfinref.2 . . . . . . . . 9 (πœ‘ β†’ 𝑋 = βˆͺ π‘ˆ)
2423adantr 482 . . . . . . . 8 ((πœ‘ ∧ π‘ˆ = βˆ…) β†’ 𝑋 = βˆͺ π‘ˆ)
252unieqd 4923 . . . . . . . 8 ((πœ‘ ∧ π‘ˆ = βˆ…) β†’ βˆͺ π‘ˆ = βˆͺ βˆ…)
2624, 25eqtrd 2773 . . . . . . 7 ((πœ‘ ∧ π‘ˆ = βˆ…) β†’ 𝑋 = βˆͺ βˆ…)
27 locfinref.x . . . . . . 7 𝑋 = βˆͺ 𝐽
2826, 27, 193eqtr3g 2796 . . . . . 6 ((πœ‘ ∧ π‘ˆ = βˆ…) β†’ βˆͺ 𝐽 = βˆ…)
29 locfinref.5 . . . . . . . 8 (πœ‘ β†’ 𝑉 ∈ (LocFinβ€˜π½))
30 locfintop 23025 . . . . . . . 8 (𝑉 ∈ (LocFinβ€˜π½) β†’ 𝐽 ∈ Top)
31 0top 22486 . . . . . . . 8 (𝐽 ∈ Top β†’ (βˆͺ 𝐽 = βˆ… ↔ 𝐽 = {βˆ…}))
3229, 30, 313syl 18 . . . . . . 7 (πœ‘ β†’ (βˆͺ 𝐽 = βˆ… ↔ 𝐽 = {βˆ…}))
3332adantr 482 . . . . . 6 ((πœ‘ ∧ π‘ˆ = βˆ…) β†’ (βˆͺ 𝐽 = βˆ… ↔ 𝐽 = {βˆ…}))
3428, 33mpbid 231 . . . . 5 ((πœ‘ ∧ π‘ˆ = βˆ…) β†’ 𝐽 = {βˆ…})
3534fveq2d 6896 . . . 4 ((πœ‘ ∧ π‘ˆ = βˆ…) β†’ (LocFinβ€˜π½) = (LocFinβ€˜{βˆ…}))
3622, 35eleqtrrd 2837 . . 3 ((πœ‘ ∧ π‘ˆ = βˆ…) β†’ ran βˆ… ∈ (LocFinβ€˜π½))
37 feq1 6699 . . . . 5 (𝑓 = βˆ… β†’ (𝑓:π‘ˆβŸΆπ½ ↔ βˆ…:π‘ˆβŸΆπ½))
38 rneq 5936 . . . . . 6 (𝑓 = βˆ… β†’ ran 𝑓 = ran βˆ…)
3938breq1d 5159 . . . . 5 (𝑓 = βˆ… β†’ (ran 𝑓Refπ‘ˆ ↔ ran βˆ…Refπ‘ˆ))
4038eleq1d 2819 . . . . 5 (𝑓 = βˆ… β†’ (ran 𝑓 ∈ (LocFinβ€˜π½) ↔ ran βˆ… ∈ (LocFinβ€˜π½)))
4137, 39, 403anbi123d 1437 . . . 4 (𝑓 = βˆ… β†’ ((𝑓:π‘ˆβŸΆπ½ ∧ ran 𝑓Refπ‘ˆ ∧ ran 𝑓 ∈ (LocFinβ€˜π½)) ↔ (βˆ…:π‘ˆβŸΆπ½ ∧ ran βˆ…Refπ‘ˆ ∧ ran βˆ… ∈ (LocFinβ€˜π½))))
426, 41spcev 3597 . . 3 ((βˆ…:π‘ˆβŸΆπ½ ∧ ran βˆ…Refπ‘ˆ ∧ ran βˆ… ∈ (LocFinβ€˜π½)) β†’ βˆƒπ‘“(𝑓:π‘ˆβŸΆπ½ ∧ ran 𝑓Refπ‘ˆ ∧ ran 𝑓 ∈ (LocFinβ€˜π½)))
434, 10, 36, 42syl3anc 1372 . 2 ((πœ‘ ∧ π‘ˆ = βˆ…) β†’ βˆƒπ‘“(𝑓:π‘ˆβŸΆπ½ ∧ ran 𝑓Refπ‘ˆ ∧ ran 𝑓 ∈ (LocFinβ€˜π½)))
44 locfinref.1 . . . . 5 (πœ‘ β†’ π‘ˆ βŠ† 𝐽)
45 locfinref.3 . . . . 5 (πœ‘ β†’ 𝑉 βŠ† 𝐽)
46 locfinref.4 . . . . 5 (πœ‘ β†’ 𝑉Refπ‘ˆ)
4727, 44, 23, 45, 46, 29locfinreflem 32820 . . . 4 (πœ‘ β†’ βˆƒπ‘”((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½))))
4847adantr 482 . . 3 ((πœ‘ ∧ π‘ˆ β‰  βˆ…) β†’ βˆƒπ‘”((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½))))
49 simpl 484 . . . 4 (((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) β†’ (πœ‘ ∧ π‘ˆ β‰  βˆ…))
50 simprl1 1219 . . . . . . . 8 (((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) β†’ Fun 𝑔)
51 fdmrn 6750 . . . . . . . 8 (Fun 𝑔 ↔ 𝑔:dom π‘”βŸΆran 𝑔)
5250, 51sylib 217 . . . . . . 7 (((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) β†’ 𝑔:dom π‘”βŸΆran 𝑔)
53 simprl3 1221 . . . . . . 7 (((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) β†’ ran 𝑔 βŠ† 𝐽)
5452, 53fssd 6736 . . . . . 6 (((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) β†’ 𝑔:dom π‘”βŸΆπ½)
55 fconstg 6779 . . . . . . . 8 (βˆ… ∈ V β†’ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…}):(π‘ˆ βˆ– dom 𝑔)⟢{βˆ…})
566, 55mp1i 13 . . . . . . 7 (((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) β†’ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…}):(π‘ˆ βˆ– dom 𝑔)⟢{βˆ…})
57 0opn 22406 . . . . . . . . . 10 (𝐽 ∈ Top β†’ βˆ… ∈ 𝐽)
5829, 30, 573syl 18 . . . . . . . . 9 (πœ‘ β†’ βˆ… ∈ 𝐽)
5958ad2antrr 725 . . . . . . . 8 (((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) β†’ βˆ… ∈ 𝐽)
6059snssd 4813 . . . . . . 7 (((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) β†’ {βˆ…} βŠ† 𝐽)
6156, 60fssd 6736 . . . . . 6 (((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) β†’ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…}):(π‘ˆ βˆ– dom 𝑔)⟢𝐽)
62 disjdif 4472 . . . . . . 7 (dom 𝑔 ∩ (π‘ˆ βˆ– dom 𝑔)) = βˆ…
6362a1i 11 . . . . . 6 (((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) β†’ (dom 𝑔 ∩ (π‘ˆ βˆ– dom 𝑔)) = βˆ…)
64 fun2 6755 . . . . . 6 (((𝑔:dom π‘”βŸΆπ½ ∧ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…}):(π‘ˆ βˆ– dom 𝑔)⟢𝐽) ∧ (dom 𝑔 ∩ (π‘ˆ βˆ– dom 𝑔)) = βˆ…) β†’ (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})):(dom 𝑔 βˆͺ (π‘ˆ βˆ– dom 𝑔))⟢𝐽)
6554, 61, 63, 64syl21anc 837 . . . . 5 (((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) β†’ (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})):(dom 𝑔 βˆͺ (π‘ˆ βˆ– dom 𝑔))⟢𝐽)
66 simprl2 1220 . . . . . . 7 (((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) β†’ dom 𝑔 βŠ† π‘ˆ)
67 undif 4482 . . . . . . 7 (dom 𝑔 βŠ† π‘ˆ ↔ (dom 𝑔 βˆͺ (π‘ˆ βˆ– dom 𝑔)) = π‘ˆ)
6866, 67sylib 217 . . . . . 6 (((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) β†’ (dom 𝑔 βˆͺ (π‘ˆ βˆ– dom 𝑔)) = π‘ˆ)
6968feq2d 6704 . . . . 5 (((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) β†’ ((𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})):(dom 𝑔 βˆͺ (π‘ˆ βˆ– dom 𝑔))⟢𝐽 ↔ (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})):π‘ˆβŸΆπ½))
7065, 69mpbid 231 . . . 4 (((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) β†’ (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})):π‘ˆβŸΆπ½)
71 simpr 486 . . . . . 6 ((((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) ∧ ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) = ran 𝑔) β†’ ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) = ran 𝑔)
72 simprrl 780 . . . . . . 7 (((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) β†’ ran 𝑔Refπ‘ˆ)
7372adantr 482 . . . . . 6 ((((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) ∧ ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) = ran 𝑔) β†’ ran 𝑔Refπ‘ˆ)
7471, 73eqbrtrd 5171 . . . . 5 ((((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) ∧ ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) = ran 𝑔) β†’ ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…}))Refπ‘ˆ)
75 simpr 486 . . . . . 6 ((((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) ∧ ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) = (ran 𝑔 βˆͺ {βˆ…})) β†’ ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) = (ran 𝑔 βˆͺ {βˆ…}))
7649simprd 497 . . . . . . . 8 (((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) β†’ π‘ˆ β‰  βˆ…)
77 refun0 23019 . . . . . . . 8 ((ran 𝑔Refπ‘ˆ ∧ π‘ˆ β‰  βˆ…) β†’ (ran 𝑔 βˆͺ {βˆ…})Refπ‘ˆ)
7872, 76, 77syl2anc 585 . . . . . . 7 (((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) β†’ (ran 𝑔 βˆͺ {βˆ…})Refπ‘ˆ)
7978adantr 482 . . . . . 6 ((((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) ∧ ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) = (ran 𝑔 βˆͺ {βˆ…})) β†’ (ran 𝑔 βˆͺ {βˆ…})Refπ‘ˆ)
8075, 79eqbrtrd 5171 . . . . 5 ((((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) ∧ ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) = (ran 𝑔 βˆͺ {βˆ…})) β†’ ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…}))Refπ‘ˆ)
81 rnxpss 6172 . . . . . . 7 ran ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…}) βŠ† {βˆ…}
82 sssn 4830 . . . . . . 7 (ran ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…}) βŠ† {βˆ…} ↔ (ran ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…}) = βˆ… ∨ ran ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…}) = {βˆ…}))
8381, 82mpbi 229 . . . . . 6 (ran ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…}) = βˆ… ∨ ran ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…}) = {βˆ…})
84 rnun 6146 . . . . . . . . 9 ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) = (ran 𝑔 βˆͺ ran ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…}))
85 uneq2 4158 . . . . . . . . 9 (ran ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…}) = βˆ… β†’ (ran 𝑔 βˆͺ ran ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) = (ran 𝑔 βˆͺ βˆ…))
8684, 85eqtrid 2785 . . . . . . . 8 (ran ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…}) = βˆ… β†’ ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) = (ran 𝑔 βˆͺ βˆ…))
87 un0 4391 . . . . . . . 8 (ran 𝑔 βˆͺ βˆ…) = ran 𝑔
8886, 87eqtrdi 2789 . . . . . . 7 (ran ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…}) = βˆ… β†’ ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) = ran 𝑔)
89 uneq2 4158 . . . . . . . 8 (ran ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…}) = {βˆ…} β†’ (ran 𝑔 βˆͺ ran ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) = (ran 𝑔 βˆͺ {βˆ…}))
9084, 89eqtrid 2785 . . . . . . 7 (ran ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…}) = {βˆ…} β†’ ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) = (ran 𝑔 βˆͺ {βˆ…}))
9188, 90orim12i 908 . . . . . 6 ((ran ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…}) = βˆ… ∨ ran ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…}) = {βˆ…}) β†’ (ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) = ran 𝑔 ∨ ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) = (ran 𝑔 βˆͺ {βˆ…})))
9283, 91mp1i 13 . . . . 5 (((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) β†’ (ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) = ran 𝑔 ∨ ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) = (ran 𝑔 βˆͺ {βˆ…})))
9374, 80, 92mpjaodan 958 . . . 4 (((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) β†’ ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…}))Refπ‘ˆ)
94 simprrr 781 . . . . . . 7 (((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) β†’ ran 𝑔 ∈ (LocFinβ€˜π½))
9594adantr 482 . . . . . 6 ((((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) ∧ ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) = ran 𝑔) β†’ ran 𝑔 ∈ (LocFinβ€˜π½))
9671, 95eqeltrd 2834 . . . . 5 ((((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) ∧ ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) = ran 𝑔) β†’ ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) ∈ (LocFinβ€˜π½))
9794adantr 482 . . . . . . 7 ((((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) ∧ ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) = (ran 𝑔 βˆͺ {βˆ…})) β†’ ran 𝑔 ∈ (LocFinβ€˜π½))
98 snfi 9044 . . . . . . . 8 {βˆ…} ∈ Fin
9998a1i 11 . . . . . . 7 ((((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) ∧ ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) = (ran 𝑔 βˆͺ {βˆ…})) β†’ {βˆ…} ∈ Fin)
10059adantr 482 . . . . . . . . 9 ((((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) ∧ ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) = (ran 𝑔 βˆͺ {βˆ…})) β†’ βˆ… ∈ 𝐽)
101100snssd 4813 . . . . . . . 8 ((((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) ∧ ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) = (ran 𝑔 βˆͺ {βˆ…})) β†’ {βˆ…} βŠ† 𝐽)
102101unissd 4919 . . . . . . 7 ((((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) ∧ ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) = (ran 𝑔 βˆͺ {βˆ…})) β†’ βˆͺ {βˆ…} βŠ† βˆͺ 𝐽)
103 lfinun 23029 . . . . . . 7 ((ran 𝑔 ∈ (LocFinβ€˜π½) ∧ {βˆ…} ∈ Fin ∧ βˆͺ {βˆ…} βŠ† βˆͺ 𝐽) β†’ (ran 𝑔 βˆͺ {βˆ…}) ∈ (LocFinβ€˜π½))
10497, 99, 102, 103syl3anc 1372 . . . . . 6 ((((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) ∧ ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) = (ran 𝑔 βˆͺ {βˆ…})) β†’ (ran 𝑔 βˆͺ {βˆ…}) ∈ (LocFinβ€˜π½))
10575, 104eqeltrd 2834 . . . . 5 ((((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) ∧ ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) = (ran 𝑔 βˆͺ {βˆ…})) β†’ ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) ∈ (LocFinβ€˜π½))
10696, 105, 92mpjaodan 958 . . . 4 (((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) β†’ ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) ∈ (LocFinβ€˜π½))
107 refrel 23012 . . . . . . . . 9 Rel Ref
108107brrelex2i 5734 . . . . . . . 8 (𝑉Refπ‘ˆ β†’ π‘ˆ ∈ V)
109 difexg 5328 . . . . . . . 8 (π‘ˆ ∈ V β†’ (π‘ˆ βˆ– dom 𝑔) ∈ V)
11046, 108, 1093syl 18 . . . . . . 7 (πœ‘ β†’ (π‘ˆ βˆ– dom 𝑔) ∈ V)
111110adantr 482 . . . . . 6 ((πœ‘ ∧ π‘ˆ β‰  βˆ…) β†’ (π‘ˆ βˆ– dom 𝑔) ∈ V)
112 p0ex 5383 . . . . . . 7 {βˆ…} ∈ V
113 xpexg 7737 . . . . . . 7 (((π‘ˆ βˆ– dom 𝑔) ∈ V ∧ {βˆ…} ∈ V) β†’ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…}) ∈ V)
114112, 113mpan2 690 . . . . . 6 ((π‘ˆ βˆ– dom 𝑔) ∈ V β†’ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…}) ∈ V)
115 vex 3479 . . . . . . 7 𝑔 ∈ V
116 unexg 7736 . . . . . . 7 ((𝑔 ∈ V ∧ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…}) ∈ V) β†’ (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) ∈ V)
117115, 116mpan 689 . . . . . 6 (((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…}) ∈ V β†’ (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) ∈ V)
118 feq1 6699 . . . . . . . 8 (𝑓 = (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) β†’ (𝑓:π‘ˆβŸΆπ½ ↔ (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})):π‘ˆβŸΆπ½))
119 rneq 5936 . . . . . . . . 9 (𝑓 = (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) β†’ ran 𝑓 = ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})))
120119breq1d 5159 . . . . . . . 8 (𝑓 = (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) β†’ (ran 𝑓Refπ‘ˆ ↔ ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…}))Refπ‘ˆ))
121119eleq1d 2819 . . . . . . . 8 (𝑓 = (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) β†’ (ran 𝑓 ∈ (LocFinβ€˜π½) ↔ ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) ∈ (LocFinβ€˜π½)))
122118, 120, 1213anbi123d 1437 . . . . . . 7 (𝑓 = (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) β†’ ((𝑓:π‘ˆβŸΆπ½ ∧ ran 𝑓Refπ‘ˆ ∧ ran 𝑓 ∈ (LocFinβ€˜π½)) ↔ ((𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})):π‘ˆβŸΆπ½ ∧ ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…}))Refπ‘ˆ ∧ ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) ∈ (LocFinβ€˜π½))))
123122spcegv 3588 . . . . . 6 ((𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) ∈ V β†’ (((𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})):π‘ˆβŸΆπ½ ∧ ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…}))Refπ‘ˆ ∧ ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) ∈ (LocFinβ€˜π½)) β†’ βˆƒπ‘“(𝑓:π‘ˆβŸΆπ½ ∧ ran 𝑓Refπ‘ˆ ∧ ran 𝑓 ∈ (LocFinβ€˜π½))))
124111, 114, 117, 1234syl 19 . . . . 5 ((πœ‘ ∧ π‘ˆ β‰  βˆ…) β†’ (((𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})):π‘ˆβŸΆπ½ ∧ ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…}))Refπ‘ˆ ∧ ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) ∈ (LocFinβ€˜π½)) β†’ βˆƒπ‘“(𝑓:π‘ˆβŸΆπ½ ∧ ran 𝑓Refπ‘ˆ ∧ ran 𝑓 ∈ (LocFinβ€˜π½))))
125124imp 408 . . . 4 (((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})):π‘ˆβŸΆπ½ ∧ ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…}))Refπ‘ˆ ∧ ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) ∈ (LocFinβ€˜π½))) β†’ βˆƒπ‘“(𝑓:π‘ˆβŸΆπ½ ∧ ran 𝑓Refπ‘ˆ ∧ ran 𝑓 ∈ (LocFinβ€˜π½)))
12649, 70, 93, 106, 125syl13anc 1373 . . 3 (((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) β†’ βˆƒπ‘“(𝑓:π‘ˆβŸΆπ½ ∧ ran 𝑓Refπ‘ˆ ∧ ran 𝑓 ∈ (LocFinβ€˜π½)))
12748, 126exlimddv 1939 . 2 ((πœ‘ ∧ π‘ˆ β‰  βˆ…) β†’ βˆƒπ‘“(𝑓:π‘ˆβŸΆπ½ ∧ ran 𝑓Refπ‘ˆ ∧ ran 𝑓 ∈ (LocFinβ€˜π½)))
12843, 127pm2.61dane 3030 1 (πœ‘ β†’ βˆƒπ‘“(𝑓:π‘ˆβŸΆπ½ ∧ ran 𝑓Refπ‘ˆ ∧ ran 𝑓 ∈ (LocFinβ€˜π½)))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∨ wo 846   ∧ w3a 1088   = wceq 1542  βˆƒwex 1782   ∈ wcel 2107   β‰  wne 2941  βˆ€wral 3062  βˆƒwrex 3071  {crab 3433  Vcvv 3475   βˆ– cdif 3946   βˆͺ cun 3947   ∩ cin 3948   βŠ† wss 3949  βˆ…c0 4323  {csn 4629  βˆͺ cuni 4909   class class class wbr 5149   Γ— cxp 5675  dom cdm 5677  ran crn 5678  Fun wfun 6538  βŸΆwf 6540  β€˜cfv 6544  Fincfn 8939  Topctop 22395  Refcref 23006  LocFinclocfin 23008
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-reg 9587  ax-inf2 9636  ax-ac2 10458
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-int 4952  df-iun 5000  df-iin 5001  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-se 5633  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-isom 6553  df-riota 7365  df-ov 7412  df-om 7856  df-2nd 7976  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-1o 8466  df-er 8703  df-en 8940  df-dom 8941  df-fin 8943  df-r1 9759  df-rank 9760  df-card 9934  df-ac 10111  df-top 22396  df-topon 22413  df-ref 23009  df-locfin 23011
This theorem is referenced by:  pcmplfinf  32841
  Copyright terms: Public domain W3C validator