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 32810
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 6770 . . . 4 βˆ…:βˆ…βŸΆπ½
2 simpr 486 . . . . 5 ((πœ‘ ∧ π‘ˆ = βˆ…) β†’ π‘ˆ = βˆ…)
32feq2d 6701 . . . 4 ((πœ‘ ∧ π‘ˆ = βˆ…) β†’ (βˆ…:π‘ˆβŸΆπ½ ↔ βˆ…:βˆ…βŸΆπ½))
41, 3mpbiri 258 . . 3 ((πœ‘ ∧ π‘ˆ = βˆ…) β†’ βˆ…:π‘ˆβŸΆπ½)
5 rn0 5924 . . . . 5 ran βˆ… = βˆ…
6 0ex 5307 . . . . . 6 βˆ… ∈ V
7 refref 23009 . . . . . 6 (βˆ… ∈ V β†’ βˆ…Refβˆ…)
86, 7ax-mp 5 . . . . 5 βˆ…Refβˆ…
95, 8eqbrtri 5169 . . . 4 ran βˆ…Refβˆ…
109, 2breqtrrid 5186 . . 3 ((πœ‘ ∧ π‘ˆ = βˆ…) β†’ ran βˆ…Refπ‘ˆ)
11 sn0top 22494 . . . . . 6 {βˆ…} ∈ Top
1211a1i 11 . . . . 5 ((πœ‘ ∧ π‘ˆ = βˆ…) β†’ {βˆ…} ∈ Top)
13 eqidd 2734 . . . . 5 ((πœ‘ ∧ π‘ˆ = βˆ…) β†’ βˆ… = βˆ…)
14 ral0 4512 . . . . . 6 βˆ€π‘₯ ∈ βˆ… βˆƒπ‘› ∈ {βˆ…} (π‘₯ ∈ 𝑛 ∧ {𝑠 ∈ ran βˆ… ∣ (𝑠 ∩ 𝑛) β‰  βˆ…} ∈ Fin)
1514a1i 11 . . . . 5 ((πœ‘ ∧ π‘ˆ = βˆ…) β†’ βˆ€π‘₯ ∈ βˆ… βˆƒπ‘› ∈ {βˆ…} (π‘₯ ∈ 𝑛 ∧ {𝑠 ∈ ran βˆ… ∣ (𝑠 ∩ 𝑛) β‰  βˆ…} ∈ Fin))
166unisn 4930 . . . . . . 7 βˆͺ {βˆ…} = βˆ…
1716eqcomi 2742 . . . . . 6 βˆ… = βˆͺ {βˆ…}
185unieqi 4921 . . . . . . 7 βˆͺ ran βˆ… = βˆͺ βˆ…
19 uni0 4939 . . . . . . 7 βˆͺ βˆ… = βˆ…
2018, 19eqtr2i 2762 . . . . . 6 βˆ… = βˆͺ ran βˆ…
2117, 20islocfin 23013 . . . . 5 (ran βˆ… ∈ (LocFinβ€˜{βˆ…}) ↔ ({βˆ…} ∈ Top ∧ βˆ… = βˆ… ∧ βˆ€π‘₯ ∈ βˆ… βˆƒπ‘› ∈ {βˆ…} (π‘₯ ∈ 𝑛 ∧ {𝑠 ∈ ran βˆ… ∣ (𝑠 ∩ 𝑛) β‰  βˆ…} ∈ Fin)))
2212, 13, 15, 21syl3anbrc 1344 . . . 4 ((πœ‘ ∧ π‘ˆ = βˆ…) β†’ ran βˆ… ∈ (LocFinβ€˜{βˆ…}))
23 locfinref.2 . . . . . . . . 9 (πœ‘ β†’ 𝑋 = βˆͺ π‘ˆ)
2423adantr 482 . . . . . . . 8 ((πœ‘ ∧ π‘ˆ = βˆ…) β†’ 𝑋 = βˆͺ π‘ˆ)
252unieqd 4922 . . . . . . . 8 ((πœ‘ ∧ π‘ˆ = βˆ…) β†’ βˆͺ π‘ˆ = βˆͺ βˆ…)
2624, 25eqtrd 2773 . . . . . . 7 ((πœ‘ ∧ π‘ˆ = βˆ…) β†’ 𝑋 = βˆͺ βˆ…)
27 locfinref.x . . . . . . 7 𝑋 = βˆͺ 𝐽
2826, 27, 193eqtr3g 2796 . . . . . 6 ((πœ‘ ∧ π‘ˆ = βˆ…) β†’ βˆͺ 𝐽 = βˆ…)
29 locfinref.5 . . . . . . . 8 (πœ‘ β†’ 𝑉 ∈ (LocFinβ€˜π½))
30 locfintop 23017 . . . . . . . 8 (𝑉 ∈ (LocFinβ€˜π½) β†’ 𝐽 ∈ Top)
31 0top 22478 . . . . . . . 8 (𝐽 ∈ Top β†’ (βˆͺ 𝐽 = βˆ… ↔ 𝐽 = {βˆ…}))
3229, 30, 313syl 18 . . . . . . 7 (πœ‘ β†’ (βˆͺ 𝐽 = βˆ… ↔ 𝐽 = {βˆ…}))
3332adantr 482 . . . . . 6 ((πœ‘ ∧ π‘ˆ = βˆ…) β†’ (βˆͺ 𝐽 = βˆ… ↔ 𝐽 = {βˆ…}))
3428, 33mpbid 231 . . . . 5 ((πœ‘ ∧ π‘ˆ = βˆ…) β†’ 𝐽 = {βˆ…})
3534fveq2d 6893 . . . 4 ((πœ‘ ∧ π‘ˆ = βˆ…) β†’ (LocFinβ€˜π½) = (LocFinβ€˜{βˆ…}))
3622, 35eleqtrrd 2837 . . 3 ((πœ‘ ∧ π‘ˆ = βˆ…) β†’ ran βˆ… ∈ (LocFinβ€˜π½))
37 feq1 6696 . . . . 5 (𝑓 = βˆ… β†’ (𝑓:π‘ˆβŸΆπ½ ↔ βˆ…:π‘ˆβŸΆπ½))
38 rneq 5934 . . . . . 6 (𝑓 = βˆ… β†’ ran 𝑓 = ran βˆ…)
3938breq1d 5158 . . . . 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 32809 . . . 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 6747 . . . . . . . 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 6733 . . . . . 6 (((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) β†’ 𝑔:dom π‘”βŸΆπ½)
55 fconstg 6776 . . . . . . . 8 (βˆ… ∈ V β†’ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…}):(π‘ˆ βˆ– dom 𝑔)⟢{βˆ…})
566, 55mp1i 13 . . . . . . 7 (((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) β†’ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…}):(π‘ˆ βˆ– dom 𝑔)⟢{βˆ…})
57 0opn 22398 . . . . . . . . . 10 (𝐽 ∈ Top β†’ βˆ… ∈ 𝐽)
5829, 30, 573syl 18 . . . . . . . . 9 (πœ‘ β†’ βˆ… ∈ 𝐽)
5958ad2antrr 725 . . . . . . . 8 (((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) β†’ βˆ… ∈ 𝐽)
6059snssd 4812 . . . . . . 7 (((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) β†’ {βˆ…} βŠ† 𝐽)
6156, 60fssd 6733 . . . . . 6 (((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) β†’ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…}):(π‘ˆ βˆ– dom 𝑔)⟢𝐽)
62 disjdif 4471 . . . . . . 7 (dom 𝑔 ∩ (π‘ˆ βˆ– dom 𝑔)) = βˆ…
6362a1i 11 . . . . . 6 (((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) β†’ (dom 𝑔 ∩ (π‘ˆ βˆ– dom 𝑔)) = βˆ…)
64 fun2 6752 . . . . . 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 4481 . . . . . . 7 (dom 𝑔 βŠ† π‘ˆ ↔ (dom 𝑔 βˆͺ (π‘ˆ βˆ– dom 𝑔)) = π‘ˆ)
6866, 67sylib 217 . . . . . 6 (((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) β†’ (dom 𝑔 βˆͺ (π‘ˆ βˆ– dom 𝑔)) = π‘ˆ)
6968feq2d 6701 . . . . 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 5170 . . . . 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 23011 . . . . . . . 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 5170 . . . . 5 ((((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) ∧ ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) = (ran 𝑔 βˆͺ {βˆ…})) β†’ ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…}))Refπ‘ˆ)
81 rnxpss 6169 . . . . . . 7 ran ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…}) βŠ† {βˆ…}
82 sssn 4829 . . . . . . 7 (ran ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…}) βŠ† {βˆ…} ↔ (ran ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…}) = βˆ… ∨ ran ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…}) = {βˆ…}))
8381, 82mpbi 229 . . . . . 6 (ran ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…}) = βˆ… ∨ ran ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…}) = {βˆ…})
84 rnun 6143 . . . . . . . . 9 ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) = (ran 𝑔 βˆͺ ran ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…}))
85 uneq2 4157 . . . . . . . . 9 (ran ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…}) = βˆ… β†’ (ran 𝑔 βˆͺ ran ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) = (ran 𝑔 βˆͺ βˆ…))
8684, 85eqtrid 2785 . . . . . . . 8 (ran ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…}) = βˆ… β†’ ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) = (ran 𝑔 βˆͺ βˆ…))
87 un0 4390 . . . . . . . 8 (ran 𝑔 βˆͺ βˆ…) = ran 𝑔
8886, 87eqtrdi 2789 . . . . . . 7 (ran ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…}) = βˆ… β†’ ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) = ran 𝑔)
89 uneq2 4157 . . . . . . . 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 9041 . . . . . . . 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 4812 . . . . . . . 8 ((((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) ∧ ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) = (ran 𝑔 βˆͺ {βˆ…})) β†’ {βˆ…} βŠ† 𝐽)
102101unissd 4918 . . . . . . 7 ((((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) ∧ ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) = (ran 𝑔 βˆͺ {βˆ…})) β†’ βˆͺ {βˆ…} βŠ† βˆͺ 𝐽)
103 lfinun 23021 . . . . . . 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 23004 . . . . . . . . 9 Rel Ref
108107brrelex2i 5732 . . . . . . . 8 (𝑉Refπ‘ˆ β†’ π‘ˆ ∈ V)
109 difexg 5327 . . . . . . . 8 (π‘ˆ ∈ V β†’ (π‘ˆ βˆ– dom 𝑔) ∈ V)
11046, 108, 1093syl 18 . . . . . . 7 (πœ‘ β†’ (π‘ˆ βˆ– dom 𝑔) ∈ V)
111110adantr 482 . . . . . 6 ((πœ‘ ∧ π‘ˆ β‰  βˆ…) β†’ (π‘ˆ βˆ– dom 𝑔) ∈ V)
112 p0ex 5382 . . . . . . 7 {βˆ…} ∈ V
113 xpexg 7734 . . . . . . 7 (((π‘ˆ βˆ– dom 𝑔) ∈ V ∧ {βˆ…} ∈ V) β†’ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…}) ∈ V)
114112, 113mpan2 690 . . . . . 6 ((π‘ˆ βˆ– dom 𝑔) ∈ V β†’ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…}) ∈ V)
115 vex 3479 . . . . . . 7 𝑔 ∈ V
116 unexg 7733 . . . . . . 7 ((𝑔 ∈ V ∧ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…}) ∈ V) β†’ (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) ∈ V)
117115, 116mpan 689 . . . . . 6 (((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…}) ∈ V β†’ (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) ∈ V)
118 feq1 6696 . . . . . . . 8 (𝑓 = (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) β†’ (𝑓:π‘ˆβŸΆπ½ ↔ (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})):π‘ˆβŸΆπ½))
119 rneq 5934 . . . . . . . . 9 (𝑓 = (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) β†’ ran 𝑓 = ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})))
120119breq1d 5158 . . . . . . . 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 3945   βˆͺ cun 3946   ∩ cin 3947   βŠ† wss 3948  βˆ…c0 4322  {csn 4628  βˆͺ cuni 4908   class class class wbr 5148   Γ— cxp 5674  dom cdm 5676  ran crn 5677  Fun wfun 6535  βŸΆwf 6537  β€˜cfv 6541  Fincfn 8936  Topctop 22387  Refcref 22998  LocFinclocfin 23000
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 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7722  ax-reg 9584  ax-inf2 9633  ax-ac2 10455
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 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-iin 5000  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-se 5632  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6298  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6493  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-isom 6550  df-riota 7362  df-ov 7409  df-om 7853  df-2nd 7973  df-frecs 8263  df-wrecs 8294  df-recs 8368  df-rdg 8407  df-1o 8463  df-er 8700  df-en 8937  df-dom 8938  df-fin 8940  df-r1 9756  df-rank 9757  df-card 9931  df-ac 10108  df-top 22388  df-topon 22405  df-ref 23001  df-locfin 23003
This theorem is referenced by:  pcmplfinf  32830
  Copyright terms: Public domain W3C validator