Metamath Proof Explorer

Theorem measvuni

Description: The measure of a countable disjoint union is the sum of the measures. This theorem uses a collection rather than a set of subsets of S . (Contributed by Thierry Arnoux, 7-Mar-2017)

Ref Expression
Assertion measvuni ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑆 ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) ) → ( 𝑀 ‘ ∪ 𝑥 ∈ 𝐴 𝐵 ) = Σ* 𝑥 ∈ 𝐴 ( 𝑀 ‘ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 simp1 ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑆 ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) ) → 𝑀 ∈ ( measures ‘ 𝑆 ) )
2 rabid ⊢ ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ { ∅ } } ↔ ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ { ∅ } ) )
3 2 simprbi ⊢ ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ { ∅ } } → 𝐵 ∈ { ∅ } )
4 3 adantl ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ { ∅ } } ) → 𝐵 ∈ { ∅ } )
5 4 ralrimiva ⊢ ( 𝑀 ∈ ( measures ‘ 𝑆 ) → ∀ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ { ∅ } } 𝐵 ∈ { ∅ } )
6 5 3ad2ant1 ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑆 ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) ) → ∀ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ { ∅ } } 𝐵 ∈ { ∅ } )
7 ssrab2 ⊢ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ { ∅ } } ⊆ 𝐴
8 ssct ⊢ ( ( { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ { ∅ } } ⊆ 𝐴 ∧ 𝐴 ≼ ω ) → { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ { ∅ } } ≼ ω )
9 7 8 mpan ⊢ ( 𝐴 ≼ ω → { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ { ∅ } } ≼ ω )
10 9 adantr ⊢ ( ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) → { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ { ∅ } } ≼ ω )
11 10 3ad2ant3 ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑆 ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) ) → { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ { ∅ } } ≼ ω )
12 simp3r ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑆 ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) ) → Disj 𝑥 ∈ 𝐴 𝐵 )
13 nfrab1 ⊢ Ⅎ 𝑥 { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ { ∅ } }
14 nfcv ⊢ Ⅎ 𝑥 𝐴
15 13 14 disjss1f ⊢ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ { ∅ } } ⊆ 𝐴 → ( Disj 𝑥 ∈ 𝐴 𝐵 → Disj 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ { ∅ } } 𝐵 ) )
16 7 12 15 mpsyl ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑆 ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) ) → Disj 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ { ∅ } } 𝐵 )
17 13 measvunilem0 ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ { ∅ } } 𝐵 ∈ { ∅ } ∧ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ { ∅ } } ≼ ω ∧ Disj 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ { ∅ } } 𝐵 ) ) → ( 𝑀 ‘ ∪ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ { ∅ } } 𝐵 ) = Σ* 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ { ∅ } } ( 𝑀 ‘ 𝐵 ) )
18 1 6 11 16 17 syl112anc ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑆 ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) ) → ( 𝑀 ‘ ∪ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ { ∅ } } 𝐵 ) = Σ* 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ { ∅ } } ( 𝑀 ‘ 𝐵 ) )
19 rabid ⊢ ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) } ↔ ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) ) )
20 19 simprbi ⊢ ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) } → 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) )
21 20 adantl ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) } ) → 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) )
22 21 ralrimiva ⊢ ( 𝑀 ∈ ( measures ‘ 𝑆 ) → ∀ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) } 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) )
23 22 3ad2ant1 ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑆 ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) ) → ∀ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) } 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) )
24 ssrab2 ⊢ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) } ⊆ 𝐴
25 ssct ⊢ ( ( { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) } ⊆ 𝐴 ∧ 𝐴 ≼ ω ) → { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) } ≼ ω )
26 24 25 mpan ⊢ ( 𝐴 ≼ ω → { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) } ≼ ω )
27 26 adantr ⊢ ( ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) → { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) } ≼ ω )
28 27 3ad2ant3 ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑆 ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) ) → { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) } ≼ ω )
29 nfrab1 ⊢ Ⅎ 𝑥 { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) }
30 29 14 disjss1f ⊢ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) } ⊆ 𝐴 → ( Disj 𝑥 ∈ 𝐴 𝐵 → Disj 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) } 𝐵 ) )
31 24 12 30 mpsyl ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑆 ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) ) → Disj 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) } 𝐵 )
32 29 measvunilem ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) } 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) ∧ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) } ≼ ω ∧ Disj 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) } 𝐵 ) ) → ( 𝑀 ‘ ∪ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) } 𝐵 ) = Σ* 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) } ( 𝑀 ‘ 𝐵 ) )
33 1 23 28 31 32 syl112anc ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑆 ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) ) → ( 𝑀 ‘ ∪ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) } 𝐵 ) = Σ* 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) } ( 𝑀 ‘ 𝐵 ) )
34 18 33 oveq12d ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑆 ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) ) → ( ( 𝑀 ‘ ∪ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ { ∅ } } 𝐵 ) +𝑒 ( 𝑀 ‘ ∪ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) } 𝐵 ) ) = ( Σ* 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ { ∅ } } ( 𝑀 ‘ 𝐵 ) +𝑒 Σ* 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) } ( 𝑀 ‘ 𝐵 ) ) )
35 nfv ⊢ Ⅎ 𝑥 𝑀 ∈ ( measures ‘ 𝑆 )
36 nfra1 ⊢ Ⅎ 𝑥 ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑆
37 nfv ⊢ Ⅎ 𝑥 𝐴 ≼ ω
38 nfdisj1 ⊢ Ⅎ 𝑥 Disj 𝑥 ∈ 𝐴 𝐵
39 37 38 nfan ⊢ Ⅎ 𝑥 ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 )
40 35 36 39 nf3an ⊢ Ⅎ 𝑥 ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑆 ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) )
41 13 29 nfun ⊢ Ⅎ 𝑥 ( { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ { ∅ } } ∪ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) } )
42 simp2 ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑆 ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) ) → ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑆 )
43 rabid2 ⊢ ( 𝐴 = { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ 𝑆 } ↔ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑆 )
44 42 43 sylibr ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑆 ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) ) → 𝐴 = { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ 𝑆 } )
45 elun ⊢ ( 𝐵 ∈ ( { ∅ } ∪ ( 𝑆 ∖ { ∅ } ) ) ↔ ( 𝐵 ∈ { ∅ } ∨ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) ) )
46 measbase ⊢ ( 𝑀 ∈ ( measures ‘ 𝑆 ) → 𝑆 ∈ ∪ ran sigAlgebra )
47 0elsiga ⊢ ( 𝑆 ∈ ∪ ran sigAlgebra → ∅ ∈ 𝑆 )
48 snssi ⊢ ( ∅ ∈ 𝑆 → { ∅ } ⊆ 𝑆 )
49 46 47 48 3syl ⊢ ( 𝑀 ∈ ( measures ‘ 𝑆 ) → { ∅ } ⊆ 𝑆 )
50 undif ⊢ ( { ∅ } ⊆ 𝑆 ↔ ( { ∅ } ∪ ( 𝑆 ∖ { ∅ } ) ) = 𝑆 )
51 49 50 sylib ⊢ ( 𝑀 ∈ ( measures ‘ 𝑆 ) → ( { ∅ } ∪ ( 𝑆 ∖ { ∅ } ) ) = 𝑆 )
52 51 eleq2d ⊢ ( 𝑀 ∈ ( measures ‘ 𝑆 ) → ( 𝐵 ∈ ( { ∅ } ∪ ( 𝑆 ∖ { ∅ } ) ) ↔ 𝐵 ∈ 𝑆 ) )
53 45 52 bitr3id ⊢ ( 𝑀 ∈ ( measures ‘ 𝑆 ) → ( ( 𝐵 ∈ { ∅ } ∨ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) ) ↔ 𝐵 ∈ 𝑆 ) )
54 53 rabbidv ⊢ ( 𝑀 ∈ ( measures ‘ 𝑆 ) → { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∈ { ∅ } ∨ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) ) } = { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ 𝑆 } )
55 54 3ad2ant1 ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑆 ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) ) → { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∈ { ∅ } ∨ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) ) } = { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ 𝑆 } )
56 44 55 eqtr4d ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑆 ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) ) → 𝐴 = { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∈ { ∅ } ∨ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) ) } )
57 unrab ⊢ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ { ∅ } } ∪ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) } ) = { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∈ { ∅ } ∨ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) ) }
58 56 57 eqtr4di ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑆 ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) ) → 𝐴 = ( { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ { ∅ } } ∪ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) } ) )
59 eqidd ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑆 ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) ) → 𝐵 = 𝐵 )
60 40 14 41 58 59 iuneq12df ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑆 ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) ) → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ { ∅ } } ∪ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) } ) 𝐵 )
61 60 fveq2d ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑆 ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) ) → ( 𝑀 ‘ ∪ 𝑥 ∈ 𝐴 𝐵 ) = ( 𝑀 ‘ ∪ 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ { ∅ } } ∪ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) } ) 𝐵 ) )
62 iunxun ⊢ ∪ 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ { ∅ } } ∪ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) } ) 𝐵 = ( ∪ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ { ∅ } } 𝐵 ∪ ∪ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) } 𝐵 )
63 62 fveq2i ⊢ ( 𝑀 ‘ ∪ 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ { ∅ } } ∪ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) } ) 𝐵 ) = ( 𝑀 ‘ ( ∪ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ { ∅ } } 𝐵 ∪ ∪ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) } 𝐵 ) )
64 61 63 eqtrdi ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑆 ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) ) → ( 𝑀 ‘ ∪ 𝑥 ∈ 𝐴 𝐵 ) = ( 𝑀 ‘ ( ∪ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ { ∅ } } 𝐵 ∪ ∪ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) } 𝐵 ) ) )
65 46 3ad2ant1 ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑆 ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) ) → 𝑆 ∈ ∪ ran sigAlgebra )
66 47 adantr ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐵 ∈ { ∅ } ) → ∅ ∈ 𝑆 )
67 elsni ⊢ ( 𝐵 ∈ { ∅ } → 𝐵 = ∅ )
68 67 eleq1d ⊢ ( 𝐵 ∈ { ∅ } → ( 𝐵 ∈ 𝑆 ↔ ∅ ∈ 𝑆 ) )
69 68 adantl ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐵 ∈ { ∅ } ) → ( 𝐵 ∈ 𝑆 ↔ ∅ ∈ 𝑆 ) )
70 66 69 mpbird ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐵 ∈ { ∅ } ) → 𝐵 ∈ 𝑆 )
71 46 3 70 syl2an ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ { ∅ } } ) → 𝐵 ∈ 𝑆 )
72 71 ralrimiva ⊢ ( 𝑀 ∈ ( measures ‘ 𝑆 ) → ∀ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ { ∅ } } 𝐵 ∈ 𝑆 )
73 72 3ad2ant1 ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑆 ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) ) → ∀ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ { ∅ } } 𝐵 ∈ 𝑆 )
74 13 sigaclcuni ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ ∀ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ { ∅ } } 𝐵 ∈ 𝑆 ∧ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ { ∅ } } ≼ ω ) → ∪ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ { ∅ } } 𝐵 ∈ 𝑆 )
75 65 73 11 74 syl3anc ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑆 ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) ) → ∪ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ { ∅ } } 𝐵 ∈ 𝑆 )
76 21 eldifad ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) } ) → 𝐵 ∈ 𝑆 )
77 76 ralrimiva ⊢ ( 𝑀 ∈ ( measures ‘ 𝑆 ) → ∀ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) } 𝐵 ∈ 𝑆 )
78 77 3ad2ant1 ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑆 ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) ) → ∀ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) } 𝐵 ∈ 𝑆 )
79 29 sigaclcuni ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ ∀ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) } 𝐵 ∈ 𝑆 ∧ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) } ≼ ω ) → ∪ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) } 𝐵 ∈ 𝑆 )
80 65 78 28 79 syl3anc ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑆 ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) ) → ∪ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) } 𝐵 ∈ 𝑆 )
81 3 67 syl ⊢ ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ { ∅ } } → 𝐵 = ∅ )
82 81 iuneq2i ⊢ ∪ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ { ∅ } } 𝐵 = ∪ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ { ∅ } } ∅
83 iun0 ⊢ ∪ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ { ∅ } } ∅ = ∅
84 82 83 eqtri ⊢ ∪ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ { ∅ } } 𝐵 = ∅
85 ineq1 ⊢ ( ∪ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ { ∅ } } 𝐵 = ∅ → ( ∪ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ { ∅ } } 𝐵 ∩ ∪ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) } 𝐵 ) = ( ∅ ∩ ∪ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) } 𝐵 ) )
86 0in ⊢ ( ∅ ∩ ∪ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) } 𝐵 ) = ∅
87 85 86 eqtrdi ⊢ ( ∪ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ { ∅ } } 𝐵 = ∅ → ( ∪ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ { ∅ } } 𝐵 ∩ ∪ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) } 𝐵 ) = ∅ )
88 84 87 mp1i ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑆 ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) ) → ( ∪ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ { ∅ } } 𝐵 ∩ ∪ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) } 𝐵 ) = ∅ )
89 measun ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ( ∪ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ { ∅ } } 𝐵 ∈ 𝑆 ∧ ∪ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) } 𝐵 ∈ 𝑆 ) ∧ ( ∪ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ { ∅ } } 𝐵 ∩ ∪ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) } 𝐵 ) = ∅ ) → ( 𝑀 ‘ ( ∪ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ { ∅ } } 𝐵 ∪ ∪ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) } 𝐵 ) ) = ( ( 𝑀 ‘ ∪ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ { ∅ } } 𝐵 ) +𝑒 ( 𝑀 ‘ ∪ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) } 𝐵 ) ) )
90 1 75 80 88 89 syl121anc ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑆 ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) ) → ( 𝑀 ‘ ( ∪ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ { ∅ } } 𝐵 ∪ ∪ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) } 𝐵 ) ) = ( ( 𝑀 ‘ ∪ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ { ∅ } } 𝐵 ) +𝑒 ( 𝑀 ‘ ∪ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) } 𝐵 ) ) )
91 64 90 eqtrd ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑆 ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) ) → ( 𝑀 ‘ ∪ 𝑥 ∈ 𝐴 𝐵 ) = ( ( 𝑀 ‘ ∪ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ { ∅ } } 𝐵 ) +𝑒 ( 𝑀 ‘ ∪ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) } 𝐵 ) ) )
92 40 58 esumeq1d ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑆 ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) ) → Σ* 𝑥 ∈ 𝐴 ( 𝑀 ‘ 𝐵 ) = Σ* 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ { ∅ } } ∪ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) } ) ( 𝑀 ‘ 𝐵 ) )
93 ctex ⊢ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ { ∅ } } ≼ ω → { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ { ∅ } } ∈ V )
94 11 93 syl ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑆 ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) ) → { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ { ∅ } } ∈ V )
95 ctex ⊢ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) } ≼ ω → { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) } ∈ V )
96 28 95 syl ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑆 ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) ) → { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) } ∈ V )
97 inrab ⊢ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ { ∅ } } ∩ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) } ) = { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∈ { ∅ } ∧ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) ) }
98 noel ⊢ ¬ 𝐵 ∈ ∅
99 disjdif ⊢ ( { ∅ } ∩ ( 𝑆 ∖ { ∅ } ) ) = ∅
100 99 eleq2i ⊢ ( 𝐵 ∈ ( { ∅ } ∩ ( 𝑆 ∖ { ∅ } ) ) ↔ 𝐵 ∈ ∅ )
101 98 100 mtbir ⊢ ¬ 𝐵 ∈ ( { ∅ } ∩ ( 𝑆 ∖ { ∅ } ) )
102 elin ⊢ ( 𝐵 ∈ ( { ∅ } ∩ ( 𝑆 ∖ { ∅ } ) ) ↔ ( 𝐵 ∈ { ∅ } ∧ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) ) )
103 101 102 mtbi ⊢ ¬ ( 𝐵 ∈ { ∅ } ∧ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) )
104 103 rgenw ⊢ ∀ 𝑥 ∈ 𝐴 ¬ ( 𝐵 ∈ { ∅ } ∧ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) )
105 rabeq0 ⊢ ( { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∈ { ∅ } ∧ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) ) } = ∅ ↔ ∀ 𝑥 ∈ 𝐴 ¬ ( 𝐵 ∈ { ∅ } ∧ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) ) )
106 104 105 mpbir ⊢ { 𝑥 ∈ 𝐴 ∣ ( 𝐵 ∈ { ∅ } ∧ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) ) } = ∅
107 97 106 eqtri ⊢ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ { ∅ } } ∩ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) } ) = ∅
108 107 a1i ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑆 ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) ) → ( { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ { ∅ } } ∩ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) } ) = ∅ )
109 1 adantr ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑆 ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) ) ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ { ∅ } } ) → 𝑀 ∈ ( measures ‘ 𝑆 ) )
110 1 71 sylan ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑆 ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) ) ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ { ∅ } } ) → 𝐵 ∈ 𝑆 )
111 measvxrge0 ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐵 ∈ 𝑆 ) → ( 𝑀 ‘ 𝐵 ) ∈ ( 0 [,] +∞ ) )
112 109 110 111 syl2anc ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑆 ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) ) ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ { ∅ } } ) → ( 𝑀 ‘ 𝐵 ) ∈ ( 0 [,] +∞ ) )
113 1 adantr ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑆 ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) ) ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) } ) → 𝑀 ∈ ( measures ‘ 𝑆 ) )
114 20 adantl ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑆 ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) ) ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) } ) → 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) )
115 114 eldifad ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑆 ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) ) ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) } ) → 𝐵 ∈ 𝑆 )
116 113 115 111 syl2anc ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑆 ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) ) ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) } ) → ( 𝑀 ‘ 𝐵 ) ∈ ( 0 [,] +∞ ) )
117 40 13 29 94 96 108 112 116 esumsplit ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑆 ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) ) → Σ* 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ { ∅ } } ∪ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) } ) ( 𝑀 ‘ 𝐵 ) = ( Σ* 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ { ∅ } } ( 𝑀 ‘ 𝐵 ) +𝑒 Σ* 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) } ( 𝑀 ‘ 𝐵 ) ) )
118 92 117 eqtrd ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑆 ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) ) → Σ* 𝑥 ∈ 𝐴 ( 𝑀 ‘ 𝐵 ) = ( Σ* 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ { ∅ } } ( 𝑀 ‘ 𝐵 ) +𝑒 Σ* 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( 𝑆 ∖ { ∅ } ) } ( 𝑀 ‘ 𝐵 ) ) )
119 34 91 118 3eqtr4d ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑆 ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) ) → ( 𝑀 ‘ ∪ 𝑥 ∈ 𝐴 𝐵 ) = Σ* 𝑥 ∈ 𝐴 ( 𝑀 ‘ 𝐵 ) )