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 33119
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 6771 . . . 4 βˆ…:βˆ…βŸΆπ½
2 simpr 483 . . . . 5 ((πœ‘ ∧ π‘ˆ = βˆ…) β†’ π‘ˆ = βˆ…)
32feq2d 6702 . . . 4 ((πœ‘ ∧ π‘ˆ = βˆ…) β†’ (βˆ…:π‘ˆβŸΆπ½ ↔ βˆ…:βˆ…βŸΆπ½))
41, 3mpbiri 257 . . 3 ((πœ‘ ∧ π‘ˆ = βˆ…) β†’ βˆ…:π‘ˆβŸΆπ½)
5 rn0 5924 . . . . 5 ran βˆ… = βˆ…
6 0ex 5306 . . . . . 6 βˆ… ∈ V
7 refref 23237 . . . . . 6 (βˆ… ∈ V β†’ βˆ…Refβˆ…)
86, 7ax-mp 5 . . . . 5 βˆ…Refβˆ…
95, 8eqbrtri 5168 . . . 4 ran βˆ…Refβˆ…
109, 2breqtrrid 5185 . . 3 ((πœ‘ ∧ π‘ˆ = βˆ…) β†’ ran βˆ…Refπ‘ˆ)
11 sn0top 22722 . . . . . 6 {βˆ…} ∈ Top
1211a1i 11 . . . . 5 ((πœ‘ ∧ π‘ˆ = βˆ…) β†’ {βˆ…} ∈ Top)
13 eqidd 2731 . . . . 5 ((πœ‘ ∧ π‘ˆ = βˆ…) β†’ βˆ… = βˆ…)
14 ral0 4511 . . . . . 6 βˆ€π‘₯ ∈ βˆ… βˆƒπ‘› ∈ {βˆ…} (π‘₯ ∈ 𝑛 ∧ {𝑠 ∈ ran βˆ… ∣ (𝑠 ∩ 𝑛) β‰  βˆ…} ∈ Fin)
1514a1i 11 . . . . 5 ((πœ‘ ∧ π‘ˆ = βˆ…) β†’ βˆ€π‘₯ ∈ βˆ… βˆƒπ‘› ∈ {βˆ…} (π‘₯ ∈ 𝑛 ∧ {𝑠 ∈ ran βˆ… ∣ (𝑠 ∩ 𝑛) β‰  βˆ…} ∈ Fin))
166unisn 4929 . . . . . . 7 βˆͺ {βˆ…} = βˆ…
1716eqcomi 2739 . . . . . 6 βˆ… = βˆͺ {βˆ…}
185unieqi 4920 . . . . . . 7 βˆͺ ran βˆ… = βˆͺ βˆ…
19 uni0 4938 . . . . . . 7 βˆͺ βˆ… = βˆ…
2018, 19eqtr2i 2759 . . . . . 6 βˆ… = βˆͺ ran βˆ…
2117, 20islocfin 23241 . . . . 5 (ran βˆ… ∈ (LocFinβ€˜{βˆ…}) ↔ ({βˆ…} ∈ Top ∧ βˆ… = βˆ… ∧ βˆ€π‘₯ ∈ βˆ… βˆƒπ‘› ∈ {βˆ…} (π‘₯ ∈ 𝑛 ∧ {𝑠 ∈ ran βˆ… ∣ (𝑠 ∩ 𝑛) β‰  βˆ…} ∈ Fin)))
2212, 13, 15, 21syl3anbrc 1341 . . . 4 ((πœ‘ ∧ π‘ˆ = βˆ…) β†’ ran βˆ… ∈ (LocFinβ€˜{βˆ…}))
23 locfinref.2 . . . . . . . . 9 (πœ‘ β†’ 𝑋 = βˆͺ π‘ˆ)
2423adantr 479 . . . . . . . 8 ((πœ‘ ∧ π‘ˆ = βˆ…) β†’ 𝑋 = βˆͺ π‘ˆ)
252unieqd 4921 . . . . . . . 8 ((πœ‘ ∧ π‘ˆ = βˆ…) β†’ βˆͺ π‘ˆ = βˆͺ βˆ…)
2624, 25eqtrd 2770 . . . . . . 7 ((πœ‘ ∧ π‘ˆ = βˆ…) β†’ 𝑋 = βˆͺ βˆ…)
27 locfinref.x . . . . . . 7 𝑋 = βˆͺ 𝐽
2826, 27, 193eqtr3g 2793 . . . . . 6 ((πœ‘ ∧ π‘ˆ = βˆ…) β†’ βˆͺ 𝐽 = βˆ…)
29 locfinref.5 . . . . . . . 8 (πœ‘ β†’ 𝑉 ∈ (LocFinβ€˜π½))
30 locfintop 23245 . . . . . . . 8 (𝑉 ∈ (LocFinβ€˜π½) β†’ 𝐽 ∈ Top)
31 0top 22706 . . . . . . . 8 (𝐽 ∈ Top β†’ (βˆͺ 𝐽 = βˆ… ↔ 𝐽 = {βˆ…}))
3229, 30, 313syl 18 . . . . . . 7 (πœ‘ β†’ (βˆͺ 𝐽 = βˆ… ↔ 𝐽 = {βˆ…}))
3332adantr 479 . . . . . 6 ((πœ‘ ∧ π‘ˆ = βˆ…) β†’ (βˆͺ 𝐽 = βˆ… ↔ 𝐽 = {βˆ…}))
3428, 33mpbid 231 . . . . 5 ((πœ‘ ∧ π‘ˆ = βˆ…) β†’ 𝐽 = {βˆ…})
3534fveq2d 6894 . . . 4 ((πœ‘ ∧ π‘ˆ = βˆ…) β†’ (LocFinβ€˜π½) = (LocFinβ€˜{βˆ…}))
3622, 35eleqtrrd 2834 . . 3 ((πœ‘ ∧ π‘ˆ = βˆ…) β†’ ran βˆ… ∈ (LocFinβ€˜π½))
37 feq1 6697 . . . . 5 (𝑓 = βˆ… β†’ (𝑓:π‘ˆβŸΆπ½ ↔ βˆ…:π‘ˆβŸΆπ½))
38 rneq 5934 . . . . . 6 (𝑓 = βˆ… β†’ ran 𝑓 = ran βˆ…)
3938breq1d 5157 . . . . 5 (𝑓 = βˆ… β†’ (ran 𝑓Refπ‘ˆ ↔ ran βˆ…Refπ‘ˆ))
4038eleq1d 2816 . . . . 5 (𝑓 = βˆ… β†’ (ran 𝑓 ∈ (LocFinβ€˜π½) ↔ ran βˆ… ∈ (LocFinβ€˜π½)))
4137, 39, 403anbi123d 1434 . . . 4 (𝑓 = βˆ… β†’ ((𝑓:π‘ˆβŸΆπ½ ∧ ran 𝑓Refπ‘ˆ ∧ ran 𝑓 ∈ (LocFinβ€˜π½)) ↔ (βˆ…:π‘ˆβŸΆπ½ ∧ ran βˆ…Refπ‘ˆ ∧ ran βˆ… ∈ (LocFinβ€˜π½))))
426, 41spcev 3595 . . 3 ((βˆ…:π‘ˆβŸΆπ½ ∧ ran βˆ…Refπ‘ˆ ∧ ran βˆ… ∈ (LocFinβ€˜π½)) β†’ βˆƒπ‘“(𝑓:π‘ˆβŸΆπ½ ∧ ran 𝑓Refπ‘ˆ ∧ ran 𝑓 ∈ (LocFinβ€˜π½)))
434, 10, 36, 42syl3anc 1369 . 2 ((πœ‘ ∧ π‘ˆ = βˆ…) β†’ βˆƒπ‘“(𝑓:π‘ˆβŸΆπ½ ∧ ran 𝑓Refπ‘ˆ ∧ ran 𝑓 ∈ (LocFinβ€˜π½)))
44 locfinref.1 . . . . 5 (πœ‘ β†’ π‘ˆ βŠ† 𝐽)
45 locfinref.3 . . . . 5 (πœ‘ β†’ 𝑉 βŠ† 𝐽)
46 locfinref.4 . . . . 5 (πœ‘ β†’ 𝑉Refπ‘ˆ)
4727, 44, 23, 45, 46, 29locfinreflem 33118 . . . 4 (πœ‘ β†’ βˆƒπ‘”((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½))))
4847adantr 479 . . 3 ((πœ‘ ∧ π‘ˆ β‰  βˆ…) β†’ βˆƒπ‘”((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½))))
49 simpl 481 . . . 4 (((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) β†’ (πœ‘ ∧ π‘ˆ β‰  βˆ…))
50 simprl1 1216 . . . . . . . 8 (((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) β†’ Fun 𝑔)
51 fdmrn 6748 . . . . . . . 8 (Fun 𝑔 ↔ 𝑔:dom π‘”βŸΆran 𝑔)
5250, 51sylib 217 . . . . . . 7 (((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) β†’ 𝑔:dom π‘”βŸΆran 𝑔)
53 simprl3 1218 . . . . . . 7 (((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) β†’ ran 𝑔 βŠ† 𝐽)
5452, 53fssd 6734 . . . . . 6 (((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) β†’ 𝑔:dom π‘”βŸΆπ½)
55 fconstg 6777 . . . . . . . 8 (βˆ… ∈ V β†’ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…}):(π‘ˆ βˆ– dom 𝑔)⟢{βˆ…})
566, 55mp1i 13 . . . . . . 7 (((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) β†’ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…}):(π‘ˆ βˆ– dom 𝑔)⟢{βˆ…})
57 0opn 22626 . . . . . . . . . 10 (𝐽 ∈ Top β†’ βˆ… ∈ 𝐽)
5829, 30, 573syl 18 . . . . . . . . 9 (πœ‘ β†’ βˆ… ∈ 𝐽)
5958ad2antrr 722 . . . . . . . 8 (((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) β†’ βˆ… ∈ 𝐽)
6059snssd 4811 . . . . . . 7 (((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) β†’ {βˆ…} βŠ† 𝐽)
6156, 60fssd 6734 . . . . . 6 (((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) β†’ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…}):(π‘ˆ βˆ– dom 𝑔)⟢𝐽)
62 disjdif 4470 . . . . . . 7 (dom 𝑔 ∩ (π‘ˆ βˆ– dom 𝑔)) = βˆ…
6362a1i 11 . . . . . 6 (((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) β†’ (dom 𝑔 ∩ (π‘ˆ βˆ– dom 𝑔)) = βˆ…)
64 fun2 6753 . . . . . 6 (((𝑔:dom π‘”βŸΆπ½ ∧ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…}):(π‘ˆ βˆ– dom 𝑔)⟢𝐽) ∧ (dom 𝑔 ∩ (π‘ˆ βˆ– dom 𝑔)) = βˆ…) β†’ (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})):(dom 𝑔 βˆͺ (π‘ˆ βˆ– dom 𝑔))⟢𝐽)
6554, 61, 63, 64syl21anc 834 . . . . 5 (((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) β†’ (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})):(dom 𝑔 βˆͺ (π‘ˆ βˆ– dom 𝑔))⟢𝐽)
66 simprl2 1217 . . . . . . 7 (((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) β†’ dom 𝑔 βŠ† π‘ˆ)
67 undif 4480 . . . . . . 7 (dom 𝑔 βŠ† π‘ˆ ↔ (dom 𝑔 βˆͺ (π‘ˆ βˆ– dom 𝑔)) = π‘ˆ)
6866, 67sylib 217 . . . . . 6 (((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) β†’ (dom 𝑔 βˆͺ (π‘ˆ βˆ– dom 𝑔)) = π‘ˆ)
6968feq2d 6702 . . . . 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 483 . . . . . 6 ((((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) ∧ ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) = ran 𝑔) β†’ ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) = ran 𝑔)
72 simprrl 777 . . . . . . 7 (((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) β†’ ran 𝑔Refπ‘ˆ)
7372adantr 479 . . . . . 6 ((((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) ∧ ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) = ran 𝑔) β†’ ran 𝑔Refπ‘ˆ)
7471, 73eqbrtrd 5169 . . . . 5 ((((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) ∧ ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) = ran 𝑔) β†’ ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…}))Refπ‘ˆ)
75 simpr 483 . . . . . 6 ((((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) ∧ ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) = (ran 𝑔 βˆͺ {βˆ…})) β†’ ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) = (ran 𝑔 βˆͺ {βˆ…}))
7649simprd 494 . . . . . . . 8 (((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) β†’ π‘ˆ β‰  βˆ…)
77 refun0 23239 . . . . . . . 8 ((ran 𝑔Refπ‘ˆ ∧ π‘ˆ β‰  βˆ…) β†’ (ran 𝑔 βˆͺ {βˆ…})Refπ‘ˆ)
7872, 76, 77syl2anc 582 . . . . . . 7 (((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) β†’ (ran 𝑔 βˆͺ {βˆ…})Refπ‘ˆ)
7978adantr 479 . . . . . 6 ((((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) ∧ ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) = (ran 𝑔 βˆͺ {βˆ…})) β†’ (ran 𝑔 βˆͺ {βˆ…})Refπ‘ˆ)
8075, 79eqbrtrd 5169 . . . . 5 ((((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) ∧ ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) = (ran 𝑔 βˆͺ {βˆ…})) β†’ ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…}))Refπ‘ˆ)
81 rnxpss 6170 . . . . . . 7 ran ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…}) βŠ† {βˆ…}
82 sssn 4828 . . . . . . 7 (ran ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…}) βŠ† {βˆ…} ↔ (ran ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…}) = βˆ… ∨ ran ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…}) = {βˆ…}))
8381, 82mpbi 229 . . . . . 6 (ran ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…}) = βˆ… ∨ ran ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…}) = {βˆ…})
84 rnun 6144 . . . . . . . . 9 ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) = (ran 𝑔 βˆͺ ran ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…}))
85 uneq2 4156 . . . . . . . . 9 (ran ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…}) = βˆ… β†’ (ran 𝑔 βˆͺ ran ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) = (ran 𝑔 βˆͺ βˆ…))
8684, 85eqtrid 2782 . . . . . . . 8 (ran ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…}) = βˆ… β†’ ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) = (ran 𝑔 βˆͺ βˆ…))
87 un0 4389 . . . . . . . 8 (ran 𝑔 βˆͺ βˆ…) = ran 𝑔
8886, 87eqtrdi 2786 . . . . . . 7 (ran ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…}) = βˆ… β†’ ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) = ran 𝑔)
89 uneq2 4156 . . . . . . . 8 (ran ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…}) = {βˆ…} β†’ (ran 𝑔 βˆͺ ran ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) = (ran 𝑔 βˆͺ {βˆ…}))
9084, 89eqtrid 2782 . . . . . . 7 (ran ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…}) = {βˆ…} β†’ ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) = (ran 𝑔 βˆͺ {βˆ…}))
9188, 90orim12i 905 . . . . . 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 955 . . . 4 (((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) β†’ ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…}))Refπ‘ˆ)
94 simprrr 778 . . . . . . 7 (((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) β†’ ran 𝑔 ∈ (LocFinβ€˜π½))
9594adantr 479 . . . . . 6 ((((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) ∧ ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) = ran 𝑔) β†’ ran 𝑔 ∈ (LocFinβ€˜π½))
9671, 95eqeltrd 2831 . . . . 5 ((((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) ∧ ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) = ran 𝑔) β†’ ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) ∈ (LocFinβ€˜π½))
9794adantr 479 . . . . . . 7 ((((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) ∧ ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) = (ran 𝑔 βˆͺ {βˆ…})) β†’ ran 𝑔 ∈ (LocFinβ€˜π½))
98 snfi 9046 . . . . . . . 8 {βˆ…} ∈ Fin
9998a1i 11 . . . . . . 7 ((((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) ∧ ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) = (ran 𝑔 βˆͺ {βˆ…})) β†’ {βˆ…} ∈ Fin)
10059adantr 479 . . . . . . . . 9 ((((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) ∧ ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) = (ran 𝑔 βˆͺ {βˆ…})) β†’ βˆ… ∈ 𝐽)
101100snssd 4811 . . . . . . . 8 ((((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) ∧ ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) = (ran 𝑔 βˆͺ {βˆ…})) β†’ {βˆ…} βŠ† 𝐽)
102101unissd 4917 . . . . . . 7 ((((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) ∧ ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) = (ran 𝑔 βˆͺ {βˆ…})) β†’ βˆͺ {βˆ…} βŠ† βˆͺ 𝐽)
103 lfinun 23249 . . . . . . 7 ((ran 𝑔 ∈ (LocFinβ€˜π½) ∧ {βˆ…} ∈ Fin ∧ βˆͺ {βˆ…} βŠ† βˆͺ 𝐽) β†’ (ran 𝑔 βˆͺ {βˆ…}) ∈ (LocFinβ€˜π½))
10497, 99, 102, 103syl3anc 1369 . . . . . 6 ((((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) ∧ ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) = (ran 𝑔 βˆͺ {βˆ…})) β†’ (ran 𝑔 βˆͺ {βˆ…}) ∈ (LocFinβ€˜π½))
10575, 104eqeltrd 2831 . . . . 5 ((((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) ∧ ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) = (ran 𝑔 βˆͺ {βˆ…})) β†’ ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) ∈ (LocFinβ€˜π½))
10696, 105, 92mpjaodan 955 . . . 4 (((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) β†’ ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) ∈ (LocFinβ€˜π½))
107 refrel 23232 . . . . . . . . 9 Rel Ref
108107brrelex2i 5732 . . . . . . . 8 (𝑉Refπ‘ˆ β†’ π‘ˆ ∈ V)
109 difexg 5326 . . . . . . . 8 (π‘ˆ ∈ V β†’ (π‘ˆ βˆ– dom 𝑔) ∈ V)
11046, 108, 1093syl 18 . . . . . . 7 (πœ‘ β†’ (π‘ˆ βˆ– dom 𝑔) ∈ V)
111110adantr 479 . . . . . 6 ((πœ‘ ∧ π‘ˆ β‰  βˆ…) β†’ (π‘ˆ βˆ– dom 𝑔) ∈ V)
112 p0ex 5381 . . . . . . 7 {βˆ…} ∈ V
113 xpexg 7739 . . . . . . 7 (((π‘ˆ βˆ– dom 𝑔) ∈ V ∧ {βˆ…} ∈ V) β†’ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…}) ∈ V)
114112, 113mpan2 687 . . . . . 6 ((π‘ˆ βˆ– dom 𝑔) ∈ V β†’ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…}) ∈ V)
115 vex 3476 . . . . . . 7 𝑔 ∈ V
116 unexg 7738 . . . . . . 7 ((𝑔 ∈ V ∧ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…}) ∈ V) β†’ (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) ∈ V)
117115, 116mpan 686 . . . . . 6 (((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…}) ∈ V β†’ (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) ∈ V)
118 feq1 6697 . . . . . . . 8 (𝑓 = (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) β†’ (𝑓:π‘ˆβŸΆπ½ ↔ (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})):π‘ˆβŸΆπ½))
119 rneq 5934 . . . . . . . . 9 (𝑓 = (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) β†’ ran 𝑓 = ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})))
120119breq1d 5157 . . . . . . . 8 (𝑓 = (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) β†’ (ran 𝑓Refπ‘ˆ ↔ ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…}))Refπ‘ˆ))
121119eleq1d 2816 . . . . . . . 8 (𝑓 = (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) β†’ (ran 𝑓 ∈ (LocFinβ€˜π½) ↔ ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) ∈ (LocFinβ€˜π½)))
122118, 120, 1213anbi123d 1434 . . . . . . 7 (𝑓 = (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) β†’ ((𝑓:π‘ˆβŸΆπ½ ∧ ran 𝑓Refπ‘ˆ ∧ ran 𝑓 ∈ (LocFinβ€˜π½)) ↔ ((𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})):π‘ˆβŸΆπ½ ∧ ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…}))Refπ‘ˆ ∧ ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) ∈ (LocFinβ€˜π½))))
123122spcegv 3586 . . . . . 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 405 . . . 4 (((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})):π‘ˆβŸΆπ½ ∧ ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…}))Refπ‘ˆ ∧ ran (𝑔 βˆͺ ((π‘ˆ βˆ– dom 𝑔) Γ— {βˆ…})) ∈ (LocFinβ€˜π½))) β†’ βˆƒπ‘“(𝑓:π‘ˆβŸΆπ½ ∧ ran 𝑓Refπ‘ˆ ∧ ran 𝑓 ∈ (LocFinβ€˜π½)))
12649, 70, 93, 106, 125syl13anc 1370 . . 3 (((πœ‘ ∧ π‘ˆ β‰  βˆ…) ∧ ((Fun 𝑔 ∧ dom 𝑔 βŠ† π‘ˆ ∧ ran 𝑔 βŠ† 𝐽) ∧ (ran 𝑔Refπ‘ˆ ∧ ran 𝑔 ∈ (LocFinβ€˜π½)))) β†’ βˆƒπ‘“(𝑓:π‘ˆβŸΆπ½ ∧ ran 𝑓Refπ‘ˆ ∧ ran 𝑓 ∈ (LocFinβ€˜π½)))
12748, 126exlimddv 1936 . 2 ((πœ‘ ∧ π‘ˆ β‰  βˆ…) β†’ βˆƒπ‘“(𝑓:π‘ˆβŸΆπ½ ∧ ran 𝑓Refπ‘ˆ ∧ ran 𝑓 ∈ (LocFinβ€˜π½)))
12843, 127pm2.61dane 3027 1 (πœ‘ β†’ βˆƒπ‘“(𝑓:π‘ˆβŸΆπ½ ∧ ran 𝑓Refπ‘ˆ ∧ ran 𝑓 ∈ (LocFinβ€˜π½)))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 394   ∨ wo 843   ∧ w3a 1085   = wceq 1539  βˆƒwex 1779   ∈ wcel 2104   β‰  wne 2938  βˆ€wral 3059  βˆƒwrex 3068  {crab 3430  Vcvv 3472   βˆ– cdif 3944   βˆͺ cun 3945   ∩ cin 3946   βŠ† wss 3947  βˆ…c0 4321  {csn 4627  βˆͺ cuni 4907   class class class wbr 5147   Γ— cxp 5673  dom cdm 5675  ran crn 5676  Fun wfun 6536  βŸΆwf 6538  β€˜cfv 6542  Fincfn 8941  Topctop 22615  Refcref 23226  LocFinclocfin 23228
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727  ax-reg 9589  ax-inf2 9638  ax-ac2 10460
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-iin 4999  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-se 5631  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-isom 6551  df-riota 7367  df-ov 7414  df-om 7858  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-1o 8468  df-er 8705  df-en 8942  df-dom 8943  df-fin 8945  df-r1 9761  df-rank 9762  df-card 9936  df-ac 10113  df-top 22616  df-topon 22633  df-ref 23229  df-locfin 23231
This theorem is referenced by:  pcmplfinf  33139
  Copyright terms: Public domain W3C validator