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 33772
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 5297 . . . 4 βˆ… ∈ V
32a1i 11 . . 3 (πœ‘ β†’ βˆ… ∈ V)
4 carsggect.0 . . 3 (πœ‘ β†’ Β¬ βˆ… ∈ 𝐴)
5 padct 32379 . . 3 ((𝐴 β‰Ό Ο‰ ∧ βˆ… ∈ V ∧ Β¬ βˆ… ∈ 𝐴) β†’ βˆƒπ‘“(𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴)))
61, 3, 4, 5syl3anc 1368 . 2 (πœ‘ β†’ βˆƒπ‘“(𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴)))
7 nfv 1909 . . . . 5 Ⅎ𝑧(πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴)))
8 simpr1 1191 . . . . . . 7 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ 𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}))
98feqmptd 6950 . . . . . 6 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ 𝑓 = (π‘˜ ∈ β„• ↦ (π‘“β€˜π‘˜)))
109rneqd 5927 . . . . 5 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ ran 𝑓 = ran (π‘˜ ∈ β„• ↦ (π‘“β€˜π‘˜)))
117, 10esumeq1d 33488 . . . 4 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ Ξ£*𝑧 ∈ ran 𝑓(π‘€β€˜π‘§) = Ξ£*𝑧 ∈ ran (π‘˜ ∈ β„• ↦ (π‘“β€˜π‘˜))(π‘€β€˜π‘§))
12 fvex 6894 . . . . . . . . . 10 (toCaraSigaβ€˜π‘€) ∈ V
1312a1i 11 . . . . . . . . 9 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ (toCaraSigaβ€˜π‘€) ∈ V)
14 carsggect.2 . . . . . . . . . . 11 (πœ‘ β†’ 𝐴 βŠ† (toCaraSigaβ€˜π‘€))
1514adantr 480 . . . . . . . . . 10 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ 𝐴 βŠ† (toCaraSigaβ€˜π‘€))
16 carsgval.1 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝑂 ∈ 𝑉)
1716adantr 480 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ 𝑂 ∈ 𝑉)
18 carsgval.2 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝑀:𝒫 π‘‚βŸΆ(0[,]+∞))
1918adantr 480 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ 𝑀:𝒫 π‘‚βŸΆ(0[,]+∞))
20 carsgsiga.1 . . . . . . . . . . . . 13 (πœ‘ β†’ (π‘€β€˜βˆ…) = 0)
2120adantr 480 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ (π‘€β€˜βˆ…) = 0)
2217, 19, 210elcarsg 33761 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ βˆ… ∈ (toCaraSigaβ€˜π‘€))
2322snssd 4804 . . . . . . . . . 10 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ {βˆ…} βŠ† (toCaraSigaβ€˜π‘€))
2415, 23unssd 4178 . . . . . . . . 9 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ (𝐴 βˆͺ {βˆ…}) βŠ† (toCaraSigaβ€˜π‘€))
2513, 24ssexd 5314 . . . . . . . 8 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ (𝐴 βˆͺ {βˆ…}) ∈ V)
2619adantr 480 . . . . . . . . 9 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑧 ∈ (𝐴 βˆͺ {βˆ…})) β†’ 𝑀:𝒫 π‘‚βŸΆ(0[,]+∞))
2716, 18carsgcl 33758 . . . . . . . . . . . . 13 (πœ‘ β†’ (toCaraSigaβ€˜π‘€) βŠ† 𝒫 𝑂)
2814, 27sstrd 3984 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐴 βŠ† 𝒫 𝑂)
2928adantr 480 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ 𝐴 βŠ† 𝒫 𝑂)
30 0elpw 5344 . . . . . . . . . . . . 13 βˆ… ∈ 𝒫 𝑂
3130a1i 11 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ βˆ… ∈ 𝒫 𝑂)
3231snssd 4804 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ {βˆ…} βŠ† 𝒫 𝑂)
3329, 32unssd 4178 . . . . . . . . . 10 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ (𝐴 βˆͺ {βˆ…}) βŠ† 𝒫 𝑂)
3433sselda 3974 . . . . . . . . 9 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑧 ∈ (𝐴 βˆͺ {βˆ…})) β†’ 𝑧 ∈ 𝒫 𝑂)
3526, 34ffvelcdmd 7077 . . . . . . . 8 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑧 ∈ (𝐴 βˆͺ {βˆ…})) β†’ (π‘€β€˜π‘§) ∈ (0[,]+∞))
368frnd 6715 . . . . . . . 8 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ ran 𝑓 βŠ† (𝐴 βˆͺ {βˆ…}))
377, 25, 35, 36esummono 33507 . . . . . . 7 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ Ξ£*𝑧 ∈ ran 𝑓(π‘€β€˜π‘§) ≀ Ξ£*𝑧 ∈ (𝐴 βˆͺ {βˆ…})(π‘€β€˜π‘§))
38 ctex 8954 . . . . . . . . . 10 (𝐴 β‰Ό Ο‰ β†’ 𝐴 ∈ V)
391, 38syl 17 . . . . . . . . 9 (πœ‘ β†’ 𝐴 ∈ V)
4039adantr 480 . . . . . . . 8 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ 𝐴 ∈ V)
4113, 23ssexd 5314 . . . . . . . 8 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ {βˆ…} ∈ V)
4219adantr 480 . . . . . . . . 9 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑧 ∈ 𝐴) β†’ 𝑀:𝒫 π‘‚βŸΆ(0[,]+∞))
4329sselda 3974 . . . . . . . . 9 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑧 ∈ 𝐴) β†’ 𝑧 ∈ 𝒫 𝑂)
4442, 43ffvelcdmd 7077 . . . . . . . 8 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑧 ∈ 𝐴) β†’ (π‘€β€˜π‘§) ∈ (0[,]+∞))
45 elsni 4637 . . . . . . . . . . 11 (𝑧 ∈ {βˆ…} β†’ 𝑧 = βˆ…)
4645adantl 481 . . . . . . . . . 10 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑧 ∈ {βˆ…}) β†’ 𝑧 = βˆ…)
4746fveq2d 6885 . . . . . . . . 9 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑧 ∈ {βˆ…}) β†’ (π‘€β€˜π‘§) = (π‘€β€˜βˆ…))
4821adantr 480 . . . . . . . . 9 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑧 ∈ {βˆ…}) β†’ (π‘€β€˜βˆ…) = 0)
4947, 48eqtrd 2764 . . . . . . . 8 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑧 ∈ {βˆ…}) β†’ (π‘€β€˜π‘§) = 0)
5040, 41, 44, 49esumpad 33508 . . . . . . 7 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ Ξ£*𝑧 ∈ (𝐴 βˆͺ {βˆ…})(π‘€β€˜π‘§) = Ξ£*𝑧 ∈ 𝐴(π‘€β€˜π‘§))
5137, 50breqtrd 5164 . . . . . 6 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ Ξ£*𝑧 ∈ ran 𝑓(π‘€β€˜π‘§) ≀ Ξ£*𝑧 ∈ 𝐴(π‘€β€˜π‘§))
5236, 24sstrd 3984 . . . . . . . 8 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ ran 𝑓 βŠ† (toCaraSigaβ€˜π‘€))
53 ssexg 5313 . . . . . . . 8 ((ran 𝑓 βŠ† (toCaraSigaβ€˜π‘€) ∧ (toCaraSigaβ€˜π‘€) ∈ V) β†’ ran 𝑓 ∈ V)
5452, 12, 53sylancl 585 . . . . . . 7 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ ran 𝑓 ∈ V)
5519adantr 480 . . . . . . . 8 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑧 ∈ ran 𝑓) β†’ 𝑀:𝒫 π‘‚βŸΆ(0[,]+∞))
5636, 33sstrd 3984 . . . . . . . . 9 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ ran 𝑓 βŠ† 𝒫 𝑂)
5756sselda 3974 . . . . . . . 8 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑧 ∈ ran 𝑓) β†’ 𝑧 ∈ 𝒫 𝑂)
5855, 57ffvelcdmd 7077 . . . . . . 7 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑧 ∈ ran 𝑓) β†’ (π‘€β€˜π‘§) ∈ (0[,]+∞))
59 simpr2 1192 . . . . . . 7 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ 𝐴 βŠ† ran 𝑓)
607, 54, 58, 59esummono 33507 . . . . . 6 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ Ξ£*𝑧 ∈ 𝐴(π‘€β€˜π‘§) ≀ Ξ£*𝑧 ∈ ran 𝑓(π‘€β€˜π‘§))
6151, 60jca 511 . . . . 5 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ (Ξ£*𝑧 ∈ ran 𝑓(π‘€β€˜π‘§) ≀ Ξ£*𝑧 ∈ 𝐴(π‘€β€˜π‘§) ∧ Ξ£*𝑧 ∈ 𝐴(π‘€β€˜π‘§) ≀ Ξ£*𝑧 ∈ ran 𝑓(π‘€β€˜π‘§)))
62 iccssxr 13403 . . . . . . 7 (0[,]+∞) βŠ† ℝ*
6358ralrimiva 3138 . . . . . . . 8 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ βˆ€π‘§ ∈ ran 𝑓(π‘€β€˜π‘§) ∈ (0[,]+∞))
64 nfcv 2895 . . . . . . . . 9 Ⅎ𝑧ran 𝑓
6564esumcl 33483 . . . . . . . 8 ((ran 𝑓 ∈ V ∧ βˆ€π‘§ ∈ ran 𝑓(π‘€β€˜π‘§) ∈ (0[,]+∞)) β†’ Ξ£*𝑧 ∈ ran 𝑓(π‘€β€˜π‘§) ∈ (0[,]+∞))
6654, 63, 65syl2anc 583 . . . . . . 7 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ Ξ£*𝑧 ∈ ran 𝑓(π‘€β€˜π‘§) ∈ (0[,]+∞))
6762, 66sselid 3972 . . . . . 6 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ Ξ£*𝑧 ∈ ran 𝑓(π‘€β€˜π‘§) ∈ ℝ*)
6844ralrimiva 3138 . . . . . . . 8 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ βˆ€π‘§ ∈ 𝐴 (π‘€β€˜π‘§) ∈ (0[,]+∞))
69 nfcv 2895 . . . . . . . . 9 Ⅎ𝑧𝐴
7069esumcl 33483 . . . . . . . 8 ((𝐴 ∈ V ∧ βˆ€π‘§ ∈ 𝐴 (π‘€β€˜π‘§) ∈ (0[,]+∞)) β†’ Ξ£*𝑧 ∈ 𝐴(π‘€β€˜π‘§) ∈ (0[,]+∞))
7140, 68, 70syl2anc 583 . . . . . . 7 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ Ξ£*𝑧 ∈ 𝐴(π‘€β€˜π‘§) ∈ (0[,]+∞))
7262, 71sselid 3972 . . . . . 6 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ Ξ£*𝑧 ∈ 𝐴(π‘€β€˜π‘§) ∈ ℝ*)
73 xrletri3 13129 . . . . . 6 ((Ξ£*𝑧 ∈ ran 𝑓(π‘€β€˜π‘§) ∈ ℝ* ∧ Ξ£*𝑧 ∈ 𝐴(π‘€β€˜π‘§) ∈ ℝ*) β†’ (Ξ£*𝑧 ∈ ran 𝑓(π‘€β€˜π‘§) = Ξ£*𝑧 ∈ 𝐴(π‘€β€˜π‘§) ↔ (Ξ£*𝑧 ∈ ran 𝑓(π‘€β€˜π‘§) ≀ Ξ£*𝑧 ∈ 𝐴(π‘€β€˜π‘§) ∧ Ξ£*𝑧 ∈ 𝐴(π‘€β€˜π‘§) ≀ Ξ£*𝑧 ∈ ran 𝑓(π‘€β€˜π‘§))))
7467, 72, 73syl2anc 583 . . . . 5 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ (Ξ£*𝑧 ∈ ran 𝑓(π‘€β€˜π‘§) = Ξ£*𝑧 ∈ 𝐴(π‘€β€˜π‘§) ↔ (Ξ£*𝑧 ∈ ran 𝑓(π‘€β€˜π‘§) ≀ Ξ£*𝑧 ∈ 𝐴(π‘€β€˜π‘§) ∧ Ξ£*𝑧 ∈ 𝐴(π‘€β€˜π‘§) ≀ Ξ£*𝑧 ∈ ran 𝑓(π‘€β€˜π‘§))))
7561, 74mpbird 257 . . . 4 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ Ξ£*𝑧 ∈ ran 𝑓(π‘€β€˜π‘§) = Ξ£*𝑧 ∈ 𝐴(π‘€β€˜π‘§))
76 fveq2 6881 . . . . 5 (𝑧 = (π‘“β€˜π‘˜) β†’ (π‘€β€˜π‘§) = (π‘€β€˜(π‘“β€˜π‘˜)))
77 nnex 12214 . . . . . 6 β„• ∈ V
7877a1i 11 . . . . 5 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ β„• ∈ V)
7919adantr 480 . . . . . 6 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ π‘˜ ∈ β„•) β†’ 𝑀:𝒫 π‘‚βŸΆ(0[,]+∞))
8033adantr 480 . . . . . . 7 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ π‘˜ ∈ β„•) β†’ (𝐴 βˆͺ {βˆ…}) βŠ† 𝒫 𝑂)
818adantr 480 . . . . . . . 8 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ π‘˜ ∈ β„•) β†’ 𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}))
82 simpr 484 . . . . . . . 8 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ π‘˜ ∈ β„•) β†’ π‘˜ ∈ β„•)
8381, 82ffvelcdmd 7077 . . . . . . 7 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ π‘˜ ∈ β„•) β†’ (π‘“β€˜π‘˜) ∈ (𝐴 βˆͺ {βˆ…}))
8480, 83sseldd 3975 . . . . . 6 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ π‘˜ ∈ β„•) β†’ (π‘“β€˜π‘˜) ∈ 𝒫 𝑂)
8579, 84ffvelcdmd 7077 . . . . 5 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ π‘˜ ∈ β„•) β†’ (π‘€β€˜(π‘“β€˜π‘˜)) ∈ (0[,]+∞))
86 simpr 484 . . . . . . 7 ((((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ π‘˜ ∈ β„•) ∧ (π‘“β€˜π‘˜) = βˆ…) β†’ (π‘“β€˜π‘˜) = βˆ…)
8786fveq2d 6885 . . . . . 6 ((((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ π‘˜ ∈ β„•) ∧ (π‘“β€˜π‘˜) = βˆ…) β†’ (π‘€β€˜(π‘“β€˜π‘˜)) = (π‘€β€˜βˆ…))
8821ad2antrr 723 . . . . . 6 ((((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ π‘˜ ∈ β„•) ∧ (π‘“β€˜π‘˜) = βˆ…) β†’ (π‘€β€˜βˆ…) = 0)
8987, 88eqtrd 2764 . . . . 5 ((((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ π‘˜ ∈ β„•) ∧ (π‘“β€˜π‘˜) = βˆ…) β†’ (π‘€β€˜(π‘“β€˜π‘˜)) = 0)
90 cnvimass 6070 . . . . . . 7 (◑𝑓 β€œ 𝐴) βŠ† dom 𝑓
9190, 8fssdm 6727 . . . . . 6 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ (◑𝑓 β€œ 𝐴) βŠ† β„•)
92 ffun 6710 . . . . . . . . . . 11 (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) β†’ Fun 𝑓)
938, 92syl 17 . . . . . . . . . 10 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ Fun 𝑓)
9493adantr 480 . . . . . . . . 9 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ π‘˜ ∈ (β„• βˆ– (◑𝑓 β€œ 𝐴))) β†’ Fun 𝑓)
95 difpreima 7056 . . . . . . . . . . . . 13 (Fun 𝑓 β†’ (◑𝑓 β€œ ((𝐴 βˆͺ {βˆ…}) βˆ– 𝐴)) = ((◑𝑓 β€œ (𝐴 βˆͺ {βˆ…})) βˆ– (◑𝑓 β€œ 𝐴)))
968, 92, 953syl 18 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ (◑𝑓 β€œ ((𝐴 βˆͺ {βˆ…}) βˆ– 𝐴)) = ((◑𝑓 β€œ (𝐴 βˆͺ {βˆ…})) βˆ– (◑𝑓 β€œ 𝐴)))
97 fimacnv 6729 . . . . . . . . . . . . . 14 (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) β†’ (◑𝑓 β€œ (𝐴 βˆͺ {βˆ…})) = β„•)
988, 97syl 17 . . . . . . . . . . . . 13 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ (◑𝑓 β€œ (𝐴 βˆͺ {βˆ…})) = β„•)
9998difeq1d 4113 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ ((◑𝑓 β€œ (𝐴 βˆͺ {βˆ…})) βˆ– (◑𝑓 β€œ 𝐴)) = (β„• βˆ– (◑𝑓 β€œ 𝐴)))
10096, 99eqtrd 2764 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ (◑𝑓 β€œ ((𝐴 βˆͺ {βˆ…}) βˆ– 𝐴)) = (β„• βˆ– (◑𝑓 β€œ 𝐴)))
101 uncom 4145 . . . . . . . . . . . . . . . 16 ({βˆ…} βˆͺ 𝐴) = (𝐴 βˆͺ {βˆ…})
102101difeq1i 4110 . . . . . . . . . . . . . . 15 (({βˆ…} βˆͺ 𝐴) βˆ– 𝐴) = ((𝐴 βˆͺ {βˆ…}) βˆ– 𝐴)
103 difun2 4472 . . . . . . . . . . . . . . 15 (({βˆ…} βˆͺ 𝐴) βˆ– 𝐴) = ({βˆ…} βˆ– 𝐴)
104102, 103eqtr3i 2754 . . . . . . . . . . . . . 14 ((𝐴 βˆͺ {βˆ…}) βˆ– 𝐴) = ({βˆ…} βˆ– 𝐴)
105 difss 4123 . . . . . . . . . . . . . 14 ({βˆ…} βˆ– 𝐴) βŠ† {βˆ…}
106104, 105eqsstri 4008 . . . . . . . . . . . . 13 ((𝐴 βˆͺ {βˆ…}) βˆ– 𝐴) βŠ† {βˆ…}
107106a1i 11 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ ((𝐴 βˆͺ {βˆ…}) βˆ– 𝐴) βŠ† {βˆ…})
108 sspreima 7059 . . . . . . . . . . . 12 ((Fun 𝑓 ∧ ((𝐴 βˆͺ {βˆ…}) βˆ– 𝐴) βŠ† {βˆ…}) β†’ (◑𝑓 β€œ ((𝐴 βˆͺ {βˆ…}) βˆ– 𝐴)) βŠ† (◑𝑓 β€œ {βˆ…}))
10993, 107, 108syl2anc 583 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ (◑𝑓 β€œ ((𝐴 βˆͺ {βˆ…}) βˆ– 𝐴)) βŠ† (◑𝑓 β€œ {βˆ…}))
110100, 109eqsstrrd 4013 . . . . . . . . . 10 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ (β„• βˆ– (◑𝑓 β€œ 𝐴)) βŠ† (◑𝑓 β€œ {βˆ…}))
111110sselda 3974 . . . . . . . . 9 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ π‘˜ ∈ (β„• βˆ– (◑𝑓 β€œ 𝐴))) β†’ π‘˜ ∈ (◑𝑓 β€œ {βˆ…}))
112 fvimacnvi 7043 . . . . . . . . 9 ((Fun 𝑓 ∧ π‘˜ ∈ (◑𝑓 β€œ {βˆ…})) β†’ (π‘“β€˜π‘˜) ∈ {βˆ…})
11394, 111, 112syl2anc 583 . . . . . . . 8 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ π‘˜ ∈ (β„• βˆ– (◑𝑓 β€œ 𝐴))) β†’ (π‘“β€˜π‘˜) ∈ {βˆ…})
114 elsni 4637 . . . . . . . 8 ((π‘“β€˜π‘˜) ∈ {βˆ…} β†’ (π‘“β€˜π‘˜) = βˆ…)
115113, 114syl 17 . . . . . . 7 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ π‘˜ ∈ (β„• βˆ– (◑𝑓 β€œ 𝐴))) β†’ (π‘“β€˜π‘˜) = βˆ…)
116115ralrimiva 3138 . . . . . 6 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ βˆ€π‘˜ ∈ (β„• βˆ– (◑𝑓 β€œ 𝐴))(π‘“β€˜π‘˜) = βˆ…)
117 carsggect.3 . . . . . . . 8 (πœ‘ β†’ Disj 𝑦 ∈ 𝐴 𝑦)
118117adantr 480 . . . . . . 7 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ Disj 𝑦 ∈ 𝐴 𝑦)
119 simpr3 1193 . . . . . . . . . 10 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ Fun (◑𝑓 β†Ύ 𝐴))
120 fresf1o 32290 . . . . . . . . . 10 ((Fun 𝑓 ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴)) β†’ (𝑓 β†Ύ (◑𝑓 β€œ 𝐴)):(◑𝑓 β€œ 𝐴)–1-1-onto→𝐴)
12193, 59, 119, 120syl3anc 1368 . . . . . . . . 9 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ (𝑓 β†Ύ (◑𝑓 β€œ 𝐴)):(◑𝑓 β€œ 𝐴)–1-1-onto→𝐴)
122 simpr 484 . . . . . . . . 9 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑦 = ((𝑓 β†Ύ (◑𝑓 β€œ 𝐴))β€˜π‘˜)) β†’ 𝑦 = ((𝑓 β†Ύ (◑𝑓 β€œ 𝐴))β€˜π‘˜))
123121, 122disjrdx 32257 . . . . . . . 8 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ (Disj π‘˜ ∈ (◑𝑓 β€œ 𝐴)((𝑓 β†Ύ (◑𝑓 β€œ 𝐴))β€˜π‘˜) ↔ Disj 𝑦 ∈ 𝐴 𝑦))
124 fvres 6900 . . . . . . . . . 10 (π‘˜ ∈ (◑𝑓 β€œ 𝐴) β†’ ((𝑓 β†Ύ (◑𝑓 β€œ 𝐴))β€˜π‘˜) = (π‘“β€˜π‘˜))
125124adantl 481 . . . . . . . . 9 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ π‘˜ ∈ (◑𝑓 β€œ 𝐴)) β†’ ((𝑓 β†Ύ (◑𝑓 β€œ 𝐴))β€˜π‘˜) = (π‘“β€˜π‘˜))
126125disjeq2dv 5108 . . . . . . . 8 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ (Disj π‘˜ ∈ (◑𝑓 β€œ 𝐴)((𝑓 β†Ύ (◑𝑓 β€œ 𝐴))β€˜π‘˜) ↔ Disj π‘˜ ∈ (◑𝑓 β€œ 𝐴)(π‘“β€˜π‘˜)))
127123, 126bitr3d 281 . . . . . . 7 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ (Disj 𝑦 ∈ 𝐴 𝑦 ↔ Disj π‘˜ ∈ (◑𝑓 β€œ 𝐴)(π‘“β€˜π‘˜)))
128118, 127mpbid 231 . . . . . 6 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ Disj π‘˜ ∈ (◑𝑓 β€œ 𝐴)(π‘“β€˜π‘˜))
129 disjss3 5137 . . . . . . 7 (((◑𝑓 β€œ 𝐴) βŠ† β„• ∧ βˆ€π‘˜ ∈ (β„• βˆ– (◑𝑓 β€œ 𝐴))(π‘“β€˜π‘˜) = βˆ…) β†’ (Disj π‘˜ ∈ (◑𝑓 β€œ 𝐴)(π‘“β€˜π‘˜) ↔ Disj π‘˜ ∈ β„• (π‘“β€˜π‘˜)))
130129biimpa 476 . . . . . 6 ((((◑𝑓 β€œ 𝐴) βŠ† β„• ∧ βˆ€π‘˜ ∈ (β„• βˆ– (◑𝑓 β€œ 𝐴))(π‘“β€˜π‘˜) = βˆ…) ∧ Disj π‘˜ ∈ (◑𝑓 β€œ 𝐴)(π‘“β€˜π‘˜)) β†’ Disj π‘˜ ∈ β„• (π‘“β€˜π‘˜))
13191, 116, 128, 130syl21anc 835 . . . . 5 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ Disj π‘˜ ∈ β„• (π‘“β€˜π‘˜))
13276, 78, 85, 84, 89, 131esumrnmpt2 33521 . . . 4 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ Ξ£*𝑧 ∈ ran (π‘˜ ∈ β„• ↦ (π‘“β€˜π‘˜))(π‘€β€˜π‘§) = Ξ£*π‘˜ ∈ β„•(π‘€β€˜(π‘“β€˜π‘˜)))
13311, 75, 1323eqtr3rd 2773 . . 3 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ Ξ£*π‘˜ ∈ β„•(π‘€β€˜(π‘“β€˜π‘˜)) = Ξ£*𝑧 ∈ 𝐴(π‘€β€˜π‘§))
134 uniiun 5051 . . . . . . 7 βˆͺ 𝐴 = βˆͺ π‘₯ ∈ 𝐴 π‘₯
13528sselda 3974 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ 𝐴) β†’ π‘₯ ∈ 𝒫 𝑂)
13639, 135elpwiuncl 32200 . . . . . . 7 (πœ‘ β†’ βˆͺ π‘₯ ∈ 𝐴 π‘₯ ∈ 𝒫 𝑂)
137134, 136eqeltrid 2829 . . . . . 6 (πœ‘ β†’ βˆͺ 𝐴 ∈ 𝒫 𝑂)
138137adantr 480 . . . . 5 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ βˆͺ 𝐴 ∈ 𝒫 𝑂)
13919, 138ffvelcdmd 7077 . . . 4 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ (π‘€β€˜βˆͺ 𝐴) ∈ (0[,]+∞))
140 carsgsiga.2 . . . . . . . . . 10 ((πœ‘ ∧ π‘₯ β‰Ό Ο‰ ∧ π‘₯ βŠ† 𝒫 𝑂) β†’ (π‘€β€˜βˆͺ π‘₯) ≀ Ξ£*𝑦 ∈ π‘₯(π‘€β€˜π‘¦))
1411403adant1r 1174 . . . . . . . . 9 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ π‘₯ β‰Ό Ο‰ ∧ π‘₯ βŠ† 𝒫 𝑂) β†’ (π‘€β€˜βˆͺ π‘₯) ≀ Ξ£*𝑦 ∈ π‘₯(π‘€β€˜π‘¦))
142 fveq2 6881 . . . . . . . . . 10 (𝑦 = 𝑧 β†’ (π‘€β€˜π‘¦) = (π‘€β€˜π‘§))
143 nfcv 2895 . . . . . . . . . 10 Ⅎ𝑧π‘₯
144 nfcv 2895 . . . . . . . . . 10 Ⅎ𝑦π‘₯
145 nfcv 2895 . . . . . . . . . 10 Ⅎ𝑧(π‘€β€˜π‘¦)
146 nfcv 2895 . . . . . . . . . 10 Ⅎ𝑦(π‘€β€˜π‘§)
147142, 143, 144, 145, 146cbvesum 33495 . . . . . . . . 9 Ξ£*𝑦 ∈ π‘₯(π‘€β€˜π‘¦) = Ξ£*𝑧 ∈ π‘₯(π‘€β€˜π‘§)
148141, 147breqtrdi 5179 . . . . . . . 8 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ π‘₯ β‰Ό Ο‰ ∧ π‘₯ βŠ† 𝒫 𝑂) β†’ (π‘€β€˜βˆͺ π‘₯) ≀ Ξ£*𝑧 ∈ π‘₯(π‘€β€˜π‘§))
149 ffn 6707 . . . . . . . . . 10 (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) β†’ 𝑓 Fn β„•)
150 fz1ssnn 13528 . . . . . . . . . . 11 (1...𝑛) βŠ† β„•
151 fnssres 6663 . . . . . . . . . . 11 ((𝑓 Fn β„• ∧ (1...𝑛) βŠ† β„•) β†’ (𝑓 β†Ύ (1...𝑛)) Fn (1...𝑛))
152150, 151mpan2 688 . . . . . . . . . 10 (𝑓 Fn β„• β†’ (𝑓 β†Ύ (1...𝑛)) Fn (1...𝑛))
1538, 149, 1523syl 18 . . . . . . . . 9 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ (𝑓 β†Ύ (1...𝑛)) Fn (1...𝑛))
154 fzfi 13933 . . . . . . . . . 10 (1...𝑛) ∈ Fin
155 fnfi 9176 . . . . . . . . . 10 (((𝑓 β†Ύ (1...𝑛)) Fn (1...𝑛) ∧ (1...𝑛) ∈ Fin) β†’ (𝑓 β†Ύ (1...𝑛)) ∈ Fin)
156154, 155mpan2 688 . . . . . . . . 9 ((𝑓 β†Ύ (1...𝑛)) Fn (1...𝑛) β†’ (𝑓 β†Ύ (1...𝑛)) ∈ Fin)
157 rnfi 9330 . . . . . . . . 9 ((𝑓 β†Ύ (1...𝑛)) ∈ Fin β†’ ran (𝑓 β†Ύ (1...𝑛)) ∈ Fin)
158153, 156, 1573syl 18 . . . . . . . 8 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ ran (𝑓 β†Ύ (1...𝑛)) ∈ Fin)
159 resss 5996 . . . . . . . . . . 11 (𝑓 β†Ύ (1...𝑛)) βŠ† 𝑓
160 rnss 5928 . . . . . . . . . . 11 ((𝑓 β†Ύ (1...𝑛)) βŠ† 𝑓 β†’ ran (𝑓 β†Ύ (1...𝑛)) βŠ† ran 𝑓)
161159, 160ax-mp 5 . . . . . . . . . 10 ran (𝑓 β†Ύ (1...𝑛)) βŠ† ran 𝑓
162161a1i 11 . . . . . . . . 9 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ ran (𝑓 β†Ύ (1...𝑛)) βŠ† ran 𝑓)
163162, 52sstrd 3984 . . . . . . . 8 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ ran (𝑓 β†Ύ (1...𝑛)) βŠ† (toCaraSigaβ€˜π‘€))
164162, 36sstrd 3984 . . . . . . . . 9 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ ran (𝑓 β†Ύ (1...𝑛)) βŠ† (𝐴 βˆͺ {βˆ…}))
165 nfcv 2895 . . . . . . . . . . . . 13 Ⅎ𝑧𝑦
166 nfcv 2895 . . . . . . . . . . . . 13 Ⅎ𝑦𝑧
167 id 22 . . . . . . . . . . . . 13 (𝑦 = 𝑧 β†’ 𝑦 = 𝑧)
168165, 166, 167cbvdisj 5113 . . . . . . . . . . . 12 (Disj 𝑦 ∈ 𝐴 𝑦 ↔ Disj 𝑧 ∈ 𝐴 𝑧)
169 disjun0 32261 . . . . . . . . . . . 12 (Disj 𝑧 ∈ 𝐴 𝑧 β†’ Disj 𝑧 ∈ (𝐴 βˆͺ {βˆ…})𝑧)
170168, 169sylbi 216 . . . . . . . . . . 11 (Disj 𝑦 ∈ 𝐴 𝑦 β†’ Disj 𝑧 ∈ (𝐴 βˆͺ {βˆ…})𝑧)
171117, 170syl 17 . . . . . . . . . 10 (πœ‘ β†’ Disj 𝑧 ∈ (𝐴 βˆͺ {βˆ…})𝑧)
172171adantr 480 . . . . . . . . 9 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ Disj 𝑧 ∈ (𝐴 βˆͺ {βˆ…})𝑧)
173 disjss1 5109 . . . . . . . . 9 (ran (𝑓 β†Ύ (1...𝑛)) βŠ† (𝐴 βˆͺ {βˆ…}) β†’ (Disj 𝑧 ∈ (𝐴 βˆͺ {βˆ…})𝑧 β†’ Disj 𝑧 ∈ ran (𝑓 β†Ύ (1...𝑛))𝑧))
174164, 172, 173sylc 65 . . . . . . . 8 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ Disj 𝑧 ∈ ran (𝑓 β†Ύ (1...𝑛))𝑧)
175 pwidg 4614 . . . . . . . . 9 (𝑂 ∈ 𝑉 β†’ 𝑂 ∈ 𝒫 𝑂)
17617, 175syl 17 . . . . . . . 8 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ 𝑂 ∈ 𝒫 𝑂)
17717, 19, 21, 148, 158, 163, 174, 176carsgclctunlem1 33771 . . . . . . 7 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ (π‘€β€˜(𝑂 ∩ βˆͺ ran (𝑓 β†Ύ (1...𝑛)))) = Ξ£*𝑧 ∈ ran (𝑓 β†Ύ (1...𝑛))(π‘€β€˜(𝑂 ∩ 𝑧)))
178177adantr 480 . . . . . 6 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•) β†’ (π‘€β€˜(𝑂 ∩ βˆͺ ran (𝑓 β†Ύ (1...𝑛)))) = Ξ£*𝑧 ∈ ran (𝑓 β†Ύ (1...𝑛))(π‘€β€˜(𝑂 ∩ 𝑧)))
179164unissd 4909 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ βˆͺ ran (𝑓 β†Ύ (1...𝑛)) βŠ† βˆͺ (𝐴 βˆͺ {βˆ…}))
180 uniun 4924 . . . . . . . . . . . 12 βˆͺ (𝐴 βˆͺ {βˆ…}) = (βˆͺ 𝐴 βˆͺ βˆͺ {βˆ…})
1812unisn 4920 . . . . . . . . . . . . 13 βˆͺ {βˆ…} = βˆ…
182181uneq2i 4152 . . . . . . . . . . . 12 (βˆͺ 𝐴 βˆͺ βˆͺ {βˆ…}) = (βˆͺ 𝐴 βˆͺ βˆ…)
183 un0 4382 . . . . . . . . . . . 12 (βˆͺ 𝐴 βˆͺ βˆ…) = βˆͺ 𝐴
184180, 182, 1833eqtri 2756 . . . . . . . . . . 11 βˆͺ (𝐴 βˆͺ {βˆ…}) = βˆͺ 𝐴
185179, 184sseqtrdi 4024 . . . . . . . . . 10 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ βˆͺ ran (𝑓 β†Ύ (1...𝑛)) βŠ† βˆͺ 𝐴)
186185adantr 480 . . . . . . . . 9 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•) β†’ βˆͺ ran (𝑓 β†Ύ (1...𝑛)) βŠ† βˆͺ 𝐴)
187 uniss 4907 . . . . . . . . . . . 12 (𝐴 βŠ† 𝒫 𝑂 β†’ βˆͺ 𝐴 βŠ† βˆͺ 𝒫 𝑂)
188 unipw 5440 . . . . . . . . . . . 12 βˆͺ 𝒫 𝑂 = 𝑂
189187, 188sseqtrdi 4024 . . . . . . . . . . 11 (𝐴 βŠ† 𝒫 𝑂 β†’ βˆͺ 𝐴 βŠ† 𝑂)
19028, 189syl 17 . . . . . . . . . 10 (πœ‘ β†’ βˆͺ 𝐴 βŠ† 𝑂)
191190ad2antrr 723 . . . . . . . . 9 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•) β†’ βˆͺ 𝐴 βŠ† 𝑂)
192186, 191sstrd 3984 . . . . . . . 8 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•) β†’ βˆͺ ran (𝑓 β†Ύ (1...𝑛)) βŠ† 𝑂)
193 sseqin2 4207 . . . . . . . 8 (βˆͺ ran (𝑓 β†Ύ (1...𝑛)) βŠ† 𝑂 ↔ (𝑂 ∩ βˆͺ ran (𝑓 β†Ύ (1...𝑛))) = βˆͺ ran (𝑓 β†Ύ (1...𝑛)))
194192, 193sylib 217 . . . . . . 7 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•) β†’ (𝑂 ∩ βˆͺ ran (𝑓 β†Ύ (1...𝑛))) = βˆͺ ran (𝑓 β†Ύ (1...𝑛)))
195194fveq2d 6885 . . . . . 6 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•) β†’ (π‘€β€˜(𝑂 ∩ βˆͺ ran (𝑓 β†Ύ (1...𝑛)))) = (π‘€β€˜βˆͺ ran (𝑓 β†Ύ (1...𝑛))))
196 nfv 1909 . . . . . . . 8 Ⅎ𝑧((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•)
197164adantr 480 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•) β†’ ran (𝑓 β†Ύ (1...𝑛)) βŠ† (𝐴 βˆͺ {βˆ…}))
19828ad2antrr 723 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•) β†’ 𝐴 βŠ† 𝒫 𝑂)
19930a1i 11 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•) β†’ βˆ… ∈ 𝒫 𝑂)
200199snssd 4804 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•) β†’ {βˆ…} βŠ† 𝒫 𝑂)
201198, 200unssd 4178 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•) β†’ (𝐴 βˆͺ {βˆ…}) βŠ† 𝒫 𝑂)
202197, 201sstrd 3984 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•) β†’ ran (𝑓 β†Ύ (1...𝑛)) βŠ† 𝒫 𝑂)
203202sselda 3974 . . . . . . . . . . . 12 ((((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•) ∧ 𝑧 ∈ ran (𝑓 β†Ύ (1...𝑛))) β†’ 𝑧 ∈ 𝒫 𝑂)
204203elpwid 4603 . . . . . . . . . . 11 ((((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•) ∧ 𝑧 ∈ ran (𝑓 β†Ύ (1...𝑛))) β†’ 𝑧 βŠ† 𝑂)
205 sseqin2 4207 . . . . . . . . . . 11 (𝑧 βŠ† 𝑂 ↔ (𝑂 ∩ 𝑧) = 𝑧)
206204, 205sylib 217 . . . . . . . . . 10 ((((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•) ∧ 𝑧 ∈ ran (𝑓 β†Ύ (1...𝑛))) β†’ (𝑂 ∩ 𝑧) = 𝑧)
207206fveq2d 6885 . . . . . . . . 9 ((((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•) ∧ 𝑧 ∈ ran (𝑓 β†Ύ (1...𝑛))) β†’ (π‘€β€˜(𝑂 ∩ 𝑧)) = (π‘€β€˜π‘§))
208207ralrimiva 3138 . . . . . . . 8 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•) β†’ βˆ€π‘§ ∈ ran (𝑓 β†Ύ (1...𝑛))(π‘€β€˜(𝑂 ∩ 𝑧)) = (π‘€β€˜π‘§))
209196, 208esumeq2d 33490 . . . . . . 7 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•) β†’ Ξ£*𝑧 ∈ ran (𝑓 β†Ύ (1...𝑛))(π‘€β€˜(𝑂 ∩ 𝑧)) = Ξ£*𝑧 ∈ ran (𝑓 β†Ύ (1...𝑛))(π‘€β€˜π‘§))
2109reseq1d 5970 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ (𝑓 β†Ύ (1...𝑛)) = ((π‘˜ ∈ β„• ↦ (π‘“β€˜π‘˜)) β†Ύ (1...𝑛)))
211210adantr 480 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•) β†’ (𝑓 β†Ύ (1...𝑛)) = ((π‘˜ ∈ β„• ↦ (π‘“β€˜π‘˜)) β†Ύ (1...𝑛)))
212 resmpt 6027 . . . . . . . . . . . 12 ((1...𝑛) βŠ† β„• β†’ ((π‘˜ ∈ β„• ↦ (π‘“β€˜π‘˜)) β†Ύ (1...𝑛)) = (π‘˜ ∈ (1...𝑛) ↦ (π‘“β€˜π‘˜)))
213150, 212ax-mp 5 . . . . . . . . . . 11 ((π‘˜ ∈ β„• ↦ (π‘“β€˜π‘˜)) β†Ύ (1...𝑛)) = (π‘˜ ∈ (1...𝑛) ↦ (π‘“β€˜π‘˜))
214211, 213eqtrdi 2780 . . . . . . . . . 10 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•) β†’ (𝑓 β†Ύ (1...𝑛)) = (π‘˜ ∈ (1...𝑛) ↦ (π‘“β€˜π‘˜)))
215214eqcomd 2730 . . . . . . . . 9 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•) β†’ (π‘˜ ∈ (1...𝑛) ↦ (π‘“β€˜π‘˜)) = (𝑓 β†Ύ (1...𝑛)))
216215rneqd 5927 . . . . . . . 8 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•) β†’ ran (π‘˜ ∈ (1...𝑛) ↦ (π‘“β€˜π‘˜)) = ran (𝑓 β†Ύ (1...𝑛)))
217196, 216esumeq1d 33488 . . . . . . 7 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•) β†’ Ξ£*𝑧 ∈ ran (π‘˜ ∈ (1...𝑛) ↦ (π‘“β€˜π‘˜))(π‘€β€˜π‘§) = Ξ£*𝑧 ∈ ran (𝑓 β†Ύ (1...𝑛))(π‘€β€˜π‘§))
218154a1i 11 . . . . . . . 8 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•) β†’ (1...𝑛) ∈ Fin)
21919ad2antrr 723 . . . . . . . . 9 ((((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ 𝑀:𝒫 π‘‚βŸΆ(0[,]+∞))
220150a1i 11 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•) β†’ (1...𝑛) βŠ† β„•)
221220sselda 3974 . . . . . . . . . 10 ((((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ π‘˜ ∈ β„•)
22284adantlr 712 . . . . . . . . . 10 ((((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ β„•) β†’ (π‘“β€˜π‘˜) ∈ 𝒫 𝑂)
223221, 222syldan 590 . . . . . . . . 9 ((((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (π‘“β€˜π‘˜) ∈ 𝒫 𝑂)
224219, 223ffvelcdmd 7077 . . . . . . . 8 ((((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (π‘€β€˜(π‘“β€˜π‘˜)) ∈ (0[,]+∞))
225 simpr 484 . . . . . . . . . 10 (((((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) ∧ (π‘“β€˜π‘˜) = βˆ…) β†’ (π‘“β€˜π‘˜) = βˆ…)
226225fveq2d 6885 . . . . . . . . 9 (((((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) ∧ (π‘“β€˜π‘˜) = βˆ…) β†’ (π‘€β€˜(π‘“β€˜π‘˜)) = (π‘€β€˜βˆ…))
22721ad3antrrr 727 . . . . . . . . 9 (((((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) ∧ (π‘“β€˜π‘˜) = βˆ…) β†’ (π‘€β€˜βˆ…) = 0)
228226, 227eqtrd 2764 . . . . . . . 8 (((((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) ∧ (π‘“β€˜π‘˜) = βˆ…) β†’ (π‘€β€˜(π‘“β€˜π‘˜)) = 0)
229 disjss1 5109 . . . . . . . . . . 11 ((1...𝑛) βŠ† β„• β†’ (Disj π‘˜ ∈ β„• (π‘“β€˜π‘˜) β†’ Disj π‘˜ ∈ (1...𝑛)(π‘“β€˜π‘˜)))
230150, 229ax-mp 5 . . . . . . . . . 10 (Disj π‘˜ ∈ β„• (π‘“β€˜π‘˜) β†’ Disj π‘˜ ∈ (1...𝑛)(π‘“β€˜π‘˜))
231131, 230syl 17 . . . . . . . . 9 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ Disj π‘˜ ∈ (1...𝑛)(π‘“β€˜π‘˜))
232231adantr 480 . . . . . . . 8 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•) β†’ Disj π‘˜ ∈ (1...𝑛)(π‘“β€˜π‘˜))
23376, 218, 224, 223, 228, 232esumrnmpt2 33521 . . . . . . 7 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•) β†’ Ξ£*𝑧 ∈ ran (π‘˜ ∈ (1...𝑛) ↦ (π‘“β€˜π‘˜))(π‘€β€˜π‘§) = Ξ£*π‘˜ ∈ (1...𝑛)(π‘€β€˜(π‘“β€˜π‘˜)))
234209, 217, 2333eqtr2d 2770 . . . . . 6 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•) β†’ Ξ£*𝑧 ∈ ran (𝑓 β†Ύ (1...𝑛))(π‘€β€˜(𝑂 ∩ 𝑧)) = Ξ£*π‘˜ ∈ (1...𝑛)(π‘€β€˜(π‘“β€˜π‘˜)))
235178, 195, 2343eqtr3d 2772 . . . . 5 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•) β†’ (π‘€β€˜βˆͺ ran (𝑓 β†Ύ (1...𝑛))) = Ξ£*π‘˜ ∈ (1...𝑛)(π‘€β€˜(π‘“β€˜π‘˜)))
236 carsggect.4 . . . . . . . 8 ((πœ‘ ∧ π‘₯ βŠ† 𝑦 ∧ 𝑦 ∈ 𝒫 𝑂) β†’ (π‘€β€˜π‘₯) ≀ (π‘€β€˜π‘¦))
2372363adant1r 1174 . . . . . . 7 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ π‘₯ βŠ† 𝑦 ∧ 𝑦 ∈ 𝒫 𝑂) β†’ (π‘€β€˜π‘₯) ≀ (π‘€β€˜π‘¦))
23817, 19, 185, 138, 237carsgmon 33768 . . . . . 6 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ (π‘€β€˜βˆͺ ran (𝑓 β†Ύ (1...𝑛))) ≀ (π‘€β€˜βˆͺ 𝐴))
239238adantr 480 . . . . 5 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•) β†’ (π‘€β€˜βˆͺ ran (𝑓 β†Ύ (1...𝑛))) ≀ (π‘€β€˜βˆͺ 𝐴))
240235, 239eqbrtrrd 5162 . . . 4 (((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) ∧ 𝑛 ∈ β„•) β†’ Ξ£*π‘˜ ∈ (1...𝑛)(π‘€β€˜(π‘“β€˜π‘˜)) ≀ (π‘€β€˜βˆͺ 𝐴))
241139, 85, 240esumgect 33543 . . 3 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ Ξ£*π‘˜ ∈ β„•(π‘€β€˜(π‘“β€˜π‘˜)) ≀ (π‘€β€˜βˆͺ 𝐴))
242133, 241eqbrtrrd 5162 . 2 ((πœ‘ ∧ (𝑓:β„•βŸΆ(𝐴 βˆͺ {βˆ…}) ∧ 𝐴 βŠ† ran 𝑓 ∧ Fun (◑𝑓 β†Ύ 𝐴))) β†’ Ξ£*𝑧 ∈ 𝐴(π‘€β€˜π‘§) ≀ (π‘€β€˜βˆͺ 𝐴))
2436, 242exlimddv 1930 1 (πœ‘ β†’ Ξ£*𝑧 ∈ 𝐴(π‘€β€˜π‘§) ≀ (π‘€β€˜βˆͺ 𝐴))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1084   = wceq 1533  βˆƒwex 1773   ∈ wcel 2098  βˆ€wral 3053  Vcvv 3466   βˆ– cdif 3937   βˆͺ cun 3938   ∩ cin 3939   βŠ† wss 3940  βˆ…c0 4314  π’« cpw 4594  {csn 4620  βˆͺ cuni 4899  βˆͺ ciun 4987  Disj wdisj 5103   class class class wbr 5138   ↦ cmpt 5221  β—‘ccnv 5665  ran crn 5667   β†Ύ cres 5668   β€œ cima 5669  Fun wfun 6527   Fn wfn 6528  βŸΆwf 6529  β€“1-1-ontoβ†’wf1o 6532  β€˜cfv 6533  (class class class)co 7401  Ο‰com 7848   β‰Ό cdom 8932  Fincfn 8934  0cc0 11105  1c1 11106  +∞cpnf 11241  β„*cxr 11243   ≀ cle 11245  β„•cn 12208  [,]cicc 13323  ...cfz 13480  Ξ£*cesum 33480  toCaraSigaccarsg 33755
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5275  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417  ax-un 7718  ax-inf2 9631  ax-cnex 11161  ax-resscn 11162  ax-1cn 11163  ax-icn 11164  ax-addcl 11165  ax-addrcl 11166  ax-mulcl 11167  ax-mulrcl 11168  ax-mulcom 11169  ax-addass 11170  ax-mulass 11171  ax-distr 11172  ax-i2m1 11173  ax-1ne0 11174  ax-1rid 11175  ax-rnegex 11176  ax-rrecex 11177  ax-cnre 11178  ax-pre-lttri 11179  ax-pre-lttrn 11180  ax-pre-ltadd 11181  ax-pre-mulgt0 11182  ax-pre-sup 11183  ax-addf 11184  ax-mulf 11185
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-nel 3039  df-ral 3054  df-rex 3063  df-rmo 3368  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3959  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-tp 4625  df-op 4627  df-uni 4900  df-int 4941  df-iun 4989  df-iin 4990  df-disj 5104  df-br 5139  df-opab 5201  df-mpt 5222  df-tr 5256  df-id 5564  df-eprel 5570  df-po 5578  df-so 5579  df-fr 5621  df-se 5622  df-we 5623  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6290  df-ord 6357  df-on 6358  df-lim 6359  df-suc 6360  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-isom 6542  df-riota 7357  df-ov 7404  df-oprab 7405  df-mpo 7406  df-of 7663  df-om 7849  df-1st 7968  df-2nd 7969  df-supp 8141  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-rdg 8405  df-1o 8461  df-2o 8462  df-er 8698  df-map 8817  df-pm 8818  df-ixp 8887  df-en 8935  df-dom 8936  df-sdom 8937  df-fin 8938  df-fsupp 9357  df-fi 9401  df-sup 9432  df-inf 9433  df-oi 9500  df-dju 9891  df-card 9929  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-div 11868  df-nn 12209  df-2 12271  df-3 12272  df-4 12273  df-5 12274  df-6 12275  df-7 12276  df-8 12277  df-9 12278  df-n0 12469  df-z 12555  df-dec 12674  df-uz 12819  df-q 12929  df-rp 12971  df-xneg 13088  df-xadd 13089  df-xmul 13090  df-ioo 13324  df-ioc 13325  df-ico 13326  df-icc 13327  df-fz 13481  df-fzo 13624  df-fl 13753  df-mod 13831  df-seq 13963  df-exp 14024  df-fac 14230  df-bc 14259  df-hash 14287  df-shft 15010  df-cj 15042  df-re 15043  df-im 15044  df-sqrt 15178  df-abs 15179  df-limsup 15411  df-clim 15428  df-rlim 15429  df-sum 15629  df-ef 16007  df-sin 16009  df-cos 16010  df-pi 16012  df-struct 17078  df-sets 17095  df-slot 17113  df-ndx 17125  df-base 17143  df-ress 17172  df-plusg 17208  df-mulr 17209  df-starv 17210  df-sca 17211  df-vsca 17212  df-ip 17213  df-tset 17214  df-ple 17215  df-ds 17217  df-unif 17218  df-hom 17219  df-cco 17220  df-rest 17366  df-topn 17367  df-0g 17385  df-gsum 17386  df-topgen 17387  df-pt 17388  df-prds 17391  df-ordt 17445  df-xrs 17446  df-qtop 17451  df-imas 17452  df-xps 17454  df-mre 17528  df-mrc 17529  df-acs 17531  df-ps 18520  df-tsr 18521  df-plusf 18561  df-mgm 18562  df-sgrp 18641  df-mnd 18657  df-mhm 18702  df-submnd 18703  df-grp 18855  df-minusg 18856  df-sbg 18857  df-mulg 18985  df-subg 19039  df-cntz 19222  df-cmn 19691  df-abl 19692  df-mgp 20029  df-rng 20047  df-ur 20076  df-ring 20129  df-cring 20130  df-subrng 20435  df-subrg 20460  df-abv 20649  df-lmod 20697  df-scaf 20698  df-sra 21010  df-rgmod 21011  df-psmet 21219  df-xmet 21220  df-met 21221  df-bl 21222  df-mopn 21223  df-fbas 21224  df-fg 21225  df-cnfld 21228  df-top 22717  df-topon 22734  df-topsp 22756  df-bases 22770  df-cld 22844  df-ntr 22845  df-cls 22846  df-nei 22923  df-lp 22961  df-perf 22962  df-cn 23052  df-cnp 23053  df-haus 23140  df-tx 23387  df-hmeo 23580  df-fil 23671  df-fm 23763  df-flim 23764  df-flf 23765  df-tmd 23897  df-tgp 23898  df-tsms 23952  df-trg 23985  df-xms 24147  df-ms 24148  df-tms 24149  df-nm 24412  df-ngp 24413  df-nrg 24415  df-nlm 24416  df-ii 24718  df-cncf 24719  df-limc 25716  df-dv 25717  df-log 26406  df-esum 33481  df-carsg 33756
This theorem is referenced by:  omsmeas  33777
  Copyright terms: Public domain W3C validator