| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simp1 1136 | . . 3
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ (𝑆 ∖ {∅}) ∧ (𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵)) → 𝑀 ∈ (measures‘𝑆)) | 
| 2 |  | simp3l 1201 | . . . . . 6
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ (𝑆 ∖ {∅}) ∧ (𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵)) → 𝐴 ≼ ω) | 
| 3 |  | measvunilem.1 | . . . . . . 7
⊢
Ⅎ𝑥𝐴 | 
| 4 | 3 | abrexctf 32731 | . . . . . 6
⊢ (𝐴 ≼ ω → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ≼ ω) | 
| 5 | 2, 4 | syl 17 | . . . . 5
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ (𝑆 ∖ {∅}) ∧ (𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵)) → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ≼ ω) | 
| 6 |  | ctex 9005 | . . . . 5
⊢ ({𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ≼ ω → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ V) | 
| 7 | 5, 6 | syl 17 | . . . 4
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ (𝑆 ∖ {∅}) ∧ (𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵)) → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ V) | 
| 8 |  | simp2 1137 | . . . . 5
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ (𝑆 ∖ {∅}) ∧ (𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵)) → ∀𝑥 ∈ 𝐴 𝐵 ∈ (𝑆 ∖ {∅})) | 
| 9 |  | eldifi 4130 | . . . . . . 7
⊢ (𝐵 ∈ (𝑆 ∖ {∅}) → 𝐵 ∈ 𝑆) | 
| 10 | 9 | ralimi 3082 | . . . . . 6
⊢
(∀𝑥 ∈
𝐴 𝐵 ∈ (𝑆 ∖ {∅}) → ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑆) | 
| 11 |  | nfcv 2904 | . . . . . . 7
⊢
Ⅎ𝑥𝑆 | 
| 12 | 11 | abrexss 32532 | . . . . . 6
⊢
(∀𝑥 ∈
𝐴 𝐵 ∈ 𝑆 → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ⊆ 𝑆) | 
| 13 | 10, 12 | syl 17 | . . . . 5
⊢
(∀𝑥 ∈
𝐴 𝐵 ∈ (𝑆 ∖ {∅}) → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ⊆ 𝑆) | 
| 14 | 8, 13 | syl 17 | . . . 4
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ (𝑆 ∖ {∅}) ∧ (𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵)) → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ⊆ 𝑆) | 
| 15 |  | elpwg 4602 | . . . . 5
⊢ ({𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ V → ({𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ 𝒫 𝑆 ↔ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ⊆ 𝑆)) | 
| 16 | 15 | biimpar 477 | . . . 4
⊢ (({𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ V ∧ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ⊆ 𝑆) → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ 𝒫 𝑆) | 
| 17 | 7, 14, 16 | syl2anc 584 | . . 3
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ (𝑆 ∖ {∅}) ∧ (𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵)) → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ 𝒫 𝑆) | 
| 18 |  | simp3r 1202 | . . . 4
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ (𝑆 ∖ {∅}) ∧ (𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵)) → Disj 𝑥 ∈ 𝐴 𝐵) | 
| 19 | 3 | disjabrexf 32597 | . . . 4
⊢
(Disj 𝑥
∈ 𝐴 𝐵 → Disj 𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}𝑧) | 
| 20 | 18, 19 | syl 17 | . . 3
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ (𝑆 ∖ {∅}) ∧ (𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵)) → Disj 𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}𝑧) | 
| 21 |  | measvun 34211 | . . 3
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ 𝒫 𝑆 ∧ ({𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ≼ ω ∧ Disj 𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}𝑧)) → (𝑀‘∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}) = Σ*𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} (𝑀‘𝑧)) | 
| 22 | 1, 17, 5, 20, 21 | syl112anc 1375 | . 2
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ (𝑆 ∖ {∅}) ∧ (𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵)) → (𝑀‘∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}) = Σ*𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} (𝑀‘𝑧)) | 
| 23 |  | dfiun2g 5029 | . . . 4
⊢
(∀𝑥 ∈
𝐴 𝐵 ∈ (𝑆 ∖ {∅}) → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}) | 
| 24 | 23 | fveq2d 6909 | . . 3
⊢
(∀𝑥 ∈
𝐴 𝐵 ∈ (𝑆 ∖ {∅}) → (𝑀‘∪ 𝑥 ∈ 𝐴 𝐵) = (𝑀‘∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵})) | 
| 25 | 8, 24 | syl 17 | . 2
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ (𝑆 ∖ {∅}) ∧ (𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵)) → (𝑀‘∪
𝑥 ∈ 𝐴 𝐵) = (𝑀‘∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵})) | 
| 26 |  | nfcv 2904 | . . 3
⊢
Ⅎ𝑥(𝑀‘𝑧) | 
| 27 |  | nfv 1913 | . . . 4
⊢
Ⅎ𝑥 𝑀 ∈ (measures‘𝑆) | 
| 28 |  | nfra1 3283 | . . . 4
⊢
Ⅎ𝑥∀𝑥 ∈ 𝐴 𝐵 ∈ (𝑆 ∖ {∅}) | 
| 29 |  | nfcv 2904 | . . . . . 6
⊢
Ⅎ𝑥
≼ | 
| 30 |  | nfcv 2904 | . . . . . 6
⊢
Ⅎ𝑥ω | 
| 31 | 3, 29, 30 | nfbr 5189 | . . . . 5
⊢
Ⅎ𝑥 𝐴 ≼
ω | 
| 32 |  | nfdisj1 5123 | . . . . 5
⊢
Ⅎ𝑥Disj
𝑥 ∈ 𝐴 𝐵 | 
| 33 | 31, 32 | nfan 1898 | . . . 4
⊢
Ⅎ𝑥(𝐴 ≼ ω ∧
Disj 𝑥 ∈ 𝐴 𝐵) | 
| 34 | 27, 28, 33 | nf3an 1900 | . . 3
⊢
Ⅎ𝑥(𝑀 ∈ (measures‘𝑆) ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ (𝑆 ∖ {∅}) ∧ (𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵)) | 
| 35 |  | fveq2 6905 | . . 3
⊢ (𝑧 = 𝐵 → (𝑀‘𝑧) = (𝑀‘𝐵)) | 
| 36 |  | ctex 9005 | . . . 4
⊢ (𝐴 ≼ ω → 𝐴 ∈ V) | 
| 37 | 2, 36 | syl 17 | . . 3
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ (𝑆 ∖ {∅}) ∧ (𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵)) → 𝐴 ∈ V) | 
| 38 | 8 | r19.21bi 3250 | . . . 4
⊢ (((𝑀 ∈ (measures‘𝑆) ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ (𝑆 ∖ {∅}) ∧ (𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵)) ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ (𝑆 ∖ {∅})) | 
| 39 | 34, 3, 38, 18 | disjdsct 32713 | . . 3
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ (𝑆 ∖ {∅}) ∧ (𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵)) → Fun ◡(𝑥 ∈ 𝐴 ↦ 𝐵)) | 
| 40 |  | simpl1 1191 | . . . 4
⊢ (((𝑀 ∈ (measures‘𝑆) ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ (𝑆 ∖ {∅}) ∧ (𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵)) ∧ 𝑥 ∈ 𝐴) → 𝑀 ∈ (measures‘𝑆)) | 
| 41 |  | measvxrge0 34207 | . . . . 5
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝐵 ∈ 𝑆) → (𝑀‘𝐵) ∈ (0[,]+∞)) | 
| 42 | 9, 41 | sylan2 593 | . . . 4
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝐵 ∈ (𝑆 ∖ {∅})) → (𝑀‘𝐵) ∈ (0[,]+∞)) | 
| 43 | 40, 38, 42 | syl2anc 584 | . . 3
⊢ (((𝑀 ∈ (measures‘𝑆) ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ (𝑆 ∖ {∅}) ∧ (𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵)) ∧ 𝑥 ∈ 𝐴) → (𝑀‘𝐵) ∈ (0[,]+∞)) | 
| 44 | 26, 34, 3, 35, 37, 39, 43, 38 | esumc 34053 | . 2
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ (𝑆 ∖ {∅}) ∧ (𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵)) → Σ*𝑥 ∈ 𝐴(𝑀‘𝐵) = Σ*𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} (𝑀‘𝑧)) | 
| 45 | 22, 25, 44 | 3eqtr4d 2786 | 1
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ (𝑆 ∖ {∅}) ∧ (𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵)) → (𝑀‘∪
𝑥 ∈ 𝐴 𝐵) = Σ*𝑥 ∈ 𝐴(𝑀‘𝐵)) |