Step |
Hyp |
Ref |
Expression |
1 |
|
measvunilem.0.1 |
⊢ Ⅎ 𝑥 𝐴 |
2 |
|
simp3l |
⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ { ∅ } ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) ) → 𝐴 ≼ ω ) |
3 |
|
ctex |
⊢ ( 𝐴 ≼ ω → 𝐴 ∈ V ) |
4 |
1
|
esum0 |
⊢ ( 𝐴 ∈ V → Σ* 𝑥 ∈ 𝐴 0 = 0 ) |
5 |
2 3 4
|
3syl |
⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ { ∅ } ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) ) → Σ* 𝑥 ∈ 𝐴 0 = 0 ) |
6 |
|
nfv |
⊢ Ⅎ 𝑥 𝑀 ∈ ( measures ‘ 𝑆 ) |
7 |
|
nfra1 |
⊢ Ⅎ 𝑥 ∀ 𝑥 ∈ 𝐴 𝐵 ∈ { ∅ } |
8 |
|
nfcv |
⊢ Ⅎ 𝑥 ≼ |
9 |
|
nfcv |
⊢ Ⅎ 𝑥 ω |
10 |
1 8 9
|
nfbr |
⊢ Ⅎ 𝑥 𝐴 ≼ ω |
11 |
|
nfdisj1 |
⊢ Ⅎ 𝑥 Disj 𝑥 ∈ 𝐴 𝐵 |
12 |
10 11
|
nfan |
⊢ Ⅎ 𝑥 ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) |
13 |
6 7 12
|
nf3an |
⊢ Ⅎ 𝑥 ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ { ∅ } ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) ) |
14 |
|
eqidd |
⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ { ∅ } ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) ) → 𝐴 = 𝐴 ) |
15 |
|
simp2 |
⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ { ∅ } ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) ) → ∀ 𝑥 ∈ 𝐴 𝐵 ∈ { ∅ } ) |
16 |
15
|
r19.21bi |
⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ { ∅ } ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ { ∅ } ) |
17 |
|
elsni |
⊢ ( 𝐵 ∈ { ∅ } → 𝐵 = ∅ ) |
18 |
16 17
|
syl |
⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ { ∅ } ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝐵 = ∅ ) |
19 |
18
|
fveq2d |
⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ { ∅ } ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑀 ‘ 𝐵 ) = ( 𝑀 ‘ ∅ ) ) |
20 |
|
measvnul |
⊢ ( 𝑀 ∈ ( measures ‘ 𝑆 ) → ( 𝑀 ‘ ∅ ) = 0 ) |
21 |
20
|
3ad2ant1 |
⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ { ∅ } ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) ) → ( 𝑀 ‘ ∅ ) = 0 ) |
22 |
21
|
adantr |
⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ { ∅ } ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑀 ‘ ∅ ) = 0 ) |
23 |
19 22
|
eqtrd |
⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ { ∅ } ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑀 ‘ 𝐵 ) = 0 ) |
24 |
13 14 23
|
esumeq12dvaf |
⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ { ∅ } ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) ) → Σ* 𝑥 ∈ 𝐴 ( 𝑀 ‘ 𝐵 ) = Σ* 𝑥 ∈ 𝐴 0 ) |
25 |
13 1 1 14 18
|
iuneq12daf |
⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ { ∅ } ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) ) → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 ∅ ) |
26 |
|
iun0 |
⊢ ∪ 𝑥 ∈ 𝐴 ∅ = ∅ |
27 |
25 26
|
eqtrdi |
⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ { ∅ } ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) ) → ∪ 𝑥 ∈ 𝐴 𝐵 = ∅ ) |
28 |
27
|
fveq2d |
⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ { ∅ } ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) ) → ( 𝑀 ‘ ∪ 𝑥 ∈ 𝐴 𝐵 ) = ( 𝑀 ‘ ∅ ) ) |
29 |
28 21
|
eqtrd |
⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ { ∅ } ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) ) → ( 𝑀 ‘ ∪ 𝑥 ∈ 𝐴 𝐵 ) = 0 ) |
30 |
5 24 29
|
3eqtr4rd |
⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ { ∅ } ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) ) → ( 𝑀 ‘ ∪ 𝑥 ∈ 𝐴 𝐵 ) = Σ* 𝑥 ∈ 𝐴 ( 𝑀 ‘ 𝐵 ) ) |