Theorem measvunilem0

Description: Lemma for measvuni . (Contributed by Thierry Arnoux, 6-Mar-2017)

	Ref	Expression
Hypothesis	measvunilem.0.1	⊢ Ⅎ 𝑥 𝐴
Assertion	measvunilem0	⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ { ∅ } ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) ) → ( 𝑀 ‘ ∪ 𝑥 ∈ 𝐴 𝐵 ) = Σ* 𝑥 ∈ 𝐴 ( 𝑀 ‘ 𝐵 ) )

Proof

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 𝑥 ∈ 𝐴 𝐵 ) ) → ( 𝑀 ‘ ∪ 𝑥 ∈ 𝐴 𝐵 ) = Σ* 𝑥 ∈ 𝐴 ( 𝑀 ‘ 𝐵 ) )