Metamath Proof Explorer

Theorem measvunilem

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

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

Proof

Step Hyp Ref Expression
1 measvunilem.1 ⊢ Ⅎ 𝑥 𝐴
2 simp1 ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) ) → 𝑀 ∈ ( measures ‘ 𝑆 ) )
3 simp3l ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) ) → 𝐴 ≼ ω )
4 1 abrexctf ⊢ ( 𝐴 ≼ ω → { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ≼ ω )
5 3 4 syl ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) ) → { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ≼ ω )
6 ctex ⊢ ( { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ≼ ω → { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ∈ V )
7 5 6 syl ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) ) → { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ∈ V )
8 simp2 ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) ) → ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) )
9 eldifi ⊢ ( 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) → 𝐵 ∈ 𝑆 )
10 9 ralimi ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) → ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑆 )
11 nfcv ⊢ Ⅎ 𝑥 𝑆
12 11 abrexss ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑆 → { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ⊆ 𝑆 )
13 10 12 syl ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) → { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ⊆ 𝑆 )
14 8 13 syl ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) ) → { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ⊆ 𝑆 )
15 elpwg ⊢ ( { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ∈ V → ( { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ∈ 𝒫 𝑆 ↔ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ⊆ 𝑆 ) )
16 15 biimpar ⊢ ( ( { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ∈ V ∧ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ⊆ 𝑆 ) → { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ∈ 𝒫 𝑆 )
17 7 14 16 syl2anc ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) ) → { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ∈ 𝒫 𝑆 )
18 simp3r ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) ) → Disj 𝑥 ∈ 𝐴 𝐵 )
19 1 disjabrexf ⊢ ( Disj 𝑥 ∈ 𝐴 𝐵 → Disj 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } 𝑧 )
20 18 19 syl ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) ) → Disj 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } 𝑧 )
21 measvun ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ∈ 𝒫 𝑆 ∧ ( { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ≼ ω ∧ Disj 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } 𝑧 ) ) → ( 𝑀 ‘ ∪ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ) = Σ* 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ( 𝑀 ‘ 𝑧 ) )
22 2 17 5 20 21 syl112anc ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) ) → ( 𝑀 ‘ ∪ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ) = Σ* 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ( 𝑀 ‘ 𝑧 ) )
23 dfiun2g ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } )
24 23 fveq2d ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) → ( 𝑀 ‘ ∪ 𝑥 ∈ 𝐴 𝐵 ) = ( 𝑀 ‘ ∪ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ) )
25 8 24 syl ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) ) → ( 𝑀 ‘ ∪ 𝑥 ∈ 𝐴 𝐵 ) = ( 𝑀 ‘ ∪ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ) )
26 nfcv ⊢ Ⅎ 𝑥 ( 𝑀 ‘ 𝑧 )
27 nfv ⊢ Ⅎ 𝑥 𝑀 ∈ ( measures ‘ 𝑆 )
28 nfra1 ⊢ Ⅎ 𝑥 ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( 𝑆 ∖ { ∅ } )
29 nfcv ⊢ Ⅎ 𝑥 ≼
30 nfcv ⊢ Ⅎ 𝑥 ω
31 1 29 30 nfbr ⊢ Ⅎ 𝑥 𝐴 ≼ ω
32 nfdisj1 ⊢ Ⅎ 𝑥 Disj 𝑥 ∈ 𝐴 𝐵
33 31 32 nfan ⊢ Ⅎ 𝑥 ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 )
34 27 28 33 nf3an ⊢ Ⅎ 𝑥 ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) )
35 fveq2 ⊢ ( 𝑧 = 𝐵 → ( 𝑀 ‘ 𝑧 ) = ( 𝑀 ‘ 𝐵 ) )
36 ctex ⊢ ( 𝐴 ≼ ω → 𝐴 ∈ V )
37 3 36 syl ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) ) → 𝐴 ∈ V )
38 8 r19.21bi ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) )
39 34 1 38 18 disjdsct ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) ) → Fun ◡ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
40 simpl1 ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑀 ∈ ( measures ‘ 𝑆 ) )
41 measvxrge0 ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐵 ∈ 𝑆 ) → ( 𝑀 ‘ 𝐵 ) ∈ ( 0 [,] +∞ ) )
42 9 41 sylan2 ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) ) → ( 𝑀 ‘ 𝐵 ) ∈ ( 0 [,] +∞ ) )
43 40 38 42 syl2anc ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑀 ‘ 𝐵 ) ∈ ( 0 [,] +∞ ) )
44 26 34 1 35 37 39 43 38 esumc ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) ) → Σ* 𝑥 ∈ 𝐴 ( 𝑀 ‘ 𝐵 ) = Σ* 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ( 𝑀 ‘ 𝑧 ) )
45 22 25 44 3eqtr4d ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) ) → ( 𝑀 ‘ ∪ 𝑥 ∈ 𝐴 𝐵 ) = Σ* 𝑥 ∈ 𝐴 ( 𝑀 ‘ 𝐵 ) )