| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | df-meas 34198 | . . . 4
⊢ measures
= (𝑠 ∈ ∪ ran sigAlgebra ↦ {𝑚 ∣ (𝑚:𝑠⟶(0[,]+∞) ∧ (𝑚‘∅) = 0 ∧
∀𝑥 ∈ 𝒫
𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑚‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑚‘𝑦)))}) | 
| 2 |  | vex 3483 | . . . . . 6
⊢ 𝑠 ∈ V | 
| 3 |  | ovex 7465 | . . . . . 6
⊢
(0[,]+∞) ∈ V | 
| 4 |  | mapex 7964 | . . . . . 6
⊢ ((𝑠 ∈ V ∧ (0[,]+∞)
∈ V) → {𝑚 ∣
𝑚:𝑠⟶(0[,]+∞)} ∈
V) | 
| 5 | 2, 3, 4 | mp2an 692 | . . . . 5
⊢ {𝑚 ∣ 𝑚:𝑠⟶(0[,]+∞)} ∈
V | 
| 6 |  | simp1 1136 | . . . . . 6
⊢ ((𝑚:𝑠⟶(0[,]+∞) ∧ (𝑚‘∅) = 0 ∧
∀𝑥 ∈ 𝒫
𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑚‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑚‘𝑦))) → 𝑚:𝑠⟶(0[,]+∞)) | 
| 7 | 6 | ss2abi 4066 | . . . . 5
⊢ {𝑚 ∣ (𝑚:𝑠⟶(0[,]+∞) ∧ (𝑚‘∅) = 0 ∧
∀𝑥 ∈ 𝒫
𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑚‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑚‘𝑦)))} ⊆ {𝑚 ∣ 𝑚:𝑠⟶(0[,]+∞)} | 
| 8 | 5, 7 | ssexi 5321 | . . . 4
⊢ {𝑚 ∣ (𝑚:𝑠⟶(0[,]+∞) ∧ (𝑚‘∅) = 0 ∧
∀𝑥 ∈ 𝒫
𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑚‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑚‘𝑦)))} ∈ V | 
| 9 |  | feq1 6715 | . . . . 5
⊢ (𝑚 = 𝑀 → (𝑚:𝑠⟶(0[,]+∞) ↔ 𝑀:𝑠⟶(0[,]+∞))) | 
| 10 |  | fveq1 6904 | . . . . . 6
⊢ (𝑚 = 𝑀 → (𝑚‘∅) = (𝑀‘∅)) | 
| 11 | 10 | eqeq1d 2738 | . . . . 5
⊢ (𝑚 = 𝑀 → ((𝑚‘∅) = 0 ↔ (𝑀‘∅) = 0)) | 
| 12 |  | fveq1 6904 | . . . . . . . 8
⊢ (𝑚 = 𝑀 → (𝑚‘∪ 𝑥) = (𝑀‘∪ 𝑥)) | 
| 13 |  | fveq1 6904 | . . . . . . . . 9
⊢ (𝑚 = 𝑀 → (𝑚‘𝑦) = (𝑀‘𝑦)) | 
| 14 | 13 | esumeq2sdv 34041 | . . . . . . . 8
⊢ (𝑚 = 𝑀 → Σ*𝑦 ∈ 𝑥(𝑚‘𝑦) = Σ*𝑦 ∈ 𝑥(𝑀‘𝑦)) | 
| 15 | 12, 14 | eqeq12d 2752 | . . . . . . 7
⊢ (𝑚 = 𝑀 → ((𝑚‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑚‘𝑦) ↔ (𝑀‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑀‘𝑦))) | 
| 16 | 15 | imbi2d 340 | . . . . . 6
⊢ (𝑚 = 𝑀 → (((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑚‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑚‘𝑦)) ↔ ((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑀‘𝑦)))) | 
| 17 | 16 | ralbidv 3177 | . . . . 5
⊢ (𝑚 = 𝑀 → (∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑚‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑚‘𝑦)) ↔ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑀‘𝑦)))) | 
| 18 | 9, 11, 17 | 3anbi123d 1437 | . . . 4
⊢ (𝑚 = 𝑀 → ((𝑚:𝑠⟶(0[,]+∞) ∧ (𝑚‘∅) = 0 ∧
∀𝑥 ∈ 𝒫
𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑚‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑚‘𝑦))) ↔ (𝑀:𝑠⟶(0[,]+∞) ∧ (𝑀‘∅) = 0 ∧
∀𝑥 ∈ 𝒫
𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑀‘𝑦))))) | 
| 19 | 1, 8, 18 | abfmpunirn 32663 | . . 3
⊢ (𝑀 ∈ ∪ ran measures ↔ (𝑀 ∈ V ∧ ∃𝑠 ∈ ∪ ran
sigAlgebra(𝑀:𝑠⟶(0[,]+∞) ∧
(𝑀‘∅) = 0 ∧
∀𝑥 ∈ 𝒫
𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑀‘𝑦))))) | 
| 20 | 19 | simprbi 496 | . 2
⊢ (𝑀 ∈ ∪ ran measures → ∃𝑠 ∈ ∪ ran
sigAlgebra(𝑀:𝑠⟶(0[,]+∞) ∧
(𝑀‘∅) = 0 ∧
∀𝑥 ∈ 𝒫
𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑀‘𝑦)))) | 
| 21 |  | fdm 6744 | . . . . . . 7
⊢ (𝑀:𝑠⟶(0[,]+∞) → dom 𝑀 = 𝑠) | 
| 22 | 21 | 3ad2ant1 1133 | . . . . . 6
⊢ ((𝑀:𝑠⟶(0[,]+∞) ∧ (𝑀‘∅) = 0 ∧
∀𝑥 ∈ 𝒫
𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑀‘𝑦))) → dom 𝑀 = 𝑠) | 
| 23 | 22 | adantl 481 | . . . . 5
⊢ ((𝑠 ∈ ∪ ran sigAlgebra ∧ (𝑀:𝑠⟶(0[,]+∞) ∧ (𝑀‘∅) = 0 ∧
∀𝑥 ∈ 𝒫
𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑀‘𝑦)))) → dom 𝑀 = 𝑠) | 
| 24 |  | simpl 482 | . . . . 5
⊢ ((𝑠 ∈ ∪ ran sigAlgebra ∧ (𝑀:𝑠⟶(0[,]+∞) ∧ (𝑀‘∅) = 0 ∧
∀𝑥 ∈ 𝒫
𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑀‘𝑦)))) → 𝑠 ∈ ∪ ran
sigAlgebra) | 
| 25 | 23, 24 | eqeltrd 2840 | . . . 4
⊢ ((𝑠 ∈ ∪ ran sigAlgebra ∧ (𝑀:𝑠⟶(0[,]+∞) ∧ (𝑀‘∅) = 0 ∧
∀𝑥 ∈ 𝒫
𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑀‘𝑦)))) → dom 𝑀 ∈ ∪ ran
sigAlgebra) | 
| 26 |  | simp1 1136 | . . . . . . 7
⊢ ((𝑀:𝑠⟶(0[,]+∞) ∧ (𝑀‘∅) = 0 ∧
∀𝑥 ∈ 𝒫
𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑀‘𝑦))) → 𝑀:𝑠⟶(0[,]+∞)) | 
| 27 |  | feq2 6716 | . . . . . . . 8
⊢ (dom
𝑀 = 𝑠 → (𝑀:dom 𝑀⟶(0[,]+∞) ↔ 𝑀:𝑠⟶(0[,]+∞))) | 
| 28 | 27 | biimpar 477 | . . . . . . 7
⊢ ((dom
𝑀 = 𝑠 ∧ 𝑀:𝑠⟶(0[,]+∞)) → 𝑀:dom 𝑀⟶(0[,]+∞)) | 
| 29 | 22, 26, 28 | syl2anc 584 | . . . . . 6
⊢ ((𝑀:𝑠⟶(0[,]+∞) ∧ (𝑀‘∅) = 0 ∧
∀𝑥 ∈ 𝒫
𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑀‘𝑦))) → 𝑀:dom 𝑀⟶(0[,]+∞)) | 
| 30 |  | simp2 1137 | . . . . . 6
⊢ ((𝑀:𝑠⟶(0[,]+∞) ∧ (𝑀‘∅) = 0 ∧
∀𝑥 ∈ 𝒫
𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑀‘𝑦))) → (𝑀‘∅) = 0) | 
| 31 |  | simp3 1138 | . . . . . . 7
⊢ ((𝑀:𝑠⟶(0[,]+∞) ∧ (𝑀‘∅) = 0 ∧
∀𝑥 ∈ 𝒫
𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑀‘𝑦))) → ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑀‘𝑦))) | 
| 32 |  | pweq 4613 | . . . . . . . . 9
⊢ (dom
𝑀 = 𝑠 → 𝒫 dom 𝑀 = 𝒫 𝑠) | 
| 33 | 32 | raleqdv 3325 | . . . . . . . 8
⊢ (dom
𝑀 = 𝑠 → (∀𝑥 ∈ 𝒫 dom 𝑀((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑀‘𝑦)) ↔ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑀‘𝑦)))) | 
| 34 | 33 | biimpar 477 | . . . . . . 7
⊢ ((dom
𝑀 = 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑀‘𝑦))) → ∀𝑥 ∈ 𝒫 dom 𝑀((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑀‘𝑦))) | 
| 35 | 22, 31, 34 | syl2anc 584 | . . . . . 6
⊢ ((𝑀:𝑠⟶(0[,]+∞) ∧ (𝑀‘∅) = 0 ∧
∀𝑥 ∈ 𝒫
𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑀‘𝑦))) → ∀𝑥 ∈ 𝒫 dom 𝑀((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑀‘𝑦))) | 
| 36 | 29, 30, 35 | 3jca 1128 | . . . . 5
⊢ ((𝑀:𝑠⟶(0[,]+∞) ∧ (𝑀‘∅) = 0 ∧
∀𝑥 ∈ 𝒫
𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑀‘𝑦))) → (𝑀:dom 𝑀⟶(0[,]+∞) ∧ (𝑀‘∅) = 0 ∧
∀𝑥 ∈ 𝒫
dom 𝑀((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑀‘𝑦)))) | 
| 37 | 36 | adantl 481 | . . . 4
⊢ ((𝑠 ∈ ∪ ran sigAlgebra ∧ (𝑀:𝑠⟶(0[,]+∞) ∧ (𝑀‘∅) = 0 ∧
∀𝑥 ∈ 𝒫
𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑀‘𝑦)))) → (𝑀:dom 𝑀⟶(0[,]+∞) ∧ (𝑀‘∅) = 0 ∧
∀𝑥 ∈ 𝒫
dom 𝑀((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑀‘𝑦)))) | 
| 38 | 25, 37 | jca 511 | . . 3
⊢ ((𝑠 ∈ ∪ ran sigAlgebra ∧ (𝑀:𝑠⟶(0[,]+∞) ∧ (𝑀‘∅) = 0 ∧
∀𝑥 ∈ 𝒫
𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑀‘𝑦)))) → (dom 𝑀 ∈ ∪ ran
sigAlgebra ∧ (𝑀:dom
𝑀⟶(0[,]+∞)
∧ (𝑀‘∅) = 0
∧ ∀𝑥 ∈
𝒫 dom 𝑀((𝑥 ≼ ω ∧
Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑀‘𝑦))))) | 
| 39 | 38 | rexlimiva 3146 | . 2
⊢
(∃𝑠 ∈
∪ ran sigAlgebra(𝑀:𝑠⟶(0[,]+∞) ∧ (𝑀‘∅) = 0 ∧
∀𝑥 ∈ 𝒫
𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑀‘𝑦))) → (dom 𝑀 ∈ ∪ ran
sigAlgebra ∧ (𝑀:dom
𝑀⟶(0[,]+∞)
∧ (𝑀‘∅) = 0
∧ ∀𝑥 ∈
𝒫 dom 𝑀((𝑥 ≼ ω ∧
Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑀‘𝑦))))) | 
| 40 | 20, 39 | syl 17 | 1
⊢ (𝑀 ∈ ∪ ran measures → (dom 𝑀 ∈ ∪ ran
sigAlgebra ∧ (𝑀:dom
𝑀⟶(0[,]+∞)
∧ (𝑀‘∅) = 0
∧ ∀𝑥 ∈
𝒫 dom 𝑀((𝑥 ≼ ω ∧
Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑀‘𝑦))))) |