| Step | Hyp | Ref
| Expression |
| 1 | | elex 3501 |
. . 3
⊢ (𝑀 ∈ (measures‘𝑆) → 𝑀 ∈ V) |
| 2 | 1 | a1i 11 |
. 2
⊢ (𝑆 ∈ ∪ ran sigAlgebra → (𝑀 ∈ (measures‘𝑆) → 𝑀 ∈ V)) |
| 3 | | simp1 1137 |
. . 3
⊢ ((𝑀:𝑆⟶(0[,]+∞) ∧ (𝑀‘∅) = 0 ∧
∀𝑥 ∈ 𝒫
𝑆((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑀‘𝑦))) → 𝑀:𝑆⟶(0[,]+∞)) |
| 4 | | ovex 7464 |
. . . 4
⊢
(0[,]+∞) ∈ V |
| 5 | | fex2 7958 |
. . . . . 6
⊢ ((𝑀:𝑆⟶(0[,]+∞) ∧ 𝑆 ∈ ∪ ran sigAlgebra ∧ (0[,]+∞) ∈ V) →
𝑀 ∈
V) |
| 6 | 5 | 3expb 1121 |
. . . . 5
⊢ ((𝑀:𝑆⟶(0[,]+∞) ∧ (𝑆 ∈ ∪ ran sigAlgebra ∧ (0[,]+∞) ∈ V)) →
𝑀 ∈
V) |
| 7 | 6 | expcom 413 |
. . . 4
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ (0[,]+∞) ∈ V) →
(𝑀:𝑆⟶(0[,]+∞) → 𝑀 ∈ V)) |
| 8 | 4, 7 | mpan2 691 |
. . 3
⊢ (𝑆 ∈ ∪ ran sigAlgebra → (𝑀:𝑆⟶(0[,]+∞) → 𝑀 ∈ V)) |
| 9 | 3, 8 | syl5 34 |
. 2
⊢ (𝑆 ∈ ∪ ran sigAlgebra → ((𝑀:𝑆⟶(0[,]+∞) ∧ (𝑀‘∅) = 0 ∧
∀𝑥 ∈ 𝒫
𝑆((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑀‘𝑦))) → 𝑀 ∈ V)) |
| 10 | | df-meas 34197 |
. . . 4
⊢ measures
= (𝑠 ∈ ∪ ran sigAlgebra ↦ {𝑚 ∣ (𝑚:𝑠⟶(0[,]+∞) ∧ (𝑚‘∅) = 0 ∧
∀𝑥 ∈ 𝒫
𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑚‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑚‘𝑦)))}) |
| 11 | | vex 3484 |
. . . . . 6
⊢ 𝑠 ∈ V |
| 12 | | mapex 7963 |
. . . . . 6
⊢ ((𝑠 ∈ V ∧ (0[,]+∞)
∈ V) → {𝑚 ∣
𝑚:𝑠⟶(0[,]+∞)} ∈
V) |
| 13 | 11, 4, 12 | mp2an 692 |
. . . . 5
⊢ {𝑚 ∣ 𝑚:𝑠⟶(0[,]+∞)} ∈
V |
| 14 | | simp1 1137 |
. . . . . 6
⊢ ((𝑚:𝑠⟶(0[,]+∞) ∧ (𝑚‘∅) = 0 ∧
∀𝑥 ∈ 𝒫
𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑚‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑚‘𝑦))) → 𝑚:𝑠⟶(0[,]+∞)) |
| 15 | 14 | ss2abi 4067 |
. . . . 5
⊢ {𝑚 ∣ (𝑚:𝑠⟶(0[,]+∞) ∧ (𝑚‘∅) = 0 ∧
∀𝑥 ∈ 𝒫
𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑚‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑚‘𝑦)))} ⊆ {𝑚 ∣ 𝑚:𝑠⟶(0[,]+∞)} |
| 16 | 13, 15 | ssexi 5322 |
. . . 4
⊢ {𝑚 ∣ (𝑚:𝑠⟶(0[,]+∞) ∧ (𝑚‘∅) = 0 ∧
∀𝑥 ∈ 𝒫
𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑚‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑚‘𝑦)))} ∈ V |
| 17 | | simpr 484 |
. . . . . 6
⊢ ((𝑠 = 𝑆 ∧ 𝑚 = 𝑀) → 𝑚 = 𝑀) |
| 18 | | simpl 482 |
. . . . . 6
⊢ ((𝑠 = 𝑆 ∧ 𝑚 = 𝑀) → 𝑠 = 𝑆) |
| 19 | 17, 18 | feq12d 6724 |
. . . . 5
⊢ ((𝑠 = 𝑆 ∧ 𝑚 = 𝑀) → (𝑚:𝑠⟶(0[,]+∞) ↔ 𝑀:𝑆⟶(0[,]+∞))) |
| 20 | | fveq1 6905 |
. . . . . . 7
⊢ (𝑚 = 𝑀 → (𝑚‘∅) = (𝑀‘∅)) |
| 21 | 20 | eqeq1d 2739 |
. . . . . 6
⊢ (𝑚 = 𝑀 → ((𝑚‘∅) = 0 ↔ (𝑀‘∅) = 0)) |
| 22 | 21 | adantl 481 |
. . . . 5
⊢ ((𝑠 = 𝑆 ∧ 𝑚 = 𝑀) → ((𝑚‘∅) = 0 ↔ (𝑀‘∅) = 0)) |
| 23 | 18 | pweqd 4617 |
. . . . . 6
⊢ ((𝑠 = 𝑆 ∧ 𝑚 = 𝑀) → 𝒫 𝑠 = 𝒫 𝑆) |
| 24 | | fveq1 6905 |
. . . . . . . . 9
⊢ (𝑚 = 𝑀 → (𝑚‘∪ 𝑥) = (𝑀‘∪ 𝑥)) |
| 25 | | fveq1 6905 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑀 → (𝑚‘𝑦) = (𝑀‘𝑦)) |
| 26 | 25 | esumeq2sdv 34040 |
. . . . . . . . 9
⊢ (𝑚 = 𝑀 → Σ*𝑦 ∈ 𝑥(𝑚‘𝑦) = Σ*𝑦 ∈ 𝑥(𝑀‘𝑦)) |
| 27 | 24, 26 | eqeq12d 2753 |
. . . . . . . 8
⊢ (𝑚 = 𝑀 → ((𝑚‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑚‘𝑦) ↔ (𝑀‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑀‘𝑦))) |
| 28 | 27 | imbi2d 340 |
. . . . . . 7
⊢ (𝑚 = 𝑀 → (((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑚‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑚‘𝑦)) ↔ ((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑀‘𝑦)))) |
| 29 | 28 | adantl 481 |
. . . . . 6
⊢ ((𝑠 = 𝑆 ∧ 𝑚 = 𝑀) → (((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑚‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑚‘𝑦)) ↔ ((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑀‘𝑦)))) |
| 30 | 23, 29 | raleqbidv 3346 |
. . . . 5
⊢ ((𝑠 = 𝑆 ∧ 𝑚 = 𝑀) → (∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑚‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑚‘𝑦)) ↔ ∀𝑥 ∈ 𝒫 𝑆((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑀‘𝑦)))) |
| 31 | 19, 22, 30 | 3anbi123d 1438 |
. . . 4
⊢ ((𝑠 = 𝑆 ∧ 𝑚 = 𝑀) → ((𝑚:𝑠⟶(0[,]+∞) ∧ (𝑚‘∅) = 0 ∧
∀𝑥 ∈ 𝒫
𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑚‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑚‘𝑦))) ↔ (𝑀:𝑆⟶(0[,]+∞) ∧ (𝑀‘∅) = 0 ∧
∀𝑥 ∈ 𝒫
𝑆((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑀‘𝑦))))) |
| 32 | 10, 16, 31 | abfmpel 32665 |
. . 3
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑀 ∈ V) → (𝑀 ∈ (measures‘𝑆) ↔ (𝑀:𝑆⟶(0[,]+∞) ∧ (𝑀‘∅) = 0 ∧
∀𝑥 ∈ 𝒫
𝑆((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑀‘𝑦))))) |
| 33 | 32 | ex 412 |
. 2
⊢ (𝑆 ∈ ∪ ran sigAlgebra → (𝑀 ∈ V → (𝑀 ∈ (measures‘𝑆) ↔ (𝑀:𝑆⟶(0[,]+∞) ∧ (𝑀‘∅) = 0 ∧
∀𝑥 ∈ 𝒫
𝑆((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑀‘𝑦)))))) |
| 34 | 2, 9, 33 | pm5.21ndd 379 |
1
⊢ (𝑆 ∈ ∪ ran sigAlgebra → (𝑀 ∈ (measures‘𝑆) ↔ (𝑀:𝑆⟶(0[,]+∞) ∧ (𝑀‘∅) = 0 ∧
∀𝑥 ∈ 𝒫
𝑆((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑀‘𝑦))))) |