| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ismeannd.mf | . . . . 5
⊢ (𝜑 → 𝑀:𝑆⟶(0[,]+∞)) | 
| 2 | 1 | fdmd 6746 | . . . . . 6
⊢ (𝜑 → dom 𝑀 = 𝑆) | 
| 3 | 2 | feq2d 6722 | . . . . 5
⊢ (𝜑 → (𝑀:dom 𝑀⟶(0[,]+∞) ↔ 𝑀:𝑆⟶(0[,]+∞))) | 
| 4 | 1, 3 | mpbird 257 | . . . 4
⊢ (𝜑 → 𝑀:dom 𝑀⟶(0[,]+∞)) | 
| 5 |  | ismeannd.sal | . . . . 5
⊢ (𝜑 → 𝑆 ∈ SAlg) | 
| 6 | 2, 5 | eqeltrd 2841 | . . . 4
⊢ (𝜑 → dom 𝑀 ∈ SAlg) | 
| 7 | 4, 6 | jca 511 | . . 3
⊢ (𝜑 → (𝑀:dom 𝑀⟶(0[,]+∞) ∧ dom 𝑀 ∈ SAlg)) | 
| 8 |  | ismeannd.m0 | . . 3
⊢ (𝜑 → (𝑀‘∅) = 0) | 
| 9 |  | unieq 4918 | . . . . . . . . . . . 12
⊢ (𝑥 = ∅ → ∪ 𝑥 =
∪ ∅) | 
| 10 |  | uni0 4935 | . . . . . . . . . . . . 13
⊢ ∪ ∅ = ∅ | 
| 11 | 10 | a1i 11 | . . . . . . . . . . . 12
⊢ (𝑥 = ∅ → ∪ ∅ = ∅) | 
| 12 | 9, 11 | eqtrd 2777 | . . . . . . . . . . 11
⊢ (𝑥 = ∅ → ∪ 𝑥 =
∅) | 
| 13 | 12 | fveq2d 6910 | . . . . . . . . . 10
⊢ (𝑥 = ∅ → (𝑀‘∪ 𝑥) =
(𝑀‘∅)) | 
| 14 | 13, 8 | sylan9eqr 2799 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 = ∅) → (𝑀‘∪ 𝑥) = 0) | 
| 15 |  | reseq2 5992 | . . . . . . . . . . . . 13
⊢ (𝑥 = ∅ → (𝑀 ↾ 𝑥) = (𝑀 ↾ ∅)) | 
| 16 |  | res0 6001 | . . . . . . . . . . . . . 14
⊢ (𝑀 ↾ ∅) =
∅ | 
| 17 | 16 | a1i 11 | . . . . . . . . . . . . 13
⊢ (𝑥 = ∅ → (𝑀 ↾ ∅) =
∅) | 
| 18 | 15, 17 | eqtrd 2777 | . . . . . . . . . . . 12
⊢ (𝑥 = ∅ → (𝑀 ↾ 𝑥) = ∅) | 
| 19 | 18 | fveq2d 6910 | . . . . . . . . . . 11
⊢ (𝑥 = ∅ →
(Σ^‘(𝑀 ↾ 𝑥)) =
(Σ^‘∅)) | 
| 20 | 19 | adantl 481 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 = ∅) →
(Σ^‘(𝑀 ↾ 𝑥)) =
(Σ^‘∅)) | 
| 21 |  | sge00 46391 | . . . . . . . . . . 11
⊢
(Σ^‘∅) = 0 | 
| 22 | 21 | a1i 11 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 = ∅) →
(Σ^‘∅) = 0) | 
| 23 | 20, 22 | eqtrd 2777 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 = ∅) →
(Σ^‘(𝑀 ↾ 𝑥)) = 0) | 
| 24 | 14, 23 | eqtr4d 2780 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 = ∅) → (𝑀‘∪ 𝑥) =
(Σ^‘(𝑀 ↾ 𝑥))) | 
| 25 | 24 | adantlr 715 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) ∧ 𝑥 = ∅) → (𝑀‘∪ 𝑥) =
(Σ^‘(𝑀 ↾ 𝑥))) | 
| 26 | 25 | adantlr 715 | . . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) ∧ (𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦)) ∧ 𝑥 = ∅) → (𝑀‘∪ 𝑥) =
(Σ^‘(𝑀 ↾ 𝑥))) | 
| 27 |  | simpll 767 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) ∧ (𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦)) ∧ ¬ 𝑥 = ∅) → (𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀)) | 
| 28 |  | simplrr 778 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) ∧ (𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦)) ∧ ¬ 𝑥 = ∅) → Disj 𝑦 ∈ 𝑥 𝑦) | 
| 29 | 27, 28 | jca 511 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) ∧ (𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦)) ∧ ¬ 𝑥 = ∅) → ((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) ∧ Disj 𝑦 ∈ 𝑥 𝑦)) | 
| 30 |  | simplrl 777 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) ∧ (𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦)) ∧ ¬ 𝑥 = ∅) → 𝑥 ≼ ω) | 
| 31 |  | neqne 2948 | . . . . . . . . 9
⊢ (¬
𝑥 = ∅ → 𝑥 ≠ ∅) | 
| 32 | 31 | adantl 481 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) ∧ (𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦)) ∧ ¬ 𝑥 = ∅) → 𝑥 ≠ ∅) | 
| 33 |  | id 22 | . . . . . . . . . . . 12
⊢ (𝑦 = 𝑤 → 𝑦 = 𝑤) | 
| 34 | 33 | cbvdisjv 5121 | . . . . . . . . . . 11
⊢
(Disj 𝑦
∈ 𝑥 𝑦 ↔ Disj 𝑤 ∈ 𝑥 𝑤) | 
| 35 | 34 | biimpi 216 | . . . . . . . . . 10
⊢
(Disj 𝑦
∈ 𝑥 𝑦 → Disj 𝑤 ∈ 𝑥 𝑤) | 
| 36 | 35 | adantl 481 | . . . . . . . . 9
⊢ ((𝑥 ≼ ω ∧
Disj 𝑦 ∈ 𝑥 𝑦) → Disj 𝑤 ∈ 𝑥 𝑤) | 
| 37 | 36 | ad2antlr 727 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) ∧ (𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦)) ∧ ¬ 𝑥 = ∅) → Disj 𝑤 ∈ 𝑥 𝑤) | 
| 38 | 30, 32, 37 | nnfoctbdj 46471 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) ∧ (𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦)) ∧ ¬ 𝑥 = ∅) → ∃𝑒(𝑒:ℕ–onto→(𝑥 ∪ {∅}) ∧ Disj 𝑛 ∈ ℕ (𝑒‘𝑛))) | 
| 39 |  | simpl 482 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) ∧ Disj 𝑦 ∈ 𝑥 𝑦) ∧ (𝑒:ℕ–onto→(𝑥 ∪ {∅}) ∧ Disj 𝑛 ∈ ℕ (𝑒‘𝑛))) → ((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) ∧ Disj 𝑦 ∈ 𝑥 𝑦)) | 
| 40 |  | simprl 771 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) ∧ Disj 𝑦 ∈ 𝑥 𝑦) ∧ (𝑒:ℕ–onto→(𝑥 ∪ {∅}) ∧ Disj 𝑛 ∈ ℕ (𝑒‘𝑛))) → 𝑒:ℕ–onto→(𝑥 ∪ {∅})) | 
| 41 |  | simprr 773 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) ∧ Disj 𝑦 ∈ 𝑥 𝑦) ∧ (𝑒:ℕ–onto→(𝑥 ∪ {∅}) ∧ Disj 𝑛 ∈ ℕ (𝑒‘𝑛))) → Disj 𝑛 ∈ ℕ (𝑒‘𝑛)) | 
| 42 |  | founiiun0 45195 | . . . . . . . . . . . . 13
⊢ (𝑒:ℕ–onto→(𝑥 ∪ {∅}) → ∪ 𝑥 =
∪ 𝑛 ∈ ℕ (𝑒‘𝑛)) | 
| 43 | 42 | fveq2d 6910 | . . . . . . . . . . . 12
⊢ (𝑒:ℕ–onto→(𝑥 ∪ {∅}) → (𝑀‘∪ 𝑥) = (𝑀‘∪
𝑛 ∈ ℕ (𝑒‘𝑛))) | 
| 44 | 43 | ad2antlr 727 | . . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) ∧ Disj 𝑦 ∈ 𝑥 𝑦) ∧ 𝑒:ℕ–onto→(𝑥 ∪ {∅})) ∧ Disj 𝑛 ∈ ℕ (𝑒‘𝑛)) → (𝑀‘∪ 𝑥) = (𝑀‘∪
𝑛 ∈ ℕ (𝑒‘𝑛))) | 
| 45 |  | simplll 775 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) ∧ 𝑒:ℕ–onto→(𝑥 ∪ {∅})) ∧ Disj 𝑛 ∈ ℕ (𝑒‘𝑛)) → 𝜑) | 
| 46 |  | fof 6820 | . . . . . . . . . . . . . . . 16
⊢ (𝑒:ℕ–onto→(𝑥 ∪ {∅}) → 𝑒:ℕ⟶(𝑥 ∪ {∅})) | 
| 47 | 46 | adantl 481 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) ∧ 𝑒:ℕ–onto→(𝑥 ∪ {∅})) → 𝑒:ℕ⟶(𝑥 ∪ {∅})) | 
| 48 |  | elpwi 4607 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ 𝒫 dom 𝑀 → 𝑥 ⊆ dom 𝑀) | 
| 49 | 48 | adantl 481 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) → 𝑥 ⊆ dom 𝑀) | 
| 50 | 2 | adantr 480 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) → dom 𝑀 = 𝑆) | 
| 51 | 49, 50 | sseqtrd 4020 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) → 𝑥 ⊆ 𝑆) | 
| 52 |  | 0sal 46335 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑆 ∈ SAlg → ∅
∈ 𝑆) | 
| 53 | 5, 52 | syl 17 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ∅ ∈ 𝑆) | 
| 54 |  | snssi 4808 | . . . . . . . . . . . . . . . . . . 19
⊢ (∅
∈ 𝑆 → {∅}
⊆ 𝑆) | 
| 55 | 53, 54 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → {∅} ⊆ 𝑆) | 
| 56 | 55 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) → {∅} ⊆ 𝑆) | 
| 57 | 51, 56 | unssd 4192 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) → (𝑥 ∪ {∅}) ⊆ 𝑆) | 
| 58 | 57 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) ∧ 𝑒:ℕ–onto→(𝑥 ∪ {∅})) → (𝑥 ∪ {∅}) ⊆ 𝑆) | 
| 59 | 47, 58 | fssd 6753 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) ∧ 𝑒:ℕ–onto→(𝑥 ∪ {∅})) → 𝑒:ℕ⟶𝑆) | 
| 60 | 59 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) ∧ 𝑒:ℕ–onto→(𝑥 ∪ {∅})) ∧ Disj 𝑛 ∈ ℕ (𝑒‘𝑛)) → 𝑒:ℕ⟶𝑆) | 
| 61 |  | simpr 484 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) ∧ 𝑒:ℕ–onto→(𝑥 ∪ {∅})) ∧ Disj 𝑛 ∈ ℕ (𝑒‘𝑛)) → Disj 𝑛 ∈ ℕ (𝑒‘𝑛)) | 
| 62 |  | ismeannd.iun | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑒:ℕ⟶𝑆 ∧ Disj 𝑛 ∈ ℕ (𝑒‘𝑛)) → (𝑀‘∪
𝑛 ∈ ℕ (𝑒‘𝑛)) =
(Σ^‘(𝑛 ∈ ℕ ↦ (𝑀‘(𝑒‘𝑛))))) | 
| 63 | 45, 60, 61, 62 | syl3anc 1373 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) ∧ 𝑒:ℕ–onto→(𝑥 ∪ {∅})) ∧ Disj 𝑛 ∈ ℕ (𝑒‘𝑛)) → (𝑀‘∪
𝑛 ∈ ℕ (𝑒‘𝑛)) =
(Σ^‘(𝑛 ∈ ℕ ↦ (𝑀‘(𝑒‘𝑛))))) | 
| 64 | 63 | adantllr 719 | . . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) ∧ Disj 𝑦 ∈ 𝑥 𝑦) ∧ 𝑒:ℕ–onto→(𝑥 ∪ {∅})) ∧ Disj 𝑛 ∈ ℕ (𝑒‘𝑛)) → (𝑀‘∪
𝑛 ∈ ℕ (𝑒‘𝑛)) =
(Σ^‘(𝑛 ∈ ℕ ↦ (𝑀‘(𝑒‘𝑛))))) | 
| 65 | 1 | feqmptd 6977 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑀 = (𝑦 ∈ 𝑆 ↦ (𝑀‘𝑦))) | 
| 66 | 65 | reseq1d 5996 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑀 ↾ 𝑥) = ((𝑦 ∈ 𝑆 ↦ (𝑀‘𝑦)) ↾ 𝑥)) | 
| 67 | 66 | adantr 480 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) → (𝑀 ↾ 𝑥) = ((𝑦 ∈ 𝑆 ↦ (𝑀‘𝑦)) ↾ 𝑥)) | 
| 68 | 67 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) ∧ ∅ ∈ 𝑥) → (𝑀 ↾ 𝑥) = ((𝑦 ∈ 𝑆 ↦ (𝑀‘𝑦)) ↾ 𝑥)) | 
| 69 | 51 | resmptd 6058 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) → ((𝑦 ∈ 𝑆 ↦ (𝑀‘𝑦)) ↾ 𝑥) = (𝑦 ∈ 𝑥 ↦ (𝑀‘𝑦))) | 
| 70 | 69 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) ∧ ∅ ∈ 𝑥) → ((𝑦 ∈ 𝑆 ↦ (𝑀‘𝑦)) ↾ 𝑥) = (𝑦 ∈ 𝑥 ↦ (𝑀‘𝑦))) | 
| 71 |  | snssi 4808 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (∅
∈ 𝑥 → {∅}
⊆ 𝑥) | 
| 72 |  | ssequn2 4189 | . . . . . . . . . . . . . . . . . . . . 21
⊢
({∅} ⊆ 𝑥
↔ (𝑥 ∪ {∅})
= 𝑥) | 
| 73 | 71, 72 | sylib 218 | . . . . . . . . . . . . . . . . . . . 20
⊢ (∅
∈ 𝑥 → (𝑥 ∪ {∅}) = 𝑥) | 
| 74 | 73 | eqcomd 2743 | . . . . . . . . . . . . . . . . . . 19
⊢ (∅
∈ 𝑥 → 𝑥 = (𝑥 ∪ {∅})) | 
| 75 | 74 | mpteq1d 5237 | . . . . . . . . . . . . . . . . . 18
⊢ (∅
∈ 𝑥 → (𝑦 ∈ 𝑥 ↦ (𝑀‘𝑦)) = (𝑦 ∈ (𝑥 ∪ {∅}) ↦ (𝑀‘𝑦))) | 
| 76 | 75 | adantl 481 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) ∧ ∅ ∈ 𝑥) → (𝑦 ∈ 𝑥 ↦ (𝑀‘𝑦)) = (𝑦 ∈ (𝑥 ∪ {∅}) ↦ (𝑀‘𝑦))) | 
| 77 | 68, 70, 76 | 3eqtrd 2781 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) ∧ ∅ ∈ 𝑥) → (𝑀 ↾ 𝑥) = (𝑦 ∈ (𝑥 ∪ {∅}) ↦ (𝑀‘𝑦))) | 
| 78 | 77 | fveq2d 6910 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) ∧ ∅ ∈ 𝑥) →
(Σ^‘(𝑀 ↾ 𝑥)) =
(Σ^‘(𝑦 ∈ (𝑥 ∪ {∅}) ↦ (𝑀‘𝑦)))) | 
| 79 |  | nfv 1914 | . . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑦((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) ∧ ¬ ∅ ∈ 𝑥) | 
| 80 |  | simplr 769 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) ∧ ¬ ∅ ∈ 𝑥) → 𝑥 ∈ 𝒫 dom 𝑀) | 
| 81 |  | p0ex 5384 | . . . . . . . . . . . . . . . . . 18
⊢ {∅}
∈ V | 
| 82 | 81 | a1i 11 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) ∧ ¬ ∅ ∈ 𝑥) → {∅} ∈
V) | 
| 83 |  | disjsn 4711 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∩ {∅}) = ∅
↔ ¬ ∅ ∈ 𝑥) | 
| 84 | 83 | biimpri 228 | . . . . . . . . . . . . . . . . . 18
⊢ (¬
∅ ∈ 𝑥 →
(𝑥 ∩ {∅}) =
∅) | 
| 85 | 84 | adantl 481 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) ∧ ¬ ∅ ∈ 𝑥) → (𝑥 ∩ {∅}) = ∅) | 
| 86 | 1 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) ∧ 𝑦 ∈ 𝑥) → 𝑀:𝑆⟶(0[,]+∞)) | 
| 87 | 51 | sselda 3983 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝑆) | 
| 88 | 86, 87 | ffvelcdmd 7105 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) ∧ 𝑦 ∈ 𝑥) → (𝑀‘𝑦) ∈ (0[,]+∞)) | 
| 89 | 88 | adantlr 715 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) ∧ ¬ ∅ ∈ 𝑥) ∧ 𝑦 ∈ 𝑥) → (𝑀‘𝑦) ∈ (0[,]+∞)) | 
| 90 |  | elsni 4643 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈ {∅} → 𝑦 = ∅) | 
| 91 | 90 | fveq2d 6910 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ {∅} → (𝑀‘𝑦) = (𝑀‘∅)) | 
| 92 | 91 | adantl 481 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑦 ∈ {∅}) → (𝑀‘𝑦) = (𝑀‘∅)) | 
| 93 | 1, 53 | ffvelcdmd 7105 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑀‘∅) ∈
(0[,]+∞)) | 
| 94 | 93 | adantr 480 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑦 ∈ {∅}) → (𝑀‘∅) ∈
(0[,]+∞)) | 
| 95 | 92, 94 | eqeltrd 2841 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑦 ∈ {∅}) → (𝑀‘𝑦) ∈ (0[,]+∞)) | 
| 96 | 95 | ad4ant14 752 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) ∧ ¬ ∅ ∈ 𝑥) ∧ 𝑦 ∈ {∅}) → (𝑀‘𝑦) ∈ (0[,]+∞)) | 
| 97 | 79, 80, 82, 85, 89, 96 | sge0splitmpt 46426 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) ∧ ¬ ∅ ∈ 𝑥) →
(Σ^‘(𝑦 ∈ (𝑥 ∪ {∅}) ↦ (𝑀‘𝑦))) =
((Σ^‘(𝑦 ∈ 𝑥 ↦ (𝑀‘𝑦))) +𝑒
(Σ^‘(𝑦 ∈ {∅} ↦ (𝑀‘𝑦))))) | 
| 98 |  | fveq2 6906 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 = ∅ → (𝑀‘𝑦) = (𝑀‘∅)) | 
| 99 | 98 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑦 = ∅) → (𝑀‘𝑦) = (𝑀‘∅)) | 
| 100 | 8 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑦 = ∅) → (𝑀‘∅) = 0) | 
| 101 | 99, 100 | eqtrd 2777 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑦 = ∅) → (𝑀‘𝑦) = 0) | 
| 102 | 90, 101 | sylan2 593 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑦 ∈ {∅}) → (𝑀‘𝑦) = 0) | 
| 103 | 102 | mpteq2dva 5242 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑦 ∈ {∅} ↦ (𝑀‘𝑦)) = (𝑦 ∈ {∅} ↦
0)) | 
| 104 | 103 | fveq2d 6910 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 →
(Σ^‘(𝑦 ∈ {∅} ↦ (𝑀‘𝑦))) =
(Σ^‘(𝑦 ∈ {∅} ↦
0))) | 
| 105 |  | nfv 1914 | . . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑦𝜑 | 
| 106 | 81 | a1i 11 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → {∅} ∈
V) | 
| 107 | 105, 106 | sge0z 46390 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 →
(Σ^‘(𝑦 ∈ {∅} ↦ 0)) =
0) | 
| 108 | 104, 107 | eqtrd 2777 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 →
(Σ^‘(𝑦 ∈ {∅} ↦ (𝑀‘𝑦))) = 0) | 
| 109 | 108 | oveq2d 7447 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 →
((Σ^‘(𝑦 ∈ 𝑥 ↦ (𝑀‘𝑦))) +𝑒
(Σ^‘(𝑦 ∈ {∅} ↦ (𝑀‘𝑦)))) =
((Σ^‘(𝑦 ∈ 𝑥 ↦ (𝑀‘𝑦))) +𝑒
0)) | 
| 110 | 109 | ad2antrr 726 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) ∧ ¬ ∅ ∈ 𝑥) →
((Σ^‘(𝑦 ∈ 𝑥 ↦ (𝑀‘𝑦))) +𝑒
(Σ^‘(𝑦 ∈ {∅} ↦ (𝑀‘𝑦)))) =
((Σ^‘(𝑦 ∈ 𝑥 ↦ (𝑀‘𝑦))) +𝑒
0)) | 
| 111 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) → 𝑥 ∈ 𝒫 dom 𝑀) | 
| 112 | 67, 69 | eqtrd 2777 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) → (𝑀 ↾ 𝑥) = (𝑦 ∈ 𝑥 ↦ (𝑀‘𝑦))) | 
| 113 | 1 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) → 𝑀:𝑆⟶(0[,]+∞)) | 
| 114 | 113, 51 | fssresd 6775 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) → (𝑀 ↾ 𝑥):𝑥⟶(0[,]+∞)) | 
| 115 | 112, 114 | feq1dd 6721 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) → (𝑦 ∈ 𝑥 ↦ (𝑀‘𝑦)):𝑥⟶(0[,]+∞)) | 
| 116 | 111, 115 | sge0xrcl 46400 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) →
(Σ^‘(𝑦 ∈ 𝑥 ↦ (𝑀‘𝑦))) ∈
ℝ*) | 
| 117 | 116 | xaddridd 13285 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) →
((Σ^‘(𝑦 ∈ 𝑥 ↦ (𝑀‘𝑦))) +𝑒 0) =
(Σ^‘(𝑦 ∈ 𝑥 ↦ (𝑀‘𝑦)))) | 
| 118 | 112 | fveq2d 6910 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) →
(Σ^‘(𝑀 ↾ 𝑥)) =
(Σ^‘(𝑦 ∈ 𝑥 ↦ (𝑀‘𝑦)))) | 
| 119 | 118 | eqcomd 2743 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) →
(Σ^‘(𝑦 ∈ 𝑥 ↦ (𝑀‘𝑦))) =
(Σ^‘(𝑀 ↾ 𝑥))) | 
| 120 | 117, 119 | eqtrd 2777 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) →
((Σ^‘(𝑦 ∈ 𝑥 ↦ (𝑀‘𝑦))) +𝑒 0) =
(Σ^‘(𝑀 ↾ 𝑥))) | 
| 121 | 120 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) ∧ ¬ ∅ ∈ 𝑥) →
((Σ^‘(𝑦 ∈ 𝑥 ↦ (𝑀‘𝑦))) +𝑒 0) =
(Σ^‘(𝑀 ↾ 𝑥))) | 
| 122 | 97, 110, 121 | 3eqtrrd 2782 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) ∧ ¬ ∅ ∈ 𝑥) →
(Σ^‘(𝑀 ↾ 𝑥)) =
(Σ^‘(𝑦 ∈ (𝑥 ∪ {∅}) ↦ (𝑀‘𝑦)))) | 
| 123 | 78, 122 | pm2.61dan 813 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) →
(Σ^‘(𝑀 ↾ 𝑥)) =
(Σ^‘(𝑦 ∈ (𝑥 ∪ {∅}) ↦ (𝑀‘𝑦)))) | 
| 124 | 123 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) ∧ 𝑒:ℕ–onto→(𝑥 ∪ {∅})) ∧ Disj 𝑛 ∈ ℕ (𝑒‘𝑛)) →
(Σ^‘(𝑀 ↾ 𝑥)) =
(Σ^‘(𝑦 ∈ (𝑥 ∪ {∅}) ↦ (𝑀‘𝑦)))) | 
| 125 |  | nfv 1914 | . . . . . . . . . . . . . 14
⊢
Ⅎ𝑦(((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) ∧ 𝑒:ℕ–onto→(𝑥 ∪ {∅})) ∧ Disj 𝑛 ∈ ℕ (𝑒‘𝑛)) | 
| 126 |  | nfv 1914 | . . . . . . . . . . . . . . 15
⊢
Ⅎ𝑛((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) ∧ 𝑒:ℕ–onto→(𝑥 ∪ {∅})) | 
| 127 |  | nfdisj1 5124 | . . . . . . . . . . . . . . 15
⊢
Ⅎ𝑛Disj
𝑛 ∈ ℕ (𝑒‘𝑛) | 
| 128 | 126, 127 | nfan 1899 | . . . . . . . . . . . . . 14
⊢
Ⅎ𝑛(((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) ∧ 𝑒:ℕ–onto→(𝑥 ∪ {∅})) ∧ Disj 𝑛 ∈ ℕ (𝑒‘𝑛)) | 
| 129 |  | fveq2 6906 | . . . . . . . . . . . . . 14
⊢ (𝑦 = (𝑒‘𝑛) → (𝑀‘𝑦) = (𝑀‘(𝑒‘𝑛))) | 
| 130 |  | nnex 12272 | . . . . . . . . . . . . . . 15
⊢ ℕ
∈ V | 
| 131 | 130 | a1i 11 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) ∧ 𝑒:ℕ–onto→(𝑥 ∪ {∅})) ∧ Disj 𝑛 ∈ ℕ (𝑒‘𝑛)) → ℕ ∈ V) | 
| 132 |  | simplr 769 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) ∧ 𝑒:ℕ–onto→(𝑥 ∪ {∅})) ∧ Disj 𝑛 ∈ ℕ (𝑒‘𝑛)) → 𝑒:ℕ–onto→(𝑥 ∪ {∅})) | 
| 133 |  | eqidd 2738 | . . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) ∧ 𝑒:ℕ–onto→(𝑥 ∪ {∅})) ∧ Disj 𝑛 ∈ ℕ (𝑒‘𝑛)) ∧ 𝑛 ∈ ℕ) → (𝑒‘𝑛) = (𝑒‘𝑛)) | 
| 134 | 1 | ad2antrr 726 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) ∧ 𝑦 ∈ (𝑥 ∪ {∅})) → 𝑀:𝑆⟶(0[,]+∞)) | 
| 135 | 57 | sselda 3983 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) ∧ 𝑦 ∈ (𝑥 ∪ {∅})) → 𝑦 ∈ 𝑆) | 
| 136 | 134, 135 | ffvelcdmd 7105 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) ∧ 𝑦 ∈ (𝑥 ∪ {∅})) → (𝑀‘𝑦) ∈ (0[,]+∞)) | 
| 137 | 136 | ad4ant14 752 | . . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) ∧ 𝑒:ℕ–onto→(𝑥 ∪ {∅})) ∧ Disj 𝑛 ∈ ℕ (𝑒‘𝑛)) ∧ 𝑦 ∈ (𝑥 ∪ {∅})) → (𝑀‘𝑦) ∈ (0[,]+∞)) | 
| 138 | 45, 101 | sylan 580 | . . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) ∧ 𝑒:ℕ–onto→(𝑥 ∪ {∅})) ∧ Disj 𝑛 ∈ ℕ (𝑒‘𝑛)) ∧ 𝑦 = ∅) → (𝑀‘𝑦) = 0) | 
| 139 | 125, 128,
129, 131, 132, 61, 133, 137, 138 | sge0fodjrn 46432 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) ∧ 𝑒:ℕ–onto→(𝑥 ∪ {∅})) ∧ Disj 𝑛 ∈ ℕ (𝑒‘𝑛)) →
(Σ^‘(𝑦 ∈ (𝑥 ∪ {∅}) ↦ (𝑀‘𝑦))) =
(Σ^‘(𝑛 ∈ ℕ ↦ (𝑀‘(𝑒‘𝑛))))) | 
| 140 | 124, 139 | eqtr2d 2778 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) ∧ 𝑒:ℕ–onto→(𝑥 ∪ {∅})) ∧ Disj 𝑛 ∈ ℕ (𝑒‘𝑛)) →
(Σ^‘(𝑛 ∈ ℕ ↦ (𝑀‘(𝑒‘𝑛)))) =
(Σ^‘(𝑀 ↾ 𝑥))) | 
| 141 | 140 | adantllr 719 | . . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) ∧ Disj 𝑦 ∈ 𝑥 𝑦) ∧ 𝑒:ℕ–onto→(𝑥 ∪ {∅})) ∧ Disj 𝑛 ∈ ℕ (𝑒‘𝑛)) →
(Σ^‘(𝑛 ∈ ℕ ↦ (𝑀‘(𝑒‘𝑛)))) =
(Σ^‘(𝑀 ↾ 𝑥))) | 
| 142 | 44, 64, 141 | 3eqtrd 2781 | . . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) ∧ Disj 𝑦 ∈ 𝑥 𝑦) ∧ 𝑒:ℕ–onto→(𝑥 ∪ {∅})) ∧ Disj 𝑛 ∈ ℕ (𝑒‘𝑛)) → (𝑀‘∪ 𝑥) =
(Σ^‘(𝑀 ↾ 𝑥))) | 
| 143 | 39, 40, 41, 142 | syl21anc 838 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) ∧ Disj 𝑦 ∈ 𝑥 𝑦) ∧ (𝑒:ℕ–onto→(𝑥 ∪ {∅}) ∧ Disj 𝑛 ∈ ℕ (𝑒‘𝑛))) → (𝑀‘∪ 𝑥) =
(Σ^‘(𝑀 ↾ 𝑥))) | 
| 144 | 143 | ex 412 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ((𝑒:ℕ–onto→(𝑥 ∪ {∅}) ∧ Disj 𝑛 ∈ ℕ (𝑒‘𝑛)) → (𝑀‘∪ 𝑥) =
(Σ^‘(𝑀 ↾ 𝑥)))) | 
| 145 | 144 | exlimdv 1933 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (∃𝑒(𝑒:ℕ–onto→(𝑥 ∪ {∅}) ∧ Disj 𝑛 ∈ ℕ (𝑒‘𝑛)) → (𝑀‘∪ 𝑥) =
(Σ^‘(𝑀 ↾ 𝑥)))) | 
| 146 | 29, 38, 145 | sylc 65 | . . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) ∧ (𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦)) ∧ ¬ 𝑥 = ∅) → (𝑀‘∪ 𝑥) =
(Σ^‘(𝑀 ↾ 𝑥))) | 
| 147 | 26, 146 | pm2.61dan 813 | . . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) ∧ (𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦)) → (𝑀‘∪ 𝑥) =
(Σ^‘(𝑀 ↾ 𝑥))) | 
| 148 | 147 | ex 412 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 dom 𝑀) → ((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) =
(Σ^‘(𝑀 ↾ 𝑥)))) | 
| 149 | 148 | ralrimiva 3146 | . . 3
⊢ (𝜑 → ∀𝑥 ∈ 𝒫 dom 𝑀((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) =
(Σ^‘(𝑀 ↾ 𝑥)))) | 
| 150 | 7, 8, 149 | jca31 514 | . 2
⊢ (𝜑 → (((𝑀:dom 𝑀⟶(0[,]+∞) ∧ dom 𝑀 ∈ SAlg) ∧ (𝑀‘∅) = 0) ∧
∀𝑥 ∈ 𝒫
dom 𝑀((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) =
(Σ^‘(𝑀 ↾ 𝑥))))) | 
| 151 |  | ismea 46466 | . 2
⊢ (𝑀 ∈ Meas ↔ (((𝑀:dom 𝑀⟶(0[,]+∞) ∧ dom 𝑀 ∈ SAlg) ∧ (𝑀‘∅) = 0) ∧
∀𝑥 ∈ 𝒫
dom 𝑀((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) =
(Σ^‘(𝑀 ↾ 𝑥))))) | 
| 152 | 150, 151 | sylibr 234 | 1
⊢ (𝜑 → 𝑀 ∈ Meas) |