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 32391
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 5246 . . . 4 ∅ ∈ V
32a1i 11 . . 3 (𝜑 → ∅ ∈ V)
4 carsggect.0 . . 3 (𝜑 → ¬ ∅ ∈ 𝐴)
5 padct 31162 . . 3 ((𝐴 ≼ ω ∧ ∅ ∈ V ∧ ¬ ∅ ∈ 𝐴) → ∃𝑓(𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴)))
61, 3, 4, 5syl3anc 1370 . 2 (𝜑 → ∃𝑓(𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴)))
7 nfv 1916 . . . . 5 𝑧(𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴)))
8 simpr1 1193 . . . . . . 7 ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) → 𝑓:ℕ⟶(𝐴 ∪ {∅}))
98feqmptd 6876 . . . . . 6 ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) → 𝑓 = (𝑘 ∈ ℕ ↦ (𝑓𝑘)))
109rneqd 5866 . . . . 5 ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) → ran 𝑓 = ran (𝑘 ∈ ℕ ↦ (𝑓𝑘)))
117, 10esumeq1d 32109 . . . 4 ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) → Σ*𝑧 ∈ ran 𝑓(𝑀𝑧) = Σ*𝑧 ∈ ran (𝑘 ∈ ℕ ↦ (𝑓𝑘))(𝑀𝑧))
12 fvex 6824 . . . . . . . . . 10 (toCaraSiga‘𝑀) ∈ V
1312a1i 11 . . . . . . . . 9 ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) → (toCaraSiga‘𝑀) ∈ V)
14 carsggect.2 . . . . . . . . . . 11 (𝜑𝐴 ⊆ (toCaraSiga‘𝑀))
1514adantr 481 . . . . . . . . . 10 ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) → 𝐴 ⊆ (toCaraSiga‘𝑀))
16 carsgval.1 . . . . . . . . . . . . 13 (𝜑𝑂𝑉)
1716adantr 481 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) → 𝑂𝑉)
18 carsgval.2 . . . . . . . . . . . . 13 (𝜑𝑀:𝒫 𝑂⟶(0[,]+∞))
1918adantr 481 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) → 𝑀:𝒫 𝑂⟶(0[,]+∞))
20 carsgsiga.1 . . . . . . . . . . . . 13 (𝜑 → (𝑀‘∅) = 0)
2120adantr 481 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) → (𝑀‘∅) = 0)
2217, 19, 210elcarsg 32380 . . . . . . . . . . 11 ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) → ∅ ∈ (toCaraSiga‘𝑀))
2322snssd 4754 . . . . . . . . . 10 ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) → {∅} ⊆ (toCaraSiga‘𝑀))
2415, 23unssd 4131 . . . . . . . . 9 ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) → (𝐴 ∪ {∅}) ⊆ (toCaraSiga‘𝑀))
2513, 24ssexd 5263 . . . . . . . 8 ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) → (𝐴 ∪ {∅}) ∈ V)
2619adantr 481 . . . . . . . . 9 (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) ∧ 𝑧 ∈ (𝐴 ∪ {∅})) → 𝑀:𝒫 𝑂⟶(0[,]+∞))
2716, 18carsgcl 32377 . . . . . . . . . . . . 13 (𝜑 → (toCaraSiga‘𝑀) ⊆ 𝒫 𝑂)
2814, 27sstrd 3941 . . . . . . . . . . . 12 (𝜑𝐴 ⊆ 𝒫 𝑂)
2928adantr 481 . . . . . . . . . . 11 ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) → 𝐴 ⊆ 𝒫 𝑂)
30 0elpw 5293 . . . . . . . . . . . . 13 ∅ ∈ 𝒫 𝑂
3130a1i 11 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) → ∅ ∈ 𝒫 𝑂)
3231snssd 4754 . . . . . . . . . . 11 ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) → {∅} ⊆ 𝒫 𝑂)
3329, 32unssd 4131 . . . . . . . . . 10 ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) → (𝐴 ∪ {∅}) ⊆ 𝒫 𝑂)
3433sselda 3931 . . . . . . . . 9 (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) ∧ 𝑧 ∈ (𝐴 ∪ {∅})) → 𝑧 ∈ 𝒫 𝑂)
3526, 34ffvelcdmd 7001 . . . . . . . 8 (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) ∧ 𝑧 ∈ (𝐴 ∪ {∅})) → (𝑀𝑧) ∈ (0[,]+∞))
368frnd 6645 . . . . . . . 8 ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) → ran 𝑓 ⊆ (𝐴 ∪ {∅}))
377, 25, 35, 36esummono 32128 . . . . . . 7 ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) → Σ*𝑧 ∈ ran 𝑓(𝑀𝑧) ≤ Σ*𝑧 ∈ (𝐴 ∪ {∅})(𝑀𝑧))
38 ctex 8801 . . . . . . . . . 10 (𝐴 ≼ ω → 𝐴 ∈ V)
391, 38syl 17 . . . . . . . . 9 (𝜑𝐴 ∈ V)
4039adantr 481 . . . . . . . 8 ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) → 𝐴 ∈ V)
4113, 23ssexd 5263 . . . . . . . 8 ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) → {∅} ∈ V)
4219adantr 481 . . . . . . . . 9 (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) ∧ 𝑧𝐴) → 𝑀:𝒫 𝑂⟶(0[,]+∞))
4329sselda 3931 . . . . . . . . 9 (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) ∧ 𝑧𝐴) → 𝑧 ∈ 𝒫 𝑂)
4442, 43ffvelcdmd 7001 . . . . . . . 8 (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) ∧ 𝑧𝐴) → (𝑀𝑧) ∈ (0[,]+∞))
45 elsni 4588 . . . . . . . . . . 11 (𝑧 ∈ {∅} → 𝑧 = ∅)
4645adantl 482 . . . . . . . . . 10 (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) ∧ 𝑧 ∈ {∅}) → 𝑧 = ∅)
4746fveq2d 6815 . . . . . . . . 9 (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) ∧ 𝑧 ∈ {∅}) → (𝑀𝑧) = (𝑀‘∅))
4821adantr 481 . . . . . . . . 9 (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) ∧ 𝑧 ∈ {∅}) → (𝑀‘∅) = 0)
4947, 48eqtrd 2777 . . . . . . . 8 (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) ∧ 𝑧 ∈ {∅}) → (𝑀𝑧) = 0)
5040, 41, 44, 49esumpad 32129 . . . . . . 7 ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) → Σ*𝑧 ∈ (𝐴 ∪ {∅})(𝑀𝑧) = Σ*𝑧𝐴(𝑀𝑧))
5137, 50breqtrd 5113 . . . . . 6 ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) → Σ*𝑧 ∈ ran 𝑓(𝑀𝑧) ≤ Σ*𝑧𝐴(𝑀𝑧))
5236, 24sstrd 3941 . . . . . . . 8 ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) → ran 𝑓 ⊆ (toCaraSiga‘𝑀))
53 ssexg 5262 . . . . . . . 8 ((ran 𝑓 ⊆ (toCaraSiga‘𝑀) ∧ (toCaraSiga‘𝑀) ∈ V) → ran 𝑓 ∈ V)
5452, 12, 53sylancl 586 . . . . . . 7 ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) → ran 𝑓 ∈ V)
5519adantr 481 . . . . . . . 8 (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) ∧ 𝑧 ∈ ran 𝑓) → 𝑀:𝒫 𝑂⟶(0[,]+∞))
5636, 33sstrd 3941 . . . . . . . . 9 ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) → ran 𝑓 ⊆ 𝒫 𝑂)
5756sselda 3931 . . . . . . . 8 (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) ∧ 𝑧 ∈ ran 𝑓) → 𝑧 ∈ 𝒫 𝑂)
5855, 57ffvelcdmd 7001 . . . . . . 7 (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) ∧ 𝑧 ∈ ran 𝑓) → (𝑀𝑧) ∈ (0[,]+∞))
59 simpr2 1194 . . . . . . 7 ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) → 𝐴 ⊆ ran 𝑓)
607, 54, 58, 59esummono 32128 . . . . . 6 ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) → Σ*𝑧𝐴(𝑀𝑧) ≤ Σ*𝑧 ∈ ran 𝑓(𝑀𝑧))
6151, 60jca 512 . . . . 5 ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) → (Σ*𝑧 ∈ ran 𝑓(𝑀𝑧) ≤ Σ*𝑧𝐴(𝑀𝑧) ∧ Σ*𝑧𝐴(𝑀𝑧) ≤ Σ*𝑧 ∈ ran 𝑓(𝑀𝑧)))
62 iccssxr 13235 . . . . . . 7 (0[,]+∞) ⊆ ℝ*
6358ralrimiva 3140 . . . . . . . 8 ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) → ∀𝑧 ∈ ran 𝑓(𝑀𝑧) ∈ (0[,]+∞))
64 nfcv 2905 . . . . . . . . 9 𝑧ran 𝑓
6564esumcl 32104 . . . . . . . 8 ((ran 𝑓 ∈ V ∧ ∀𝑧 ∈ ran 𝑓(𝑀𝑧) ∈ (0[,]+∞)) → Σ*𝑧 ∈ ran 𝑓(𝑀𝑧) ∈ (0[,]+∞))
6654, 63, 65syl2anc 584 . . . . . . 7 ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) → Σ*𝑧 ∈ ran 𝑓(𝑀𝑧) ∈ (0[,]+∞))
6762, 66sselid 3929 . . . . . 6 ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) → Σ*𝑧 ∈ ran 𝑓(𝑀𝑧) ∈ ℝ*)
6844ralrimiva 3140 . . . . . . . 8 ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) → ∀𝑧𝐴 (𝑀𝑧) ∈ (0[,]+∞))
69 nfcv 2905 . . . . . . . . 9 𝑧𝐴
7069esumcl 32104 . . . . . . . 8 ((𝐴 ∈ V ∧ ∀𝑧𝐴 (𝑀𝑧) ∈ (0[,]+∞)) → Σ*𝑧𝐴(𝑀𝑧) ∈ (0[,]+∞))
7140, 68, 70syl2anc 584 . . . . . . 7 ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) → Σ*𝑧𝐴(𝑀𝑧) ∈ (0[,]+∞))
7262, 71sselid 3929 . . . . . 6 ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) → Σ*𝑧𝐴(𝑀𝑧) ∈ ℝ*)
73 xrletri3 12961 . . . . . 6 ((Σ*𝑧 ∈ ran 𝑓(𝑀𝑧) ∈ ℝ* ∧ Σ*𝑧𝐴(𝑀𝑧) ∈ ℝ*) → (Σ*𝑧 ∈ ran 𝑓(𝑀𝑧) = Σ*𝑧𝐴(𝑀𝑧) ↔ (Σ*𝑧 ∈ ran 𝑓(𝑀𝑧) ≤ Σ*𝑧𝐴(𝑀𝑧) ∧ Σ*𝑧𝐴(𝑀𝑧) ≤ Σ*𝑧 ∈ ran 𝑓(𝑀𝑧))))
7467, 72, 73syl2anc 584 . . . . 5 ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) → (Σ*𝑧 ∈ ran 𝑓(𝑀𝑧) = Σ*𝑧𝐴(𝑀𝑧) ↔ (Σ*𝑧 ∈ ran 𝑓(𝑀𝑧) ≤ Σ*𝑧𝐴(𝑀𝑧) ∧ Σ*𝑧𝐴(𝑀𝑧) ≤ Σ*𝑧 ∈ ran 𝑓(𝑀𝑧))))
7561, 74mpbird 256 . . . 4 ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) → Σ*𝑧 ∈ ran 𝑓(𝑀𝑧) = Σ*𝑧𝐴(𝑀𝑧))
76 fveq2 6811 . . . . 5 (𝑧 = (𝑓𝑘) → (𝑀𝑧) = (𝑀‘(𝑓𝑘)))
77 nnex 12052 . . . . . 6 ℕ ∈ V
7877a1i 11 . . . . 5 ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) → ℕ ∈ V)
7919adantr 481 . . . . . 6 (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) ∧ 𝑘 ∈ ℕ) → 𝑀:𝒫 𝑂⟶(0[,]+∞))
8033adantr 481 . . . . . . 7 (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) ∧ 𝑘 ∈ ℕ) → (𝐴 ∪ {∅}) ⊆ 𝒫 𝑂)
818adantr 481 . . . . . . . 8 (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) ∧ 𝑘 ∈ ℕ) → 𝑓:ℕ⟶(𝐴 ∪ {∅}))
82 simpr 485 . . . . . . . 8 (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ)
8381, 82ffvelcdmd 7001 . . . . . . 7 (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) ∧ 𝑘 ∈ ℕ) → (𝑓𝑘) ∈ (𝐴 ∪ {∅}))
8480, 83sseldd 3932 . . . . . 6 (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) ∧ 𝑘 ∈ ℕ) → (𝑓𝑘) ∈ 𝒫 𝑂)
8579, 84ffvelcdmd 7001 . . . . 5 (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) ∧ 𝑘 ∈ ℕ) → (𝑀‘(𝑓𝑘)) ∈ (0[,]+∞))
86 simpr 485 . . . . . . 7 ((((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) ∧ 𝑘 ∈ ℕ) ∧ (𝑓𝑘) = ∅) → (𝑓𝑘) = ∅)
8786fveq2d 6815 . . . . . 6 ((((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) ∧ 𝑘 ∈ ℕ) ∧ (𝑓𝑘) = ∅) → (𝑀‘(𝑓𝑘)) = (𝑀‘∅))
8821ad2antrr 723 . . . . . 6 ((((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) ∧ 𝑘 ∈ ℕ) ∧ (𝑓𝑘) = ∅) → (𝑀‘∅) = 0)
8987, 88eqtrd 2777 . . . . 5 ((((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) ∧ 𝑘 ∈ ℕ) ∧ (𝑓𝑘) = ∅) → (𝑀‘(𝑓𝑘)) = 0)
90 cnvimass 6006 . . . . . . 7 (𝑓𝐴) ⊆ dom 𝑓
9190, 8fssdm 6657 . . . . . 6 ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) → (𝑓𝐴) ⊆ ℕ)
92 ffun 6640 . . . . . . . . . . 11 (𝑓:ℕ⟶(𝐴 ∪ {∅}) → Fun 𝑓)
938, 92syl 17 . . . . . . . . . 10 ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) → Fun 𝑓)
9493adantr 481 . . . . . . . . 9 (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) ∧ 𝑘 ∈ (ℕ ∖ (𝑓𝐴))) → Fun 𝑓)
95 difpreima 6981 . . . . . . . . . . . . 13 (Fun 𝑓 → (𝑓 “ ((𝐴 ∪ {∅}) ∖ 𝐴)) = ((𝑓 “ (𝐴 ∪ {∅})) ∖ (𝑓𝐴)))
968, 92, 953syl 18 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) → (𝑓 “ ((𝐴 ∪ {∅}) ∖ 𝐴)) = ((𝑓 “ (𝐴 ∪ {∅})) ∖ (𝑓𝐴)))
97 fimacnv 6659 . . . . . . . . . . . . . 14 (𝑓:ℕ⟶(𝐴 ∪ {∅}) → (𝑓 “ (𝐴 ∪ {∅})) = ℕ)
988, 97syl 17 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) → (𝑓 “ (𝐴 ∪ {∅})) = ℕ)
9998difeq1d 4067 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) → ((𝑓 “ (𝐴 ∪ {∅})) ∖ (𝑓𝐴)) = (ℕ ∖ (𝑓𝐴)))
10096, 99eqtrd 2777 . . . . . . . . . . 11 ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) → (𝑓 “ ((𝐴 ∪ {∅}) ∖ 𝐴)) = (ℕ ∖ (𝑓𝐴)))
101 uncom 4098 . . . . . . . . . . . . . . . 16 ({∅} ∪ 𝐴) = (𝐴 ∪ {∅})
102101difeq1i 4064 . . . . . . . . . . . . . . 15 (({∅} ∪ 𝐴) ∖ 𝐴) = ((𝐴 ∪ {∅}) ∖ 𝐴)
103 difun2 4425 . . . . . . . . . . . . . . 15 (({∅} ∪ 𝐴) ∖ 𝐴) = ({∅} ∖ 𝐴)
104102, 103eqtr3i 2767 . . . . . . . . . . . . . 14 ((𝐴 ∪ {∅}) ∖ 𝐴) = ({∅} ∖ 𝐴)
105 difss 4077 . . . . . . . . . . . . . 14 ({∅} ∖ 𝐴) ⊆ {∅}
106104, 105eqsstri 3965 . . . . . . . . . . . . 13 ((𝐴 ∪ {∅}) ∖ 𝐴) ⊆ {∅}
107106a1i 11 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) → ((𝐴 ∪ {∅}) ∖ 𝐴) ⊆ {∅})
108 sspreima 6984 . . . . . . . . . . . 12 ((Fun 𝑓 ∧ ((𝐴 ∪ {∅}) ∖ 𝐴) ⊆ {∅}) → (𝑓 “ ((𝐴 ∪ {∅}) ∖ 𝐴)) ⊆ (𝑓 “ {∅}))
10993, 107, 108syl2anc 584 . . . . . . . . . . 11 ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) → (𝑓 “ ((𝐴 ∪ {∅}) ∖ 𝐴)) ⊆ (𝑓 “ {∅}))
110100, 109eqsstrrd 3970 . . . . . . . . . 10 ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) → (ℕ ∖ (𝑓𝐴)) ⊆ (𝑓 “ {∅}))
111110sselda 3931 . . . . . . . . 9 (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) ∧ 𝑘 ∈ (ℕ ∖ (𝑓𝐴))) → 𝑘 ∈ (𝑓 “ {∅}))
112 fvimacnvi 6968 . . . . . . . . 9 ((Fun 𝑓𝑘 ∈ (𝑓 “ {∅})) → (𝑓𝑘) ∈ {∅})
11394, 111, 112syl2anc 584 . . . . . . . 8 (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) ∧ 𝑘 ∈ (ℕ ∖ (𝑓𝐴))) → (𝑓𝑘) ∈ {∅})
114 elsni 4588 . . . . . . . 8 ((𝑓𝑘) ∈ {∅} → (𝑓𝑘) = ∅)
115113, 114syl 17 . . . . . . 7 (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) ∧ 𝑘 ∈ (ℕ ∖ (𝑓𝐴))) → (𝑓𝑘) = ∅)
116115ralrimiva 3140 . . . . . 6 ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) → ∀𝑘 ∈ (ℕ ∖ (𝑓𝐴))(𝑓𝑘) = ∅)
117 carsggect.3 . . . . . . . 8 (𝜑Disj 𝑦𝐴 𝑦)
118117adantr 481 . . . . . . 7 ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) → Disj 𝑦𝐴 𝑦)
119 simpr3 1195 . . . . . . . . . 10 ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) → Fun (𝑓𝐴))
120 fresf1o 31074 . . . . . . . . . 10 ((Fun 𝑓𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴)) → (𝑓 ↾ (𝑓𝐴)):(𝑓𝐴)–1-1-onto𝐴)
12193, 59, 119, 120syl3anc 1370 . . . . . . . . 9 ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) → (𝑓 ↾ (𝑓𝐴)):(𝑓𝐴)–1-1-onto𝐴)
122 simpr 485 . . . . . . . . 9 (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) ∧ 𝑦 = ((𝑓 ↾ (𝑓𝐴))‘𝑘)) → 𝑦 = ((𝑓 ↾ (𝑓𝐴))‘𝑘))
123121, 122disjrdx 31038 . . . . . . . 8 ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) → (Disj 𝑘 ∈ (𝑓𝐴)((𝑓 ↾ (𝑓𝐴))‘𝑘) ↔ Disj 𝑦𝐴 𝑦))
124 fvres 6830 . . . . . . . . . 10 (𝑘 ∈ (𝑓𝐴) → ((𝑓 ↾ (𝑓𝐴))‘𝑘) = (𝑓𝑘))
125124adantl 482 . . . . . . . . 9 (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) ∧ 𝑘 ∈ (𝑓𝐴)) → ((𝑓 ↾ (𝑓𝐴))‘𝑘) = (𝑓𝑘))
126125disjeq2dv 5057 . . . . . . . 8 ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) → (Disj 𝑘 ∈ (𝑓𝐴)((𝑓 ↾ (𝑓𝐴))‘𝑘) ↔ Disj 𝑘 ∈ (𝑓𝐴)(𝑓𝑘)))
127123, 126bitr3d 280 . . . . . . 7 ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) → (Disj 𝑦𝐴 𝑦Disj 𝑘 ∈ (𝑓𝐴)(𝑓𝑘)))
128118, 127mpbid 231 . . . . . 6 ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) → Disj 𝑘 ∈ (𝑓𝐴)(𝑓𝑘))
129 disjss3 5086 . . . . . . 7 (((𝑓𝐴) ⊆ ℕ ∧ ∀𝑘 ∈ (ℕ ∖ (𝑓𝐴))(𝑓𝑘) = ∅) → (Disj 𝑘 ∈ (𝑓𝐴)(𝑓𝑘) ↔ Disj 𝑘 ∈ ℕ (𝑓𝑘)))
130129biimpa 477 . . . . . 6 ((((𝑓𝐴) ⊆ ℕ ∧ ∀𝑘 ∈ (ℕ ∖ (𝑓𝐴))(𝑓𝑘) = ∅) ∧ Disj 𝑘 ∈ (𝑓𝐴)(𝑓𝑘)) → Disj 𝑘 ∈ ℕ (𝑓𝑘))
13191, 116, 128, 130syl21anc 835 . . . . 5 ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) → Disj 𝑘 ∈ ℕ (𝑓𝑘))
13276, 78, 85, 84, 89, 131esumrnmpt2 32142 . . . 4 ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) → Σ*𝑧 ∈ ran (𝑘 ∈ ℕ ↦ (𝑓𝑘))(𝑀𝑧) = Σ*𝑘 ∈ ℕ(𝑀‘(𝑓𝑘)))
13311, 75, 1323eqtr3rd 2786 . . 3 ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) → Σ*𝑘 ∈ ℕ(𝑀‘(𝑓𝑘)) = Σ*𝑧𝐴(𝑀𝑧))
134 uniiun 5001 . . . . . . 7 𝐴 = 𝑥𝐴 𝑥
13528sselda 3931 . . . . . . . 8 ((𝜑𝑥𝐴) → 𝑥 ∈ 𝒫 𝑂)
13639, 135elpwiuncl 30984 . . . . . . 7 (𝜑 𝑥𝐴 𝑥 ∈ 𝒫 𝑂)
137134, 136eqeltrid 2842 . . . . . 6 (𝜑 𝐴 ∈ 𝒫 𝑂)
138137adantr 481 . . . . 5 ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) → 𝐴 ∈ 𝒫 𝑂)
13919, 138ffvelcdmd 7001 . . . 4 ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) → (𝑀 𝐴) ∈ (0[,]+∞))
140 carsgsiga.2 . . . . . . . . . 10 ((𝜑𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂) → (𝑀 𝑥) ≤ Σ*𝑦𝑥(𝑀𝑦))
1411403adant1r 1176 . . . . . . . . 9 (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂) → (𝑀 𝑥) ≤ Σ*𝑦𝑥(𝑀𝑦))
142 fveq2 6811 . . . . . . . . . 10 (𝑦 = 𝑧 → (𝑀𝑦) = (𝑀𝑧))
143 nfcv 2905 . . . . . . . . . 10 𝑧𝑥
144 nfcv 2905 . . . . . . . . . 10 𝑦𝑥
145 nfcv 2905 . . . . . . . . . 10 𝑧(𝑀𝑦)
146 nfcv 2905 . . . . . . . . . 10 𝑦(𝑀𝑧)
147142, 143, 144, 145, 146cbvesum 32116 . . . . . . . . 9 Σ*𝑦𝑥(𝑀𝑦) = Σ*𝑧𝑥(𝑀𝑧)
148141, 147breqtrdi 5128 . . . . . . . 8 (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂) → (𝑀 𝑥) ≤ Σ*𝑧𝑥(𝑀𝑧))
149 ffn 6637 . . . . . . . . . 10 (𝑓:ℕ⟶(𝐴 ∪ {∅}) → 𝑓 Fn ℕ)
150 fz1ssnn 13360 . . . . . . . . . . 11 (1...𝑛) ⊆ ℕ
151 fnssres 6593 . . . . . . . . . . 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 13765 . . . . . . . . . 10 (1...𝑛) ∈ Fin
155 fnfi 9023 . . . . . . . . . 10 (((𝑓 ↾ (1...𝑛)) Fn (1...𝑛) ∧ (1...𝑛) ∈ Fin) → (𝑓 ↾ (1...𝑛)) ∈ Fin)
156154, 155mpan2 688 . . . . . . . . 9 ((𝑓 ↾ (1...𝑛)) Fn (1...𝑛) → (𝑓 ↾ (1...𝑛)) ∈ Fin)
157 rnfi 9172 . . . . . . . . 9 ((𝑓 ↾ (1...𝑛)) ∈ Fin → ran (𝑓 ↾ (1...𝑛)) ∈ Fin)
158153, 156, 1573syl 18 . . . . . . . 8 ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) → ran (𝑓 ↾ (1...𝑛)) ∈ Fin)
159 resss 5935 . . . . . . . . . . 11 (𝑓 ↾ (1...𝑛)) ⊆ 𝑓
160 rnss 5867 . . . . . . . . . . 11 ((𝑓 ↾ (1...𝑛)) ⊆ 𝑓 → ran (𝑓 ↾ (1...𝑛)) ⊆ ran 𝑓)
161159, 160ax-mp 5 . . . . . . . . . 10 ran (𝑓 ↾ (1...𝑛)) ⊆ ran 𝑓
162161a1i 11 . . . . . . . . 9 ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) → ran (𝑓 ↾ (1...𝑛)) ⊆ ran 𝑓)
163162, 52sstrd 3941 . . . . . . . 8 ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) → ran (𝑓 ↾ (1...𝑛)) ⊆ (toCaraSiga‘𝑀))
164162, 36sstrd 3941 . . . . . . . . 9 ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) → ran (𝑓 ↾ (1...𝑛)) ⊆ (𝐴 ∪ {∅}))
165 nfcv 2905 . . . . . . . . . . . . 13 𝑧𝑦
166 nfcv 2905 . . . . . . . . . . . . 13 𝑦𝑧
167 id 22 . . . . . . . . . . . . 13 (𝑦 = 𝑧𝑦 = 𝑧)
168165, 166, 167cbvdisj 5062 . . . . . . . . . . . 12 (Disj 𝑦𝐴 𝑦Disj 𝑧𝐴 𝑧)
169 disjun0 31042 . . . . . . . . . . . 12 (Disj 𝑧𝐴 𝑧Disj 𝑧 ∈ (𝐴 ∪ {∅})𝑧)
170168, 169sylbi 216 . . . . . . . . . . 11 (Disj 𝑦𝐴 𝑦Disj 𝑧 ∈ (𝐴 ∪ {∅})𝑧)
171117, 170syl 17 . . . . . . . . . 10 (𝜑Disj 𝑧 ∈ (𝐴 ∪ {∅})𝑧)
172171adantr 481 . . . . . . . . 9 ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) → Disj 𝑧 ∈ (𝐴 ∪ {∅})𝑧)
173 disjss1 5058 . . . . . . . . 9 (ran (𝑓 ↾ (1...𝑛)) ⊆ (𝐴 ∪ {∅}) → (Disj 𝑧 ∈ (𝐴 ∪ {∅})𝑧Disj 𝑧 ∈ ran (𝑓 ↾ (1...𝑛))𝑧))
174164, 172, 173sylc 65 . . . . . . . 8 ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) → Disj 𝑧 ∈ ran (𝑓 ↾ (1...𝑛))𝑧)
175 pwidg 4565 . . . . . . . . 9 (𝑂𝑉𝑂 ∈ 𝒫 𝑂)
17617, 175syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) → 𝑂 ∈ 𝒫 𝑂)
17717, 19, 21, 148, 158, 163, 174, 176carsgclctunlem1 32390 . . . . . . 7 ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) → (𝑀‘(𝑂 ran (𝑓 ↾ (1...𝑛)))) = Σ*𝑧 ∈ ran (𝑓 ↾ (1...𝑛))(𝑀‘(𝑂𝑧)))
178177adantr 481 . . . . . 6 (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) ∧ 𝑛 ∈ ℕ) → (𝑀‘(𝑂 ran (𝑓 ↾ (1...𝑛)))) = Σ*𝑧 ∈ ran (𝑓 ↾ (1...𝑛))(𝑀‘(𝑂𝑧)))
179164unissd 4860 . . . . . . . . . . 11 ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) → ran (𝑓 ↾ (1...𝑛)) ⊆ (𝐴 ∪ {∅}))
180 uniun 4876 . . . . . . . . . . . 12 (𝐴 ∪ {∅}) = ( 𝐴 {∅})
1812unisn 4872 . . . . . . . . . . . . 13 {∅} = ∅
182181uneq2i 4105 . . . . . . . . . . . 12 ( 𝐴 {∅}) = ( 𝐴 ∪ ∅)
183 un0 4335 . . . . . . . . . . . 12 ( 𝐴 ∪ ∅) = 𝐴
184180, 182, 1833eqtri 2769 . . . . . . . . . . 11 (𝐴 ∪ {∅}) = 𝐴
185179, 184sseqtrdi 3981 . . . . . . . . . 10 ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) → ran (𝑓 ↾ (1...𝑛)) ⊆ 𝐴)
186185adantr 481 . . . . . . . . 9 (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) ∧ 𝑛 ∈ ℕ) → ran (𝑓 ↾ (1...𝑛)) ⊆ 𝐴)
187 uniss 4858 . . . . . . . . . . . 12 (𝐴 ⊆ 𝒫 𝑂 𝐴 𝒫 𝑂)
188 unipw 5385 . . . . . . . . . . . 12 𝒫 𝑂 = 𝑂
189187, 188sseqtrdi 3981 . . . . . . . . . . 11 (𝐴 ⊆ 𝒫 𝑂 𝐴𝑂)
19028, 189syl 17 . . . . . . . . . 10 (𝜑 𝐴𝑂)
191190ad2antrr 723 . . . . . . . . 9 (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) ∧ 𝑛 ∈ ℕ) → 𝐴𝑂)
192186, 191sstrd 3941 . . . . . . . 8 (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) ∧ 𝑛 ∈ ℕ) → ran (𝑓 ↾ (1...𝑛)) ⊆ 𝑂)
193 sseqin2 4160 . . . . . . . 8 ( ran (𝑓 ↾ (1...𝑛)) ⊆ 𝑂 ↔ (𝑂 ran (𝑓 ↾ (1...𝑛))) = ran (𝑓 ↾ (1...𝑛)))
194192, 193sylib 217 . . . . . . 7 (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) ∧ 𝑛 ∈ ℕ) → (𝑂 ran (𝑓 ↾ (1...𝑛))) = ran (𝑓 ↾ (1...𝑛)))
195194fveq2d 6815 . . . . . 6 (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) ∧ 𝑛 ∈ ℕ) → (𝑀‘(𝑂 ran (𝑓 ↾ (1...𝑛)))) = (𝑀 ran (𝑓 ↾ (1...𝑛))))
196 nfv 1916 . . . . . . . 8 𝑧((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) ∧ 𝑛 ∈ ℕ)
197164adantr 481 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) ∧ 𝑛 ∈ ℕ) → ran (𝑓 ↾ (1...𝑛)) ⊆ (𝐴 ∪ {∅}))
19828ad2antrr 723 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) ∧ 𝑛 ∈ ℕ) → 𝐴 ⊆ 𝒫 𝑂)
19930a1i 11 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) ∧ 𝑛 ∈ ℕ) → ∅ ∈ 𝒫 𝑂)
200199snssd 4754 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) ∧ 𝑛 ∈ ℕ) → {∅} ⊆ 𝒫 𝑂)
201198, 200unssd 4131 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) ∧ 𝑛 ∈ ℕ) → (𝐴 ∪ {∅}) ⊆ 𝒫 𝑂)
202197, 201sstrd 3941 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) ∧ 𝑛 ∈ ℕ) → ran (𝑓 ↾ (1...𝑛)) ⊆ 𝒫 𝑂)
203202sselda 3931 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) ∧ 𝑛 ∈ ℕ) ∧ 𝑧 ∈ ran (𝑓 ↾ (1...𝑛))) → 𝑧 ∈ 𝒫 𝑂)
204203elpwid 4554 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) ∧ 𝑛 ∈ ℕ) ∧ 𝑧 ∈ ran (𝑓 ↾ (1...𝑛))) → 𝑧𝑂)
205 sseqin2 4160 . . . . . . . . . . 11 (𝑧𝑂 ↔ (𝑂𝑧) = 𝑧)
206204, 205sylib 217 . . . . . . . . . 10 ((((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) ∧ 𝑛 ∈ ℕ) ∧ 𝑧 ∈ ran (𝑓 ↾ (1...𝑛))) → (𝑂𝑧) = 𝑧)
207206fveq2d 6815 . . . . . . . . 9 ((((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) ∧ 𝑛 ∈ ℕ) ∧ 𝑧 ∈ ran (𝑓 ↾ (1...𝑛))) → (𝑀‘(𝑂𝑧)) = (𝑀𝑧))
208207ralrimiva 3140 . . . . . . . 8 (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) ∧ 𝑛 ∈ ℕ) → ∀𝑧 ∈ ran (𝑓 ↾ (1...𝑛))(𝑀‘(𝑂𝑧)) = (𝑀𝑧))
209196, 208esumeq2d 32111 . . . . . . 7 (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) ∧ 𝑛 ∈ ℕ) → Σ*𝑧 ∈ ran (𝑓 ↾ (1...𝑛))(𝑀‘(𝑂𝑧)) = Σ*𝑧 ∈ ran (𝑓 ↾ (1...𝑛))(𝑀𝑧))
2109reseq1d 5909 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) → (𝑓 ↾ (1...𝑛)) = ((𝑘 ∈ ℕ ↦ (𝑓𝑘)) ↾ (1...𝑛)))
211210adantr 481 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) ∧ 𝑛 ∈ ℕ) → (𝑓 ↾ (1...𝑛)) = ((𝑘 ∈ ℕ ↦ (𝑓𝑘)) ↾ (1...𝑛)))
212 resmpt 5964 . . . . . . . . . . . 12 ((1...𝑛) ⊆ ℕ → ((𝑘 ∈ ℕ ↦ (𝑓𝑘)) ↾ (1...𝑛)) = (𝑘 ∈ (1...𝑛) ↦ (𝑓𝑘)))
213150, 212ax-mp 5 . . . . . . . . . . 11 ((𝑘 ∈ ℕ ↦ (𝑓𝑘)) ↾ (1...𝑛)) = (𝑘 ∈ (1...𝑛) ↦ (𝑓𝑘))
214211, 213eqtrdi 2793 . . . . . . . . . 10 (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) ∧ 𝑛 ∈ ℕ) → (𝑓 ↾ (1...𝑛)) = (𝑘 ∈ (1...𝑛) ↦ (𝑓𝑘)))
215214eqcomd 2743 . . . . . . . . 9 (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) ∧ 𝑛 ∈ ℕ) → (𝑘 ∈ (1...𝑛) ↦ (𝑓𝑘)) = (𝑓 ↾ (1...𝑛)))
216215rneqd 5866 . . . . . . . 8 (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) ∧ 𝑛 ∈ ℕ) → ran (𝑘 ∈ (1...𝑛) ↦ (𝑓𝑘)) = ran (𝑓 ↾ (1...𝑛)))
217196, 216esumeq1d 32109 . . . . . . 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 3931 . . . . . . . . . 10 ((((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ ℕ)
22284adantlr 712 . . . . . . . . . 10 ((((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → (𝑓𝑘) ∈ 𝒫 𝑂)
223221, 222syldan 591 . . . . . . . . 9 ((((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝑓𝑘) ∈ 𝒫 𝑂)
224219, 223ffvelcdmd 7001 . . . . . . . 8 ((((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝑀‘(𝑓𝑘)) ∈ (0[,]+∞))
225 simpr 485 . . . . . . . . . 10 (((((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) ∧ (𝑓𝑘) = ∅) → (𝑓𝑘) = ∅)
226225fveq2d 6815 . . . . . . . . 9 (((((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) ∧ (𝑓𝑘) = ∅) → (𝑀‘(𝑓𝑘)) = (𝑀‘∅))
22721ad3antrrr 727 . . . . . . . . 9 (((((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) ∧ (𝑓𝑘) = ∅) → (𝑀‘∅) = 0)
228226, 227eqtrd 2777 . . . . . . . 8 (((((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) ∧ (𝑓𝑘) = ∅) → (𝑀‘(𝑓𝑘)) = 0)
229 disjss1 5058 . . . . . . . . . . 11 ((1...𝑛) ⊆ ℕ → (Disj 𝑘 ∈ ℕ (𝑓𝑘) → Disj 𝑘 ∈ (1...𝑛)(𝑓𝑘)))
230150, 229ax-mp 5 . . . . . . . . . 10 (Disj 𝑘 ∈ ℕ (𝑓𝑘) → Disj 𝑘 ∈ (1...𝑛)(𝑓𝑘))
231131, 230syl 17 . . . . . . . . 9 ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) → Disj 𝑘 ∈ (1...𝑛)(𝑓𝑘))
232231adantr 481 . . . . . . . 8 (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) ∧ 𝑛 ∈ ℕ) → Disj 𝑘 ∈ (1...𝑛)(𝑓𝑘))
23376, 218, 224, 223, 228, 232esumrnmpt2 32142 . . . . . . 7 (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) ∧ 𝑛 ∈ ℕ) → Σ*𝑧 ∈ ran (𝑘 ∈ (1...𝑛) ↦ (𝑓𝑘))(𝑀𝑧) = Σ*𝑘 ∈ (1...𝑛)(𝑀‘(𝑓𝑘)))
234209, 217, 2333eqtr2d 2783 . . . . . 6 (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) ∧ 𝑛 ∈ ℕ) → Σ*𝑧 ∈ ran (𝑓 ↾ (1...𝑛))(𝑀‘(𝑂𝑧)) = Σ*𝑘 ∈ (1...𝑛)(𝑀‘(𝑓𝑘)))
235178, 195, 2343eqtr3d 2785 . . . . 5 (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) ∧ 𝑛 ∈ ℕ) → (𝑀 ran (𝑓 ↾ (1...𝑛))) = Σ*𝑘 ∈ (1...𝑛)(𝑀‘(𝑓𝑘)))
236 carsggect.4 . . . . . . . 8 ((𝜑𝑥𝑦𝑦 ∈ 𝒫 𝑂) → (𝑀𝑥) ≤ (𝑀𝑦))
2372363adant1r 1176 . . . . . . 7 (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) ∧ 𝑥𝑦𝑦 ∈ 𝒫 𝑂) → (𝑀𝑥) ≤ (𝑀𝑦))
23817, 19, 185, 138, 237carsgmon 32387 . . . . . 6 ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) → (𝑀 ran (𝑓 ↾ (1...𝑛))) ≤ (𝑀 𝐴))
239238adantr 481 . . . . 5 (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) ∧ 𝑛 ∈ ℕ) → (𝑀 ran (𝑓 ↾ (1...𝑛))) ≤ (𝑀 𝐴))
240235, 239eqbrtrrd 5111 . . . 4 (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) ∧ 𝑛 ∈ ℕ) → Σ*𝑘 ∈ (1...𝑛)(𝑀‘(𝑓𝑘)) ≤ (𝑀 𝐴))
241139, 85, 240esumgect 32164 . . 3 ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) → Σ*𝑘 ∈ ℕ(𝑀‘(𝑓𝑘)) ≤ (𝑀 𝐴))
242133, 241eqbrtrrd 5111 . 2 ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (𝑓𝐴))) → Σ*𝑧𝐴(𝑀𝑧) ≤ (𝑀 𝐴))
2436, 242exlimddv 1937 1 (𝜑 → Σ*𝑧𝐴(𝑀𝑧) ≤ (𝑀 𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  w3a 1086   = wceq 1540  wex 1780  wcel 2105  wral 3062  Vcvv 3441  cdif 3894  cun 3895  cin 3896  wss 3897  c0 4267  𝒫 cpw 4545  {csn 4571   cuni 4850   ciun 4937  Disj wdisj 5052   class class class wbr 5087  cmpt 5170  ccnv 5606  ran crn 5608  cres 5609  cima 5610  Fun wfun 6459   Fn wfn 6460  wf 6461  1-1-ontowf1o 6464  cfv 6465  (class class class)co 7315  ωcom 7757  cdom 8779  Fincfn 8781  0cc0 10944  1c1 10945  +∞cpnf 11079  *cxr 11081  cle 11083  cn 12046  [,]cicc 13155  ...cfz 13312  Σ*cesum 32101  toCaraSigaccarsg 32374
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2708  ax-rep 5224  ax-sep 5238  ax-nul 5245  ax-pow 5303  ax-pr 5367  ax-un 7628  ax-inf2 9470  ax-cnex 11000  ax-resscn 11001  ax-1cn 11002  ax-icn 11003  ax-addcl 11004  ax-addrcl 11005  ax-mulcl 11006  ax-mulrcl 11007  ax-mulcom 11008  ax-addass 11009  ax-mulass 11010  ax-distr 11011  ax-i2m1 11012  ax-1ne0 11013  ax-1rid 11014  ax-rnegex 11015  ax-rrecex 11016  ax-cnre 11017  ax-pre-lttri 11018  ax-pre-lttrn 11019  ax-pre-ltadd 11020  ax-pre-mulgt0 11021  ax-pre-sup 11022  ax-addf 11023  ax-mulf 11024
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3350  df-reu 3351  df-rab 3405  df-v 3443  df-sbc 3727  df-csb 3843  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3916  df-nul 4268  df-if 4472  df-pw 4547  df-sn 4572  df-pr 4574  df-tp 4576  df-op 4578  df-uni 4851  df-int 4893  df-iun 4939  df-iin 4940  df-disj 5053  df-br 5088  df-opab 5150  df-mpt 5171  df-tr 5205  df-id 5507  df-eprel 5513  df-po 5521  df-so 5522  df-fr 5562  df-se 5563  df-we 5564  df-xp 5613  df-rel 5614  df-cnv 5615  df-co 5616  df-dm 5617  df-rn 5618  df-res 5619  df-ima 5620  df-pred 6224  df-ord 6291  df-on 6292  df-lim 6293  df-suc 6294  df-iota 6417  df-fun 6467  df-fn 6468  df-f 6469  df-f1 6470  df-fo 6471  df-f1o 6472  df-fv 6473  df-isom 6474  df-riota 7272  df-ov 7318  df-oprab 7319  df-mpo 7320  df-of 7573  df-om 7758  df-1st 7876  df-2nd 7877  df-supp 8025  df-frecs 8144  df-wrecs 8175  df-recs 8249  df-rdg 8288  df-1o 8344  df-2o 8345  df-er 8546  df-map 8665  df-pm 8666  df-ixp 8734  df-en 8782  df-dom 8783  df-sdom 8784  df-fin 8785  df-fsupp 9199  df-fi 9240  df-sup 9271  df-inf 9272  df-oi 9339  df-dju 9730  df-card 9768  df-pnf 11084  df-mnf 11085  df-xr 11086  df-ltxr 11087  df-le 11088  df-sub 11280  df-neg 11281  df-div 11706  df-nn 12047  df-2 12109  df-3 12110  df-4 12111  df-5 12112  df-6 12113  df-7 12114  df-8 12115  df-9 12116  df-n0 12307  df-z 12393  df-dec 12511  df-uz 12656  df-q 12762  df-rp 12804  df-xneg 12921  df-xadd 12922  df-xmul 12923  df-ioo 13156  df-ioc 13157  df-ico 13158  df-icc 13159  df-fz 13313  df-fzo 13456  df-fl 13585  df-mod 13663  df-seq 13795  df-exp 13856  df-fac 14061  df-bc 14090  df-hash 14118  df-shft 14850  df-cj 14882  df-re 14883  df-im 14884  df-sqrt 15018  df-abs 15019  df-limsup 15252  df-clim 15269  df-rlim 15270  df-sum 15470  df-ef 15849  df-sin 15851  df-cos 15852  df-pi 15854  df-struct 16918  df-sets 16935  df-slot 16953  df-ndx 16965  df-base 16983  df-ress 17012  df-plusg 17045  df-mulr 17046  df-starv 17047  df-sca 17048  df-vsca 17049  df-ip 17050  df-tset 17051  df-ple 17052  df-ds 17054  df-unif 17055  df-hom 17056  df-cco 17057  df-rest 17203  df-topn 17204  df-0g 17222  df-gsum 17223  df-topgen 17224  df-pt 17225  df-prds 17228  df-ordt 17282  df-xrs 17283  df-qtop 17288  df-imas 17289  df-xps 17291  df-mre 17365  df-mrc 17366  df-acs 17368  df-ps 18354  df-tsr 18355  df-plusf 18395  df-mgm 18396  df-sgrp 18445  df-mnd 18456  df-mhm 18500  df-submnd 18501  df-grp 18649  df-minusg 18650  df-sbg 18651  df-mulg 18770  df-subg 18821  df-cntz 18992  df-cmn 19456  df-abl 19457  df-mgp 19789  df-ur 19806  df-ring 19853  df-cring 19854  df-subrg 20094  df-abv 20149  df-lmod 20197  df-scaf 20198  df-sra 20506  df-rgmod 20507  df-psmet 20661  df-xmet 20662  df-met 20663  df-bl 20664  df-mopn 20665  df-fbas 20666  df-fg 20667  df-cnfld 20670  df-top 22115  df-topon 22132  df-topsp 22154  df-bases 22168  df-cld 22242  df-ntr 22243  df-cls 22244  df-nei 22321  df-lp 22359  df-perf 22360  df-cn 22450  df-cnp 22451  df-haus 22538  df-tx 22785  df-hmeo 22978  df-fil 23069  df-fm 23161  df-flim 23162  df-flf 23163  df-tmd 23295  df-tgp 23296  df-tsms 23350  df-trg 23383  df-xms 23545  df-ms 23546  df-tms 23547  df-nm 23810  df-ngp 23811  df-nrg 23813  df-nlm 23814  df-ii 24112  df-cncf 24113  df-limc 25102  df-dv 25103  df-log 25784  df-esum 32102  df-carsg 32375
This theorem is referenced by:  omsmeas  32396
  Copyright terms: Public domain W3C validator