Metamath Proof Explorer


Theorem unelcarsg

Description: The Caratheodory-measurable sets are closed under pairwise unions. (Contributed by Thierry Arnoux, 21-May-2020)

Ref Expression
Hypotheses carsgval.1
|- ( ph -> O e. V )
carsgval.2
|- ( ph -> M : ~P O --> ( 0 [,] +oo ) )
difelcarsg.1
|- ( ph -> A e. ( toCaraSiga ` M ) )
inelcarsg.1
|- ( ( ph /\ a e. ~P O /\ b e. ~P O ) -> ( M ` ( a u. b ) ) <_ ( ( M ` a ) +e ( M ` b ) ) )
inelcarsg.2
|- ( ph -> B e. ( toCaraSiga ` M ) )
Assertion unelcarsg
|- ( ph -> ( A u. B ) e. ( toCaraSiga ` M ) )

Proof

Step Hyp Ref Expression
1 carsgval.1
 |-  ( ph -> O e. V )
2 carsgval.2
 |-  ( ph -> M : ~P O --> ( 0 [,] +oo ) )
3 difelcarsg.1
 |-  ( ph -> A e. ( toCaraSiga ` M ) )
4 inelcarsg.1
 |-  ( ( ph /\ a e. ~P O /\ b e. ~P O ) -> ( M ` ( a u. b ) ) <_ ( ( M ` a ) +e ( M ` b ) ) )
5 inelcarsg.2
 |-  ( ph -> B e. ( toCaraSiga ` M ) )
6 1 2 3 elcarsgss
 |-  ( ph -> A C_ O )
7 dfss4
 |-  ( A C_ O <-> ( O \ ( O \ A ) ) = A )
8 6 7 sylib
 |-  ( ph -> ( O \ ( O \ A ) ) = A )
9 1 2 5 elcarsgss
 |-  ( ph -> B C_ O )
10 dfss4
 |-  ( B C_ O <-> ( O \ ( O \ B ) ) = B )
11 9 10 sylib
 |-  ( ph -> ( O \ ( O \ B ) ) = B )
12 8 11 uneq12d
 |-  ( ph -> ( ( O \ ( O \ A ) ) u. ( O \ ( O \ B ) ) ) = ( A u. B ) )
13 difindi
 |-  ( O \ ( ( O \ A ) i^i ( O \ B ) ) ) = ( ( O \ ( O \ A ) ) u. ( O \ ( O \ B ) ) )
14 1 2 3 difelcarsg
 |-  ( ph -> ( O \ A ) e. ( toCaraSiga ` M ) )
15 1 2 5 difelcarsg
 |-  ( ph -> ( O \ B ) e. ( toCaraSiga ` M ) )
16 1 2 14 4 15 inelcarsg
 |-  ( ph -> ( ( O \ A ) i^i ( O \ B ) ) e. ( toCaraSiga ` M ) )
17 1 2 16 difelcarsg
 |-  ( ph -> ( O \ ( ( O \ A ) i^i ( O \ B ) ) ) e. ( toCaraSiga ` M ) )
18 13 17 eqeltrrid
 |-  ( ph -> ( ( O \ ( O \ A ) ) u. ( O \ ( O \ B ) ) ) e. ( toCaraSiga ` M ) )
19 12 18 eqeltrrd
 |-  ( ph -> ( A u. B ) e. ( toCaraSiga ` M ) )