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 ⊢ Ⅎ _ x A
Assertion measvunilem ⊢ M ∈ measures ⁡ S ∧ ∀ x ∈ A B ∈ S ∖ ∅ ∧ A ≼ ω ∧ Disj x ∈ A B → M ⁡ ⋃ x ∈ A B = ∑ * x ∈ A M ⁡ B

Proof

Step Hyp Ref Expression
1 measvunilem.1 ⊢ Ⅎ _ x A
2 simp1 ⊢ M ∈ measures ⁡ S ∧ ∀ x ∈ A B ∈ S ∖ ∅ ∧ A ≼ ω ∧ Disj x ∈ A B → M ∈ measures ⁡ S
3 simp3l ⊢ M ∈ measures ⁡ S ∧ ∀ x ∈ A B ∈ S ∖ ∅ ∧ A ≼ ω ∧ Disj x ∈ A B → A ≼ ω
4 1 abrexctf ⊢ A ≼ ω → y | ∃ x ∈ A y = B ≼ ω
5 3 4 syl ⊢ M ∈ measures ⁡ S ∧ ∀ x ∈ A B ∈ S ∖ ∅ ∧ A ≼ ω ∧ Disj x ∈ A B → y | ∃ x ∈ A y = B ≼ ω
6 ctex ⊢ y | ∃ x ∈ A y = B ≼ ω → y | ∃ x ∈ A y = B ∈ V
7 5 6 syl ⊢ M ∈ measures ⁡ S ∧ ∀ x ∈ A B ∈ S ∖ ∅ ∧ A ≼ ω ∧ Disj x ∈ A B → y | ∃ x ∈ A y = B ∈ V
8 simp2 ⊢ M ∈ measures ⁡ S ∧ ∀ x ∈ A B ∈ S ∖ ∅ ∧ A ≼ ω ∧ Disj x ∈ A B → ∀ x ∈ A B ∈ S ∖ ∅
9 eldifi ⊢ B ∈ S ∖ ∅ → B ∈ S
10 9 ralimi ⊢ ∀ x ∈ A B ∈ S ∖ ∅ → ∀ x ∈ A B ∈ S
11 nfcv ⊢ Ⅎ _ x S
12 11 abrexss ⊢ ∀ x ∈ A B ∈ S → y | ∃ x ∈ A y = B ⊆ S
13 10 12 syl ⊢ ∀ x ∈ A B ∈ S ∖ ∅ → y | ∃ x ∈ A y = B ⊆ S
14 8 13 syl ⊢ M ∈ measures ⁡ S ∧ ∀ x ∈ A B ∈ S ∖ ∅ ∧ A ≼ ω ∧ Disj x ∈ A B → y | ∃ x ∈ A y = B ⊆ S
15 elpwg ⊢ y | ∃ x ∈ A y = B ∈ V → y | ∃ x ∈ A y = B ∈ 𝒫 S ↔ y | ∃ x ∈ A y = B ⊆ S
16 15 biimpar ⊢ y | ∃ x ∈ A y = B ∈ V ∧ y | ∃ x ∈ A y = B ⊆ S → y | ∃ x ∈ A y = B ∈ 𝒫 S
17 7 14 16 syl2anc ⊢ M ∈ measures ⁡ S ∧ ∀ x ∈ A B ∈ S ∖ ∅ ∧ A ≼ ω ∧ Disj x ∈ A B → y | ∃ x ∈ A y = B ∈ 𝒫 S
18 simp3r ⊢ M ∈ measures ⁡ S ∧ ∀ x ∈ A B ∈ S ∖ ∅ ∧ A ≼ ω ∧ Disj x ∈ A B → Disj x ∈ A B
19 1 disjabrexf ⊢ Disj x ∈ A B → Disj z ∈ y | ∃ x ∈ A y = B z
20 18 19 syl ⊢ M ∈ measures ⁡ S ∧ ∀ x ∈ A B ∈ S ∖ ∅ ∧ A ≼ ω ∧ Disj x ∈ A B → Disj z ∈ y | ∃ x ∈ A y = B z
21 measvun ⊢ M ∈ measures ⁡ S ∧ y | ∃ x ∈ A y = B ∈ 𝒫 S ∧ y | ∃ x ∈ A y = B ≼ ω ∧ Disj z ∈ y | ∃ x ∈ A y = B z → M ⁡ ⋃ y | ∃ x ∈ A y = B = ∑ * z ∈ y | ∃ x ∈ A y = B M ⁡ z
22 2 17 5 20 21 syl112anc ⊢ M ∈ measures ⁡ S ∧ ∀ x ∈ A B ∈ S ∖ ∅ ∧ A ≼ ω ∧ Disj x ∈ A B → M ⁡ ⋃ y | ∃ x ∈ A y = B = ∑ * z ∈ y | ∃ x ∈ A y = B M ⁡ z
23 dfiun2g ⊢ ∀ x ∈ A B ∈ S ∖ ∅ → ⋃ x ∈ A B = ⋃ y | ∃ x ∈ A y = B
24 23 fveq2d ⊢ ∀ x ∈ A B ∈ S ∖ ∅ → M ⁡ ⋃ x ∈ A B = M ⁡ ⋃ y | ∃ x ∈ A y = B
25 8 24 syl ⊢ M ∈ measures ⁡ S ∧ ∀ x ∈ A B ∈ S ∖ ∅ ∧ A ≼ ω ∧ Disj x ∈ A B → M ⁡ ⋃ x ∈ A B = M ⁡ ⋃ y | ∃ x ∈ A y = B
26 nfcv ⊢ Ⅎ _ x M ⁡ z
27 nfv ⊢ Ⅎ x M ∈ measures ⁡ S
28 nfra1 ⊢ Ⅎ x ∀ x ∈ A B ∈ S ∖ ∅
29 nfcv ⊢ Ⅎ _ x ≼
30 nfcv ⊢ Ⅎ _ x ω
31 1 29 30 nfbr ⊢ Ⅎ x A ≼ ω
32 nfdisj1 ⊢ Ⅎ x Disj x ∈ A B
33 31 32 nfan ⊢ Ⅎ x A ≼ ω ∧ Disj x ∈ A B
34 27 28 33 nf3an ⊢ Ⅎ x M ∈ measures ⁡ S ∧ ∀ x ∈ A B ∈ S ∖ ∅ ∧ A ≼ ω ∧ Disj x ∈ A B
35 fveq2 ⊢ z = B → M ⁡ z = M ⁡ B
36 ctex ⊢ A ≼ ω → A ∈ V
37 3 36 syl ⊢ M ∈ measures ⁡ S ∧ ∀ x ∈ A B ∈ S ∖ ∅ ∧ A ≼ ω ∧ Disj x ∈ A B → A ∈ V
38 8 r19.21bi ⊢ M ∈ measures ⁡ S ∧ ∀ x ∈ A B ∈ S ∖ ∅ ∧ A ≼ ω ∧ Disj x ∈ A B ∧ x ∈ A → B ∈ S ∖ ∅
39 34 1 38 18 disjdsct ⊢ M ∈ measures ⁡ S ∧ ∀ x ∈ A B ∈ S ∖ ∅ ∧ A ≼ ω ∧ Disj x ∈ A B → Fun ⁡ x ∈ A ⟼ B -1
40 simpl1 ⊢ M ∈ measures ⁡ S ∧ ∀ x ∈ A B ∈ S ∖ ∅ ∧ A ≼ ω ∧ Disj x ∈ A B ∧ x ∈ A → M ∈ measures ⁡ S
41 measvxrge0 ⊢ M ∈ measures ⁡ S ∧ B ∈ S → M ⁡ B ∈ 0 +∞
42 9 41 sylan2 ⊢ M ∈ measures ⁡ S ∧ B ∈ S ∖ ∅ → M ⁡ B ∈ 0 +∞
43 40 38 42 syl2anc ⊢ M ∈ measures ⁡ S ∧ ∀ x ∈ A B ∈ S ∖ ∅ ∧ A ≼ ω ∧ Disj x ∈ A B ∧ x ∈ A → M ⁡ B ∈ 0 +∞
44 26 34 1 35 37 39 43 38 esumc ⊢ M ∈ measures ⁡ S ∧ ∀ x ∈ A B ∈ S ∖ ∅ ∧ A ≼ ω ∧ Disj x ∈ A B → ∑ * x ∈ A M ⁡ B = ∑ * z ∈ y | ∃ x ∈ A y = B M ⁡ z
45 22 25 44 3eqtr4d ⊢ M ∈ measures ⁡ S ∧ ∀ x ∈ A B ∈ S ∖ ∅ ∧ A ≼ ω ∧ Disj x ∈ A B → M ⁡ ⋃ x ∈ A B = ∑ * x ∈ A M ⁡ B