Metamath Proof Explorer


Theorem measinblem

Description: Lemma for measinb . (Contributed by Thierry Arnoux, 2-Jun-2017)

Ref Expression
Assertion measinblem M measures S A S B 𝒫 S B ω Disj x B x M B A = * x B M x A

Proof

Step Hyp Ref Expression
1 iunin1 x B x A = x B x A
2 uniiun B = x B x
3 2 ineq1i B A = x B x A
4 1 3 eqtr4i x B x A = B A
5 4 fveq2i M x B x A = M B A
6 simplll M measures S A S B 𝒫 S B ω Disj x B x M measures S
7 nfv x M measures S A S B 𝒫 S
8 nfv x B ω
9 nfdisj1 x Disj x B x
10 8 9 nfan x B ω Disj x B x
11 7 10 nfan x M measures S A S B 𝒫 S B ω Disj x B x
12 simp1ll M measures S A S B 𝒫 S B ω Disj x B x x B M measures S
13 measbase M measures S S ran sigAlgebra
14 12 13 syl M measures S A S B 𝒫 S B ω Disj x B x x B S ran sigAlgebra
15 simp3 M measures S A S B 𝒫 S B ω Disj x B x x B x B
16 simp1r M measures S A S B 𝒫 S B ω Disj x B x x B B 𝒫 S
17 elelpwi x B B 𝒫 S x S
18 15 16 17 syl2anc M measures S A S B 𝒫 S B ω Disj x B x x B x S
19 simp1lr M measures S A S B 𝒫 S B ω Disj x B x x B A S
20 inelsiga S ran sigAlgebra x S A S x A S
21 14 18 19 20 syl3anc M measures S A S B 𝒫 S B ω Disj x B x x B x A S
22 21 3expia M measures S A S B 𝒫 S B ω Disj x B x x B x A S
23 11 22 ralrimi M measures S A S B 𝒫 S B ω Disj x B x x B x A S
24 simprl M measures S A S B 𝒫 S B ω Disj x B x B ω
25 disjin Disj x B x Disj x B x A
26 25 ad2antll M measures S A S B 𝒫 S B ω Disj x B x Disj x B x A
27 measvuni M measures S x B x A S B ω Disj x B x A M x B x A = * x B M x A
28 6 23 24 26 27 syl112anc M measures S A S B 𝒫 S B ω Disj x B x M x B x A = * x B M x A
29 5 28 eqtr3id M measures S A S B 𝒫 S B ω Disj x B x M B A = * x B M x A