Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  carsggect Structured version   Visualization version   GIF version
Theorem carsggect 33306
Description: The outer measure is countably superadditive on Caratheodory measurable sets. (Contributed by Thierry Arnoux, 31-May-2020.)
Hypotheses
Ref Expression
carsgval.1 (πœ‘ β†’ 𝑂 ∈ 𝑉)
carsgval.2 (πœ‘ β†’ 𝑀:𝒫 π‘‚βŸΆ(0[,]+∞))
carsgsiga.1 (πœ‘ β†’ (π‘€β€˜βˆ…) = 0)
carsgsiga.2 ((πœ‘ ∧ π‘₯ β‰Ό Ο‰ ∧ π‘₯ βŠ† 𝒫 𝑂) β†’ (π‘€β€˜βˆͺ π‘₯) ≀ Ξ£*𝑦 ∈ π‘₯(π‘€β€˜π‘¦))
carsggect.0 (πœ‘ β†’ Β¬ βˆ… ∈ 𝐴)
carsggect.1 (πœ‘ β†’ 𝐴 β‰Ό Ο‰)
carsggect.2 (πœ‘ β†’ 𝐴 βŠ† (toCaraSigaβ€˜π‘€))
carsggect.3 (πœ‘ β†’ Disj 𝑦 ∈ 𝐴 𝑦)
carsggect.4 ((πœ‘ ∧ π‘₯ βŠ† 𝑦 ∧ 𝑦 ∈ 𝒫 𝑂) β†’ (π‘€β€˜π‘₯) ≀ (π‘€β€˜π‘¦))
Assertion
Ref Expression
carsggect (πœ‘ β†’ Ξ£*𝑧 ∈ 𝐴(π‘€β€˜π‘§) ≀ (π‘€β€˜βˆͺ 𝐴))
Distinct variable groups:   π‘₯,𝐴,𝑦   π‘₯,𝑀,𝑦   π‘₯,𝑂,𝑦   πœ‘,π‘₯,𝑦   𝑧,𝐴   𝑧,𝑀   𝑧,𝑂,π‘₯,𝑦   πœ‘,𝑧
Allowed substitution hints:   𝑉(π‘₯,𝑦,𝑧)
Proof of Theorem carsggect
Dummy variables 𝑓 π‘˜ 𝑛 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 carsggect.1 . . 3 (πœ‘ β†’ 𝐴 β‰Ό Ο‰)
2 0ex 5307 . . . 4 βˆ… ∈ V
32a1i 11 . . 3 (πœ‘ β†’ βˆ… ∈ V)
4 carsggect.0 . . 3 (πœ‘ β†’ Β¬ βˆ… ∈ 𝐴)
5 padct 31932 . . 3 ((𝐴 β‰Ό Ο‰ ∧ βˆ… ∈ V ∧ Β¬ βˆ… ∈ 𝐴) β†’ βˆƒπ‘“(𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴)))
61, 3, 4, 5syl3anc 1372 . 2 (πœ‘ β†’ βˆƒπ‘“(𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴)))
7 nfv 1918 . . . . 5 Ⅎ𝑧(πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴)))
8 simpr1 1195 . . . . . . 7 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ 𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}))
98feqmptd 6958 . . . . . 6 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ 𝑓 = (π‘˜ ∈ β„• ↦ (π‘“β€˜π‘˜)))
109rneqd 5936 . . . . 5 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ ran 𝑓 = ran (π‘˜ ∈ β„• ↦ (π‘“β€˜π‘˜)))
117, 10esumeq1d 33022 . . . 4 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ Ξ£*𝑧 ∈ ran 𝑓(π‘€β€˜π‘§) = Ξ£*𝑧 ∈ ran (π‘˜ ∈ β„• ↦ (π‘“β€˜π‘˜))(π‘€β€˜π‘§))
12 fvex 6902 . . . . . . . . . 10 (toCaraSigaβ€˜π‘€) ∈ V
1312a1i 11 . . . . . . . . 9 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ (toCaraSigaβ€˜π‘€) ∈ V)
14 carsggect.2 . . . . . . . . . . 11 (πœ‘ β†’ 𝐴 βŠ† (toCaraSigaβ€˜π‘€))
1514adantr 482 . . . . . . . . . 10 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ 𝐴 βŠ† (toCaraSigaβ€˜π‘€))
16 carsgval.1 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝑂 ∈ 𝑉)
1716adantr 482 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ 𝑂 ∈ 𝑉)
18 carsgval.2 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝑀:𝒫 π‘‚βŸΆ(0[,]+∞))
1918adantr 482 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ 𝑀:𝒫 π‘‚βŸΆ(0[,]+∞))
20 carsgsiga.1 . . . . . . . . . . . . 13 (πœ‘ β†’ (π‘€β€˜βˆ…) = 0)
2120adantr 482 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ (π‘€β€˜βˆ…) = 0)
2217, 19, 210elcarsg 33295 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ βˆ… ∈ (toCaraSigaβ€˜π‘€))
2322snssd 4812 . . . . . . . . . 10 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ {βˆ…} βŠ† (toCaraSigaβ€˜π‘€))
2415, 23unssd 4186 . . . . . . . . 9 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ (𝐴 βˆͺ {βˆ…}) βŠ† (toCaraSigaβ€˜π‘€))
2513, 24ssexd 5324 . . . . . . . 8 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ (𝐴 βˆͺ {βˆ…}) ∈ V)
2619adantr 482 . . . . . . . . 9 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑧 ∈ (𝐴 βˆͺ {βˆ…})) β†’ 𝑀:𝒫 π‘‚βŸΆ(0[,]+∞))
2716, 18carsgcl 33292 . . . . . . . . . . . . 13 (πœ‘ β†’ (toCaraSigaβ€˜π‘€) βŠ† 𝒫 𝑂)
2814, 27sstrd 3992 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐴 βŠ† 𝒫 𝑂)
2928adantr 482 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ 𝐴 βŠ† 𝒫 𝑂)
30 0elpw 5354 . . . . . . . . . . . . 13 βˆ… ∈ 𝒫 𝑂
3130a1i 11 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ βˆ… ∈ 𝒫 𝑂)
3231snssd 4812 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ {βˆ…} βŠ† 𝒫 𝑂)
3329, 32unssd 4186 . . . . . . . . . 10 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ (𝐴 βˆͺ {βˆ…}) βŠ† 𝒫 𝑂)
3433sselda 3982 . . . . . . . . 9 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑧 ∈ (𝐴 βˆͺ {βˆ…})) β†’ 𝑧 ∈ 𝒫 𝑂)
3526, 34ffvelcdmd 7085 . . . . . . . 8 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑧 ∈ (𝐴 βˆͺ {βˆ…})) β†’ (π‘€β€˜π‘§) ∈ (0[,]+∞))
368frnd 6723 . . . . . . . 8 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ ran 𝑓 βŠ† (𝐴 βˆͺ {βˆ…}))
377, 25, 35, 36esummono 33041 . . . . . . 7 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ Ξ£*𝑧 ∈ ran 𝑓(π‘€β€˜π‘§) ≀ Ξ£*𝑧 ∈ (𝐴 βˆͺ {βˆ…})(π‘€β€˜π‘§))
38 ctex 8956 . . . . . . . . . 10 (𝐴 β‰Ό Ο‰ β†’ 𝐴 ∈ V)
391, 38syl 17 . . . . . . . . 9 (πœ‘ β†’ 𝐴 ∈ V)
4039adantr 482 . . . . . . . 8 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ 𝐴 ∈ V)
4113, 23ssexd 5324 . . . . . . . 8 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ {βˆ…} ∈ V)
4219adantr 482 . . . . . . . . 9 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑧 ∈ 𝐴) β†’ 𝑀:𝒫 π‘‚βŸΆ(0[,]+∞))
4329sselda 3982 . . . . . . . . 9 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑧 ∈ 𝐴) β†’ 𝑧 ∈ 𝒫 𝑂)
4442, 43ffvelcdmd 7085 . . . . . . . 8 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑧 ∈ 𝐴) β†’ (π‘€β€˜π‘§) ∈ (0[,]+∞))
45 elsni 4645 . . . . . . . . . . 11 (𝑧 ∈ {βˆ…} β†’ 𝑧 = βˆ…)
4645adantl 483 . . . . . . . . . 10 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑧 ∈ {βˆ…}) β†’ 𝑧 = βˆ…)
4746fveq2d 6893 . . . . . . . . 9 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑧 ∈ {βˆ…}) β†’ (π‘€β€˜π‘§) = (π‘€β€˜βˆ…))
4821adantr 482 . . . . . . . . 9 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑧 ∈ {βˆ…}) β†’ (π‘€β€˜βˆ…) = 0)
4947, 48eqtrd 2773 . . . . . . . 8 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑧 ∈ {βˆ…}) β†’ (π‘€β€˜π‘§) = 0)
5040, 41, 44, 49esumpad 33042 . . . . . . 7 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ Ξ£*𝑧 ∈ (𝐴 βˆͺ {βˆ…})(π‘€β€˜π‘§) = Ξ£*𝑧 ∈ 𝐴(π‘€β€˜π‘§))
5137, 50breqtrd 5174 . . . . . 6 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ Ξ£*𝑧 ∈ ran 𝑓(π‘€β€˜π‘§) ≀ Ξ£*𝑧 ∈ 𝐴(π‘€β€˜π‘§))
5236, 24sstrd 3992 . . . . . . . 8 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ ran 𝑓 βŠ† (toCaraSigaβ€˜π‘€))
53 ssexg 5323 . . . . . . . 8 ((ran 𝑓 βŠ† (toCaraSigaβ€˜π‘€) ∧ (toCaraSigaβ€˜π‘€) ∈ V) β†’ ran 𝑓 ∈ V)
5452, 12, 53sylancl 587 . . . . . . 7 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ ran 𝑓 ∈ V)
5519adantr 482 . . . . . . . 8 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑧 ∈ ran 𝑓) β†’ 𝑀:𝒫 π‘‚βŸΆ(0[,]+∞))
5636, 33sstrd 3992 . . . . . . . . 9 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ ran 𝑓 βŠ† 𝒫 𝑂)
5756sselda 3982 . . . . . . . 8 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑧 ∈ ran 𝑓) β†’ 𝑧 ∈ 𝒫 𝑂)
5855, 57ffvelcdmd 7085 . . . . . . 7 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑧 ∈ ran 𝑓) β†’ (π‘€β€˜π‘§) ∈ (0[,]+∞))
59 simpr2 1196 . . . . . . 7 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ 𝐴 βŠ† ran 𝑓)
607, 54, 58, 59esummono 33041 . . . . . 6 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ Ξ£*𝑧 ∈ 𝐴(π‘€β€˜π‘§) ≀ Ξ£*𝑧 ∈ ran 𝑓(π‘€β€˜π‘§))
6151, 60jca 513 . . . . 5 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ (Ξ£*𝑧 ∈ ran 𝑓(π‘€β€˜π‘§) ≀ Ξ£*𝑧 ∈ 𝐴(π‘€β€˜π‘§) ∧ Ξ£*𝑧 ∈ 𝐴(π‘€β€˜π‘§) ≀ Ξ£*𝑧 ∈ ran 𝑓(π‘€β€˜π‘§)))
62 iccssxr 13404 . . . . . . 7 (0[,]+∞) βŠ† ℝ*
6358ralrimiva 3147 . . . . . . . 8 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ βˆ€π‘§ ∈ ran 𝑓(π‘€β€˜π‘§) ∈ (0[,]+∞))
64 nfcv 2904 . . . . . . . . 9 Ⅎ𝑧ran 𝑓
6564esumcl 33017 . . . . . . . 8 ((ran 𝑓 ∈ V ∧ βˆ€π‘§ ∈ ran 𝑓(π‘€β€˜π‘§) ∈ (0[,]+∞)) β†’ Ξ£*𝑧 ∈ ran 𝑓(π‘€β€˜π‘§) ∈ (0[,]+∞))
6654, 63, 65syl2anc 585 . . . . . . 7 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ Ξ£*𝑧 ∈ ran 𝑓(π‘€β€˜π‘§) ∈ (0[,]+∞))
6762, 66sselid 3980 . . . . . 6 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ Ξ£*𝑧 ∈ ran 𝑓(π‘€β€˜π‘§) ∈ ℝ*)
6844ralrimiva 3147 . . . . . . . 8 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ βˆ€π‘§ ∈ 𝐴 (π‘€β€˜π‘§) ∈ (0[,]+∞))
69 nfcv 2904 . . . . . . . . 9 Ⅎ𝑧𝐴
7069esumcl 33017 . . . . . . . 8 ((𝐴 ∈ V ∧ βˆ€π‘§ ∈ 𝐴 (π‘€β€˜π‘§) ∈ (0[,]+∞)) β†’ Ξ£*𝑧 ∈ 𝐴(π‘€β€˜π‘§) ∈ (0[,]+∞))
7140, 68, 70syl2anc 585 . . . . . . 7 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ Ξ£*𝑧 ∈ 𝐴(π‘€β€˜π‘§) ∈ (0[,]+∞))
7262, 71sselid 3980 . . . . . 6 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ Ξ£*𝑧 ∈ 𝐴(π‘€β€˜π‘§) ∈ ℝ*)
73 xrletri3 13130 . . . . . 6 ((Ξ£*𝑧 ∈ ran 𝑓(π‘€β€˜π‘§) ∈ ℝ* ∧ Ξ£*𝑧 ∈ 𝐴(π‘€β€˜π‘§) ∈ ℝ*) β†’ (Ξ£*𝑧 ∈ ran 𝑓(π‘€β€˜π‘§) = Ξ£*𝑧 ∈ 𝐴(π‘€β€˜π‘§) ↔ (Ξ£*𝑧 ∈ ran 𝑓(π‘€β€˜π‘§) ≀ Ξ£*𝑧 ∈ 𝐴(π‘€β€˜π‘§) ∧ Ξ£*𝑧 ∈ 𝐴(π‘€β€˜π‘§) ≀ Ξ£*𝑧 ∈ ran 𝑓(π‘€β€˜π‘§))))
7467, 72, 73syl2anc 585 . . . . 5 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ (Ξ£*𝑧 ∈ ran 𝑓(π‘€β€˜π‘§) = Ξ£*𝑧 ∈ 𝐴(π‘€β€˜π‘§) ↔ (Ξ£*𝑧 ∈ ran 𝑓(π‘€β€˜π‘§) ≀ Ξ£*𝑧 ∈ 𝐴(π‘€β€˜π‘§) ∧ Ξ£*𝑧 ∈ 𝐴(π‘€β€˜π‘§) ≀ Ξ£*𝑧 ∈ ran 𝑓(π‘€β€˜π‘§))))
7561, 74mpbird 257 . . . 4 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ Ξ£*𝑧 ∈ ran 𝑓(π‘€β€˜π‘§) = Ξ£*𝑧 ∈ 𝐴(π‘€β€˜π‘§))
76 fveq2 6889 . . . . 5 (𝑧 = (π‘“β€˜π‘˜) β†’ (π‘€β€˜π‘§) = (π‘€β€˜(π‘“β€˜π‘˜)))
77 nnex 12215 . . . . . 6 β„• ∈ V
7877a1i 11 . . . . 5 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ β„• ∈ V)
7919adantr 482 . . . . . 6 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ π‘˜ ∈ β„•) β†’ 𝑀:𝒫 π‘‚βŸΆ(0[,]+∞))
8033adantr 482 . . . . . . 7 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ π‘˜ ∈ β„•) β†’ (𝐴 βˆͺ {βˆ…}) βŠ† 𝒫 𝑂)
818adantr 482 . . . . . . . 8 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ π‘˜ ∈ β„•) β†’ 𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}))
82 simpr 486 . . . . . . . 8 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ π‘˜ ∈ β„•) β†’ π‘˜ ∈ β„•)
8381, 82ffvelcdmd 7085 . . . . . . 7 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ π‘˜ ∈ β„•) β†’ (π‘“β€˜π‘˜) ∈ (𝐴 βˆͺ {βˆ…}))
8480, 83sseldd 3983 . . . . . 6 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ π‘˜ ∈ β„•) β†’ (π‘“β€˜π‘˜) ∈ 𝒫 𝑂)
8579, 84ffvelcdmd 7085 . . . . 5 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ π‘˜ ∈ β„•) β†’ (π‘€β€˜(π‘“β€˜π‘˜)) ∈ (0[,]+∞))
86 simpr 486 . . . . . . 7 ((((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ π‘˜ ∈ β„•) ∧ (π‘“β€˜π‘˜) = βˆ…) β†’ (π‘“β€˜π‘˜) = βˆ…)
8786fveq2d 6893 . . . . . 6 ((((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ π‘˜ ∈ β„•) ∧ (π‘“β€˜π‘˜) = βˆ…) β†’ (π‘€β€˜(π‘“β€˜π‘˜)) = (π‘€β€˜βˆ…))
8821ad2antrr 725 . . . . . 6 ((((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ π‘˜ ∈ β„•) ∧ (π‘“β€˜π‘˜) = βˆ…) β†’ (π‘€β€˜βˆ…) = 0)
8987, 88eqtrd 2773 . . . . 5 ((((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ π‘˜ ∈ β„•) ∧ (π‘“β€˜π‘˜) = βˆ…) β†’ (π‘€β€˜(π‘“β€˜π‘˜)) = 0)
90 cnvimass 6078 . . . . . . 7 (◑𝑓 β€œ 𝐴) βŠ† dom 𝑓
9190, 8fssdm 6735 . . . . . 6 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ (◑𝑓 β€œ 𝐴) βŠ† β„•)
92 ffun 6718 . . . . . . . . . . 11 (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) β†’ Fun 𝑓)
938, 92syl 17 . . . . . . . . . 10 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ Fun 𝑓)
9493adantr 482 . . . . . . . . 9 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ π‘˜ ∈ (β„• βˆ– (◑𝑓 β€œ 𝐴))) β†’ Fun 𝑓)
95 difpreima 7064 . . . . . . . . . . . . 13 (Fun 𝑓 β†’ (◑𝑓 β€œ ((𝐴 βˆͺ {βˆ…}) βˆ– 𝐴)) = ((◑𝑓 β€œ (𝐴 βˆͺ {βˆ…})) βˆ– (◑𝑓 β€œ 𝐴)))
968, 92, 953syl 18 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ (◑𝑓 β€œ ((𝐴 βˆͺ {βˆ…}) βˆ– 𝐴)) = ((◑𝑓 β€œ (𝐴 βˆͺ {βˆ…})) βˆ– (◑𝑓 β€œ 𝐴)))
97 fimacnv 6737 . . . . . . . . . . . . . 14 (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) β†’ (◑𝑓 β€œ (𝐴 βˆͺ {βˆ…})) = β„•)
988, 97syl 17 . . . . . . . . . . . . 13 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ (◑𝑓 β€œ (𝐴 βˆͺ {βˆ…})) = β„•)
9998difeq1d 4121 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ ((◑𝑓 β€œ (𝐴 βˆͺ {βˆ…})) βˆ– (◑𝑓 β€œ 𝐴)) = (β„• βˆ– (◑𝑓 β€œ 𝐴)))
10096, 99eqtrd 2773 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ (◑𝑓 β€œ ((𝐴 βˆͺ {βˆ…}) βˆ– 𝐴)) = (β„• βˆ– (◑𝑓 β€œ 𝐴)))
101 uncom 4153 . . . . . . . . . . . . . . . 16 ({βˆ…} βˆͺ 𝐴) = (𝐴 βˆͺ {βˆ…})
102101difeq1i 4118 . . . . . . . . . . . . . . 15 (({βˆ…} βˆͺ 𝐴) βˆ– 𝐴) = ((𝐴 βˆͺ {βˆ…}) βˆ– 𝐴)
103 difun2 4480 . . . . . . . . . . . . . . 15 (({βˆ…} βˆͺ 𝐴) βˆ– 𝐴) = ({βˆ…} βˆ– 𝐴)
104102, 103eqtr3i 2763 . . . . . . . . . . . . . 14 ((𝐴 βˆͺ {βˆ…}) βˆ– 𝐴) = ({βˆ…} βˆ– 𝐴)
105 difss 4131 . . . . . . . . . . . . . 14 ({βˆ…} βˆ– 𝐴) βŠ† {βˆ…}
106104, 105eqsstri 4016 . . . . . . . . . . . . 13 ((𝐴 βˆͺ {βˆ…}) βˆ– 𝐴) βŠ† {βˆ…}
107106a1i 11 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ ((𝐴 βˆͺ {βˆ…}) βˆ– 𝐴) βŠ† {βˆ…})
108 sspreima 7067 . . . . . . . . . . . 12 ((Fun 𝑓 ∧ ((𝐴 βˆͺ {βˆ…}) βˆ– 𝐴) βŠ† {βˆ…}) β†’ (◑𝑓 β€œ ((𝐴 βˆͺ {βˆ…}) βˆ– 𝐴)) βŠ† (◑𝑓 β€œ {βˆ…}))
10993, 107, 108syl2anc 585 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ (◑𝑓 β€œ ((𝐴 βˆͺ {βˆ…}) βˆ– 𝐴)) βŠ† (◑𝑓 β€œ {βˆ…}))
110100, 109eqsstrrd 4021 . . . . . . . . . 10 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ (β„• βˆ– (◑𝑓 β€œ 𝐴)) βŠ† (◑𝑓 β€œ {βˆ…}))
111110sselda 3982 . . . . . . . . 9 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ π‘˜ ∈ (β„• βˆ– (◑𝑓 β€œ 𝐴))) β†’ π‘˜ ∈ (◑𝑓 β€œ {βˆ…}))
112 fvimacnvi 7051 . . . . . . . . 9 ((Fun 𝑓 ∧ π‘˜ ∈ (◑𝑓 β€œ {βˆ…})) β†’ (π‘“β€˜π‘˜) ∈ {βˆ…})
11394, 111, 112syl2anc 585 . . . . . . . 8 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ π‘˜ ∈ (β„• βˆ– (◑𝑓 β€œ 𝐴))) β†’ (π‘“β€˜π‘˜) ∈ {βˆ…})
114 elsni 4645 . . . . . . . 8 ((π‘“β€˜π‘˜) ∈ {βˆ…} β†’ (π‘“β€˜π‘˜) = βˆ…)
115113, 114syl 17 . . . . . . 7 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ π‘˜ ∈ (β„• βˆ– (◑𝑓 β€œ 𝐴))) β†’ (π‘“β€˜π‘˜) = βˆ…)
116115ralrimiva 3147 . . . . . 6 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ βˆ€π‘˜ ∈ (β„• βˆ– (◑𝑓 β€œ 𝐴))(π‘“β€˜π‘˜) = βˆ…)
117 carsggect.3 . . . . . . . 8 (πœ‘ β†’ Disj 𝑦 ∈ 𝐴 𝑦)
118117adantr 482 . . . . . . 7 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ Disj 𝑦 ∈ 𝐴 𝑦)
119 simpr3 1197 . . . . . . . . . 10 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ Fun (◑𝑓 β†Ύ 𝐴))
120 fresf1o 31843 . . . . . . . . . 10 ((Fun 𝑓 ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴)) β†’ (𝑓 β†Ύ (◑𝑓 β€œ 𝐴)):(◑𝑓 β€œ 𝐴)–1-1-onto→𝐴)
12193, 59, 119, 120syl3anc 1372 . . . . . . . . 9 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ (𝑓 β†Ύ (◑𝑓 β€œ 𝐴)):(◑𝑓 β€œ 𝐴)–1-1-onto→𝐴)
122 simpr 486 . . . . . . . . 9 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑦 = ((𝑓 β†Ύ (◑𝑓 β€œ 𝐴))β€˜π‘˜)) β†’ 𝑦 = ((𝑓 β†Ύ (◑𝑓 β€œ 𝐴))β€˜π‘˜))
123121, 122disjrdx 31810 . . . . . . . 8 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ (Disj π‘˜ ∈ (◑𝑓 β€œ 𝐴)((𝑓 β†Ύ (◑𝑓 β€œ 𝐴))β€˜π‘˜) ↔ Disj 𝑦 ∈ 𝐴 𝑦))
124 fvres 6908 . . . . . . . . . 10 (π‘˜ ∈ (◑𝑓 β€œ 𝐴) β†’ ((𝑓 β†Ύ (◑𝑓 β€œ 𝐴))β€˜π‘˜) = (π‘“β€˜π‘˜))
125124adantl 483 . . . . . . . . 9 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ π‘˜ ∈ (◑𝑓 β€œ 𝐴)) β†’ ((𝑓 β†Ύ (◑𝑓 β€œ 𝐴))β€˜π‘˜) = (π‘“β€˜π‘˜))
126125disjeq2dv 5118 . . . . . . . 8 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ (Disj π‘˜ ∈ (◑𝑓 β€œ 𝐴)((𝑓 β†Ύ (◑𝑓 β€œ 𝐴))β€˜π‘˜) ↔ Disj π‘˜ ∈ (◑𝑓 β€œ 𝐴)(π‘“β€˜π‘˜)))
127123, 126bitr3d 281 . . . . . . 7 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ (Disj 𝑦 ∈ 𝐴 𝑦 ↔ Disj π‘˜ ∈ (◑𝑓 β€œ 𝐴)(π‘“β€˜π‘˜)))
128118, 127mpbid 231 . . . . . 6 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ Disj π‘˜ ∈ (◑𝑓 β€œ 𝐴)(π‘“β€˜π‘˜))
129 disjss3 5147 . . . . . . 7 (((◑𝑓 β€œ 𝐴) βŠ† β„• ∧ βˆ€π‘˜ ∈ (β„• βˆ– (◑𝑓 β€œ 𝐴))(π‘“β€˜π‘˜) = βˆ…) β†’ (Disj π‘˜ ∈ (◑𝑓 β€œ 𝐴)(π‘“β€˜π‘˜) ↔ Disj π‘˜ ∈ β„• (π‘“β€˜π‘˜)))
130129biimpa 478 . . . . . 6 ((((◑𝑓 β€œ 𝐴) βŠ† β„• ∧ βˆ€π‘˜ ∈ (β„• βˆ– (◑𝑓 β€œ 𝐴))(π‘“β€˜π‘˜) = βˆ…) ∧ Disj π‘˜ ∈ (◑𝑓 β€œ 𝐴)(π‘“β€˜π‘˜)) β†’ Disj π‘˜ ∈ β„• (π‘“β€˜π‘˜))
13191, 116, 128, 130syl21anc 837 . . . . 5 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ Disj π‘˜ ∈ β„• (π‘“β€˜π‘˜))
13276, 78, 85, 84, 89, 131esumrnmpt2 33055 . . . 4 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ Ξ£*𝑧 ∈ ran (π‘˜ ∈ β„• ↦ (π‘“β€˜π‘˜))(π‘€β€˜π‘§) = Ξ£*π‘˜ ∈ β„•(π‘€β€˜(π‘“β€˜π‘˜)))
13311, 75, 1323eqtr3rd 2782 . . 3 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ Ξ£*π‘˜ ∈ β„•(π‘€β€˜(π‘“β€˜π‘˜)) = Ξ£*𝑧 ∈ 𝐴(π‘€β€˜π‘§))
134 uniiun 5061 . . . . . . 7 βˆͺ 𝐴 = βˆͺ π‘₯ ∈ 𝐴 π‘₯
13528sselda 3982 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ 𝐴) β†’ π‘₯ ∈ 𝒫 𝑂)
13639, 135elpwiuncl 31753 . . . . . . 7 (πœ‘ β†’ βˆͺ π‘₯ ∈ 𝐴 π‘₯ ∈ 𝒫 𝑂)
137134, 136eqeltrid 2838 . . . . . 6 (πœ‘ β†’ βˆͺ 𝐴 ∈ 𝒫 𝑂)
138137adantr 482 . . . . 5 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ βˆͺ 𝐴 ∈ 𝒫 𝑂)
13919, 138ffvelcdmd 7085 . . . 4 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ (π‘€β€˜βˆͺ 𝐴) ∈ (0[,]+∞))
140 carsgsiga.2 . . . . . . . . . 10 ((πœ‘ ∧ π‘₯ β‰Ό Ο‰ ∧ π‘₯ βŠ† 𝒫 𝑂) β†’ (π‘€β€˜βˆͺ π‘₯) ≀ Ξ£*𝑦 ∈ π‘₯(π‘€β€˜π‘¦))
1411403adant1r 1178 . . . . . . . . 9 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ π‘₯ β‰Ό Ο‰ ∧ π‘₯ βŠ† 𝒫 𝑂) β†’ (π‘€β€˜βˆͺ π‘₯) ≀ Ξ£*𝑦 ∈ π‘₯(π‘€β€˜π‘¦))
142 fveq2 6889 . . . . . . . . . 10 (𝑦 = 𝑧 β†’ (π‘€β€˜π‘¦) = (π‘€β€˜π‘§))
143 nfcv 2904 . . . . . . . . . 10 Ⅎ𝑧π‘₯
144 nfcv 2904 . . . . . . . . . 10 Ⅎ𝑦π‘₯
145 nfcv 2904 . . . . . . . . . 10 Ⅎ𝑧(π‘€β€˜π‘¦)
146 nfcv 2904 . . . . . . . . . 10 Ⅎ𝑦(π‘€β€˜π‘§)
147142, 143, 144, 145, 146cbvesum 33029 . . . . . . . . 9 Ξ£*𝑦 ∈ π‘₯(π‘€β€˜π‘¦) = Ξ£*𝑧 ∈ π‘₯(π‘€β€˜π‘§)
148141, 147breqtrdi 5189 . . . . . . . 8 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ π‘₯ β‰Ό Ο‰ ∧ π‘₯ βŠ† 𝒫 𝑂) β†’ (π‘€β€˜βˆͺ π‘₯) ≀ Ξ£*𝑧 ∈ π‘₯(π‘€β€˜π‘§))
149 ffn 6715 . . . . . . . . . 10 (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) β†’ 𝑓 Fn β„•)
150 fz1ssnn 13529 . . . . . . . . . . 11 (1...𝑛) βŠ† β„•
151 fnssres 6671 . . . . . . . . . . 11 ((𝑓 Fn β„• ∧ (1...𝑛) βŠ† β„•) β†’ (𝑓 β†Ύ (1...𝑛)) Fn (1...𝑛))
152150, 151mpan2 690 . . . . . . . . . 10 (𝑓 Fn β„• β†’ (𝑓 β†Ύ (1...𝑛)) Fn (1...𝑛))
1538, 149, 1523syl 18 . . . . . . . . 9 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ (𝑓 β†Ύ (1...𝑛)) Fn (1...𝑛))
154 fzfi 13934 . . . . . . . . . 10 (1...𝑛) ∈ Fin
155 fnfi 9178 . . . . . . . . . 10 (((𝑓 β†Ύ (1...𝑛)) Fn (1...𝑛) ∧ (1...𝑛) ∈ Fin) β†’ (𝑓 β†Ύ (1...𝑛)) ∈ Fin)
156154, 155mpan2 690 . . . . . . . . 9 ((𝑓 β†Ύ (1...𝑛)) Fn (1...𝑛) β†’ (𝑓 β†Ύ (1...𝑛)) ∈ Fin)
157 rnfi 9332 . . . . . . . . 9 ((𝑓 β†Ύ (1...𝑛)) ∈ Fin β†’ ran (𝑓 β†Ύ (1...𝑛)) ∈ Fin)
158153, 156, 1573syl 18 . . . . . . . 8 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ ran (𝑓 β†Ύ (1...𝑛)) ∈ Fin)
159 resss 6005 . . . . . . . . . . 11 (𝑓 β†Ύ (1...𝑛)) βŠ† 𝑓
160 rnss 5937 . . . . . . . . . . 11 ((𝑓 β†Ύ (1...𝑛)) βŠ† 𝑓 β†’ ran (𝑓 β†Ύ (1...𝑛)) βŠ† ran 𝑓)
161159, 160ax-mp 5 . . . . . . . . . 10 ran (𝑓 β†Ύ (1...𝑛)) βŠ† ran 𝑓
162161a1i 11 . . . . . . . . 9 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ ran (𝑓 β†Ύ (1...𝑛)) βŠ† ran 𝑓)
163162, 52sstrd 3992 . . . . . . . 8 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ ran (𝑓 β†Ύ (1...𝑛)) βŠ† (toCaraSigaβ€˜π‘€))
164162, 36sstrd 3992 . . . . . . . . 9 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ ran (𝑓 β†Ύ (1...𝑛)) βŠ† (𝐴 βˆͺ {βˆ…}))
165 nfcv 2904 . . . . . . . . . . . . 13 Ⅎ𝑧𝑦
166 nfcv 2904 . . . . . . . . . . . . 13 Ⅎ𝑦𝑧
167 id 22 . . . . . . . . . . . . 13 (𝑦 = 𝑧 β†’ 𝑦 = 𝑧)
168165, 166, 167cbvdisj 5123 . . . . . . . . . . . 12 (Disj 𝑦 ∈ 𝐴 𝑦 ↔ Disj 𝑧 ∈ 𝐴 𝑧)
169 disjun0 31814 . . . . . . . . . . . 12 (Disj 𝑧 ∈ 𝐴 𝑧 β†’ Disj 𝑧 ∈ (𝐴 βˆͺ {βˆ…})𝑧)
170168, 169sylbi 216 . . . . . . . . . . 11 (Disj 𝑦 ∈ 𝐴 𝑦 β†’ Disj 𝑧 ∈ (𝐴 βˆͺ {βˆ…})𝑧)
171117, 170syl 17 . . . . . . . . . 10 (πœ‘ β†’ Disj 𝑧 ∈ (𝐴 βˆͺ {βˆ…})𝑧)
172171adantr 482 . . . . . . . . 9 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ Disj 𝑧 ∈ (𝐴 βˆͺ {βˆ…})𝑧)
173 disjss1 5119 . . . . . . . . 9 (ran (𝑓 β†Ύ (1...𝑛)) βŠ† (𝐴 βˆͺ {βˆ…}) β†’ (Disj 𝑧 ∈ (𝐴 βˆͺ {βˆ…})𝑧 β†’ Disj 𝑧 ∈ ran (𝑓 β†Ύ (1...𝑛))𝑧))
174164, 172, 173sylc 65 . . . . . . . 8 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ Disj 𝑧 ∈ ran (𝑓 β†Ύ (1...𝑛))𝑧)
175 pwidg 4622 . . . . . . . . 9 (𝑂 ∈ 𝑉 β†’ 𝑂 ∈ 𝒫 𝑂)
17617, 175syl 17 . . . . . . . 8 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ 𝑂 ∈ 𝒫 𝑂)
17717, 19, 21, 148, 158, 163, 174, 176carsgclctunlem1 33305 . . . . . . 7 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ (π‘€β€˜(𝑂 ∩ βˆͺ ran (𝑓 β†Ύ (1...𝑛)))) = Ξ£*𝑧 ∈ ran (𝑓 β†Ύ (1...𝑛))(π‘€β€˜(𝑂 ∩ 𝑧)))
178177adantr 482 . . . . . 6 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•) β†’ (π‘€β€˜(𝑂 ∩ βˆͺ ran (𝑓 β†Ύ (1...𝑛)))) = Ξ£*𝑧 ∈ ran (𝑓 β†Ύ (1...𝑛))(π‘€β€˜(𝑂 ∩ 𝑧)))
179164unissd 4918 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ βˆͺ ran (𝑓 β†Ύ (1...𝑛)) βŠ† βˆͺ (𝐴 βˆͺ {βˆ…}))
180 uniun 4934 . . . . . . . . . . . 12 βˆͺ (𝐴 βˆͺ {βˆ…}) = (βˆͺ 𝐴 βˆͺ βˆͺ {βˆ…})
1812unisn 4930 . . . . . . . . . . . . 13 βˆͺ {βˆ…} = βˆ…
182181uneq2i 4160 . . . . . . . . . . . 12 (βˆͺ 𝐴 βˆͺ βˆͺ {βˆ…}) = (βˆͺ 𝐴 βˆͺ βˆ…)
183 un0 4390 . . . . . . . . . . . 12 (βˆͺ 𝐴 βˆͺ βˆ…) = βˆͺ 𝐴
184180, 182, 1833eqtri 2765 . . . . . . . . . . 11 βˆͺ (𝐴 βˆͺ {βˆ…}) = βˆͺ 𝐴
185179, 184sseqtrdi 4032 . . . . . . . . . 10 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ βˆͺ ran (𝑓 β†Ύ (1...𝑛)) βŠ† βˆͺ 𝐴)
186185adantr 482 . . . . . . . . 9 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•) β†’ βˆͺ ran (𝑓 β†Ύ (1...𝑛)) βŠ† βˆͺ 𝐴)
187 uniss 4916 . . . . . . . . . . . 12 (𝐴 βŠ† 𝒫 𝑂 β†’ βˆͺ 𝐴 βŠ† βˆͺ 𝒫 𝑂)
188 unipw 5450 . . . . . . . . . . . 12 βˆͺ 𝒫 𝑂 = 𝑂
189187, 188sseqtrdi 4032 . . . . . . . . . . 11 (𝐴 βŠ† 𝒫 𝑂 β†’ βˆͺ 𝐴 βŠ† 𝑂)
19028, 189syl 17 . . . . . . . . . 10 (πœ‘ β†’ βˆͺ 𝐴 βŠ† 𝑂)
191190ad2antrr 725 . . . . . . . . 9 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•) β†’ βˆͺ 𝐴 βŠ† 𝑂)
192186, 191sstrd 3992 . . . . . . . 8 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•) β†’ βˆͺ ran (𝑓 β†Ύ (1...𝑛)) βŠ† 𝑂)
193 sseqin2 4215 . . . . . . . 8 (βˆͺ ran (𝑓 β†Ύ (1...𝑛)) βŠ† 𝑂 ↔ (𝑂 ∩ βˆͺ ran (𝑓 β†Ύ (1...𝑛))) = βˆͺ ran (𝑓 β†Ύ (1...𝑛)))
194192, 193sylib 217 . . . . . . 7 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•) β†’ (𝑂 ∩ βˆͺ ran (𝑓 β†Ύ (1...𝑛))) = βˆͺ ran (𝑓 β†Ύ (1...𝑛)))
195194fveq2d 6893 . . . . . 6 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•) β†’ (π‘€β€˜(𝑂 ∩ βˆͺ ran (𝑓 β†Ύ (1...𝑛)))) = (π‘€β€˜βˆͺ ran (𝑓 β†Ύ (1...𝑛))))
196 nfv 1918 . . . . . . . 8 Ⅎ𝑧((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•)
197164adantr 482 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•) β†’ ran (𝑓 β†Ύ (1...𝑛)) βŠ† (𝐴 βˆͺ {βˆ…}))
19828ad2antrr 725 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•) β†’ 𝐴 βŠ† 𝒫 𝑂)
19930a1i 11 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•) β†’ βˆ… ∈ 𝒫 𝑂)
200199snssd 4812 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•) β†’ {βˆ…} βŠ† 𝒫 𝑂)
201198, 200unssd 4186 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•) β†’ (𝐴 βˆͺ {βˆ…}) βŠ† 𝒫 𝑂)
202197, 201sstrd 3992 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•) β†’ ran (𝑓 β†Ύ (1...𝑛)) βŠ† 𝒫 𝑂)
203202sselda 3982 . . . . . . . . . . . 12 ((((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•) ∧ 𝑧 ∈ ran (𝑓 β†Ύ (1...𝑛))) β†’ 𝑧 ∈ 𝒫 𝑂)
204203elpwid 4611 . . . . . . . . . . 11 ((((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•) ∧ 𝑧 ∈ ran (𝑓 β†Ύ (1...𝑛))) β†’ 𝑧 βŠ† 𝑂)
205 sseqin2 4215 . . . . . . . . . . 11 (𝑧 βŠ† 𝑂 ↔ (𝑂 ∩ 𝑧) = 𝑧)
206204, 205sylib 217 . . . . . . . . . 10 ((((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•) ∧ 𝑧 ∈ ran (𝑓 β†Ύ (1...𝑛))) β†’ (𝑂 ∩ 𝑧) = 𝑧)
207206fveq2d 6893 . . . . . . . . 9 ((((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•) ∧ 𝑧 ∈ ran (𝑓 β†Ύ (1...𝑛))) β†’ (π‘€β€˜(𝑂 ∩ 𝑧)) = (π‘€β€˜π‘§))
208207ralrimiva 3147 . . . . . . . 8 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•) β†’ βˆ€π‘§ ∈ ran (𝑓 β†Ύ (1...𝑛))(π‘€β€˜(𝑂 ∩ 𝑧)) = (π‘€β€˜π‘§))
209196, 208esumeq2d 33024 . . . . . . 7 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•) β†’ Ξ£*𝑧 ∈ ran (𝑓 β†Ύ (1...𝑛))(π‘€β€˜(𝑂 ∩ 𝑧)) = Ξ£*𝑧 ∈ ran (𝑓 β†Ύ (1...𝑛))(π‘€β€˜π‘§))
2109reseq1d 5979 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ (𝑓 β†Ύ (1...𝑛)) = ((π‘˜ ∈ β„• ↦ (π‘“β€˜π‘˜)) β†Ύ (1...𝑛)))
211210adantr 482 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•) β†’ (𝑓 β†Ύ (1...𝑛)) = ((π‘˜ ∈ β„• ↦ (π‘“β€˜π‘˜)) β†Ύ (1...𝑛)))
212 resmpt 6036 . . . . . . . . . . . 12 ((1...𝑛) βŠ† β„• β†’ ((π‘˜ ∈ β„• ↦ (π‘“β€˜π‘˜)) β†Ύ (1...𝑛)) = (π‘˜ ∈ (1...𝑛) ↦ (π‘“β€˜π‘˜)))
213150, 212ax-mp 5 . . . . . . . . . . 11 ((π‘˜ ∈ β„• ↦ (π‘“β€˜π‘˜)) β†Ύ (1...𝑛)) = (π‘˜ ∈ (1...𝑛) ↦ (π‘“β€˜π‘˜))
214211, 213eqtrdi 2789 . . . . . . . . . 10 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•) β†’ (𝑓 β†Ύ (1...𝑛)) = (π‘˜ ∈ (1...𝑛) ↦ (π‘“β€˜π‘˜)))
215214eqcomd 2739 . . . . . . . . 9 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•) β†’ (π‘˜ ∈ (1...𝑛) ↦ (π‘“β€˜π‘˜)) = (𝑓 β†Ύ (1...𝑛)))
216215rneqd 5936 . . . . . . . 8 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•) β†’ ran (π‘˜ ∈ (1...𝑛) ↦ (π‘“β€˜π‘˜)) = ran (𝑓 β†Ύ (1...𝑛)))
217196, 216esumeq1d 33022 . . . . . . 7 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•) β†’ Ξ£*𝑧 ∈ ran (π‘˜ ∈ (1...𝑛) ↦ (π‘“β€˜π‘˜))(π‘€β€˜π‘§) = Ξ£*𝑧 ∈ ran (𝑓 β†Ύ (1...𝑛))(π‘€β€˜π‘§))
218154a1i 11 . . . . . . . 8 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•) β†’ (1...𝑛) ∈ Fin)
21919ad2antrr 725 . . . . . . . . 9 ((((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ 𝑀:𝒫 π‘‚βŸΆ(0[,]+∞))
220150a1i 11 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•) β†’ (1...𝑛) βŠ† β„•)
221220sselda 3982 . . . . . . . . . 10 ((((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ π‘˜ ∈ β„•)
22284adantlr 714 . . . . . . . . . 10 ((((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ β„•) β†’ (π‘“β€˜π‘˜) ∈ 𝒫 𝑂)
223221, 222syldan 592 . . . . . . . . 9 ((((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (π‘“β€˜π‘˜) ∈ 𝒫 𝑂)
224219, 223ffvelcdmd 7085 . . . . . . . 8 ((((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (π‘€β€˜(π‘“β€˜π‘˜)) ∈ (0[,]+∞))
225 simpr 486 . . . . . . . . . 10 (((((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) ∧ (π‘“β€˜π‘˜) = βˆ…) β†’ (π‘“β€˜π‘˜) = βˆ…)
226225fveq2d 6893 . . . . . . . . 9 (((((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) ∧ (π‘“β€˜π‘˜) = βˆ…) β†’ (π‘€β€˜(π‘“β€˜π‘˜)) = (π‘€β€˜βˆ…))
22721ad3antrrr 729 . . . . . . . . 9 (((((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) ∧ (π‘“β€˜π‘˜) = βˆ…) β†’ (π‘€β€˜βˆ…) = 0)
228226, 227eqtrd 2773 . . . . . . . 8 (((((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) ∧ (π‘“β€˜π‘˜) = βˆ…) β†’ (π‘€β€˜(π‘“β€˜π‘˜)) = 0)
229 disjss1 5119 . . . . . . . . . . 11 ((1...𝑛) βŠ† β„• β†’ (Disj π‘˜ ∈ β„• (π‘“β€˜π‘˜) β†’ Disj π‘˜ ∈ (1...𝑛)(π‘“β€˜π‘˜)))
230150, 229ax-mp 5 . . . . . . . . . 10 (Disj π‘˜ ∈ β„• (π‘“β€˜π‘˜) β†’ Disj π‘˜ ∈ (1...𝑛)(π‘“β€˜π‘˜))
231131, 230syl 17 . . . . . . . . 9 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ Disj π‘˜ ∈ (1...𝑛)(π‘“β€˜π‘˜))
232231adantr 482 . . . . . . . 8 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•) β†’ Disj π‘˜ ∈ (1...𝑛)(π‘“β€˜π‘˜))
23376, 218, 224, 223, 228, 232esumrnmpt2 33055 . . . . . . 7 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•) β†’ Ξ£*𝑧 ∈ ran (π‘˜ ∈ (1...𝑛) ↦ (π‘“β€˜π‘˜))(π‘€β€˜π‘§) = Ξ£*π‘˜ ∈ (1...𝑛)(π‘€β€˜(π‘“β€˜π‘˜)))
234209, 217, 2333eqtr2d 2779 . . . . . 6 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•) β†’ Ξ£*𝑧 ∈ ran (𝑓 β†Ύ (1...𝑛))(π‘€β€˜(𝑂 ∩ 𝑧)) = Ξ£*π‘˜ ∈ (1...𝑛)(π‘€β€˜(π‘“β€˜π‘˜)))
235178, 195, 2343eqtr3d 2781 . . . . 5 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•) β†’ (π‘€β€˜βˆͺ ran (𝑓 β†Ύ (1...𝑛))) = Ξ£*π‘˜ ∈ (1...𝑛)(π‘€β€˜(π‘“β€˜π‘˜)))
236 carsggect.4 . . . . . . . 8 ((πœ‘ ∧ π‘₯ βŠ† 𝑦 ∧ 𝑦 ∈ 𝒫 𝑂) β†’ (π‘€β€˜π‘₯) ≀ (π‘€β€˜π‘¦))
2372363adant1r 1178 . . . . . . 7 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ π‘₯ βŠ† 𝑦 ∧ 𝑦 ∈ 𝒫 𝑂) β†’ (π‘€β€˜π‘₯) ≀ (π‘€β€˜π‘¦))
23817, 19, 185, 138, 237carsgmon 33302 . . . . . 6 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ (π‘€β€˜βˆͺ ran (𝑓 β†Ύ (1...𝑛))) ≀ (π‘€β€˜βˆͺ 𝐴))
239238adantr 482 . . . . 5 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•) β†’ (π‘€β€˜βˆͺ ran (𝑓 β†Ύ (1...𝑛))) ≀ (π‘€β€˜βˆͺ 𝐴))
240235, 239eqbrtrrd 5172 . . . 4 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•) β†’ Ξ£*π‘˜ ∈ (1...𝑛)(π‘€β€˜(π‘“β€˜π‘˜)) ≀ (π‘€β€˜βˆͺ 𝐴))
241139, 85, 240esumgect 33077 . . 3 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ Ξ£*π‘˜ ∈ β„•(π‘€β€˜(π‘“β€˜π‘˜)) ≀ (π‘€β€˜βˆͺ 𝐴))
242133, 241eqbrtrrd 5172 . 2 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ Ξ£*𝑧 ∈ 𝐴(π‘€β€˜π‘§) ≀ (π‘€β€˜βˆͺ 𝐴))
2436, 242exlimddv 1939 1 (πœ‘ β†’ Ξ£*𝑧 ∈ 𝐴(π‘€β€˜π‘§) ≀ (π‘€β€˜βˆͺ 𝐴))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088   = wceq 1542  βˆƒwex 1782   ∈ wcel 2107  βˆ€wral 3062  Vcvv 3475   βˆ– cdif 3945   βˆͺ cun 3946   ∩ cin 3947   βŠ† wss 3948  βˆ…c0 4322  π’« cpw 4602  {csn 4628  βˆͺ cuni 4908  βˆͺ ciun 4997  Disj wdisj 5113   class class class wbr 5148   ↦ cmpt 5231  β—‘ccnv 5675  ran crn 5677   β†Ύ cres 5678   β€œ cima 5679  Fun wfun 6535   Fn wfn 6536  βŸΆwf 6537  β€“1-1-ontoβ†’wf1o 6540  β€˜cfv 6541  (class class class)co 7406  Ο‰com 7852   β‰Ό cdom 8934  Fincfn 8936  0cc0 11107  1c1 11108  +∞cpnf 11242  β„*cxr 11244   ≀ cle 11246  β„•cn 12209  [,]cicc 13324  ...cfz 13481  Ξ£*cesum 33014  toCaraSigaccarsg 33289
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-inf2 9633  ax-cnex 11163  ax-resscn 11164  ax-1cn 11165  ax-icn 11166  ax-addcl 11167  ax-addrcl 11168  ax-mulcl 11169  ax-mulrcl 11170  ax-mulcom 11171  ax-addass 11172  ax-mulass 11173  ax-distr 11174  ax-i2m1 11175  ax-1ne0 11176  ax-1rid 11177  ax-rnegex 11178  ax-rrecex 11179  ax-cnre 11180  ax-pre-lttri 11181  ax-pre-lttrn 11182  ax-pre-ltadd 11183  ax-pre-mulgt0 11184  ax-pre-sup 11185  ax-addf 11186  ax-mulf 11187
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-nel 3048  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-tp 4633  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-iin 5000  df-disj 5114  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-oprab 7410  df-mpo 7411  df-of 7667  df-om 7853  df-1st 7972  df-2nd 7973  df-supp 8144  df-frecs 8263  df-wrecs 8294  df-recs 8368  df-rdg 8407  df-1o 8463  df-2o 8464  df-er 8700  df-map 8819  df-pm 8820  df-ixp 8889  df-en 8937  df-dom 8938  df-sdom 8939  df-fin 8940  df-fsupp 9359  df-fi 9403  df-sup 9434  df-inf 9435  df-oi 9502  df-dju 9893  df-card 9931  df-pnf 11247  df-mnf 11248  df-xr 11249  df-ltxr 11250  df-le 11251  df-sub 11443  df-neg 11444  df-div 11869  df-nn 12210  df-2 12272  df-3 12273  df-4 12274  df-5 12275  df-6 12276  df-7 12277  df-8 12278  df-9 12279  df-n0 12470  df-z 12556  df-dec 12675  df-uz 12820  df-q 12930  df-rp 12972  df-xneg 13089  df-xadd 13090  df-xmul 13091  df-ioo 13325  df-ioc 13326  df-ico 13327  df-icc 13328  df-fz 13482  df-fzo 13625  df-fl 13754  df-mod 13832  df-seq 13964  df-exp 14025  df-fac 14231  df-bc 14260  df-hash 14288  df-shft 15011  df-cj 15043  df-re 15044  df-im 15045  df-sqrt 15179  df-abs 15180  df-limsup 15412  df-clim 15429  df-rlim 15430  df-sum 15630  df-ef 16008  df-sin 16010  df-cos 16011  df-pi 16013  df-struct 17077  df-sets 17094  df-slot 17112  df-ndx 17124  df-base 17142  df-ress 17171  df-plusg 17207  df-mulr 17208  df-starv 17209  df-sca 17210  df-vsca 17211  df-ip 17212  df-tset 17213  df-ple 17214  df-ds 17216  df-unif 17217  df-hom 17218  df-cco 17219  df-rest 17365  df-topn 17366  df-0g 17384  df-gsum 17385  df-topgen 17386  df-pt 17387  df-prds 17390  df-ordt 17444  df-xrs 17445  df-qtop 17450  df-imas 17451  df-xps 17453  df-mre 17527  df-mrc 17528  df-acs 17530  df-ps 18516  df-tsr 18517  df-plusf 18557  df-mgm 18558  df-sgrp 18607  df-mnd 18623  df-mhm 18668  df-submnd 18669  df-grp 18819  df-minusg 18820  df-sbg 18821  df-mulg 18946  df-subg 18998  df-cntz 19176  df-cmn 19645  df-abl 19646  df-mgp 19983  df-ur 20000  df-ring 20052  df-cring 20053  df-subrg 20354  df-abv 20418  df-lmod 20466  df-scaf 20467  df-sra 20778  df-rgmod 20779  df-psmet 20929  df-xmet 20930  df-met 20931  df-bl 20932  df-mopn 20933  df-fbas 20934  df-fg 20935  df-cnfld 20938  df-top 22388  df-topon 22405  df-topsp 22427  df-bases 22441  df-cld 22515  df-ntr 22516  df-cls 22517  df-nei 22594  df-lp 22632  df-perf 22633  df-cn 22723  df-cnp 22724  df-haus 22811  df-tx 23058  df-hmeo 23251  df-fil 23342  df-fm 23434  df-flim 23435  df-flf 23436  df-tmd 23568  df-tgp 23569  df-tsms 23623  df-trg 23656  df-xms 23818  df-ms 23819  df-tms 23820  df-nm 24083  df-ngp 24084  df-nrg 24086  df-nlm 24087  df-ii 24385  df-cncf 24386  df-limc 25375  df-dv 25376  df-log 26057  df-esum 33015  df-carsg 33290
This theorem is referenced by:  omsmeas  33311
  Copyright terms: Public domain W3C validator