Metamath Proof Explorer

Theorem fiunelcarsg

Description: The Caratheodory measurable sets are closed under finite union. (Contributed by Thierry Arnoux, 23-May-2020)

Ref Expression
Hypotheses carsgval.1 ⊢ ( 𝜑 → 𝑂 ∈ 𝑉 )
carsgval.2 ⊢ ( 𝜑 → 𝑀 : 𝒫 𝑂 ⟶ ( 0 [,] +∞ ) )
carsgsiga.1 ⊢ ( 𝜑 → ( 𝑀 ‘ ∅ ) = 0 )
carsgsiga.2 ⊢ ( ( 𝜑 ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂 ) → ( 𝑀 ‘ ∪ 𝑥 ) ≤ Σ* 𝑦 ∈ 𝑥 ( 𝑀 ‘ 𝑦 ) )
fiunelcarsg.1 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
fiunelcarsg.2 ⊢ ( 𝜑 → 𝐴 ⊆ ( toCaraSiga ‘ 𝑀 ) )
Assertion fiunelcarsg ( 𝜑 → ∪ 𝐴 ∈ ( toCaraSiga ‘ 𝑀 ) )

Proof

Step Hyp Ref Expression
1 carsgval.1 ⊢ ( 𝜑 → 𝑂 ∈ 𝑉 )
2 carsgval.2 ⊢ ( 𝜑 → 𝑀 : 𝒫 𝑂 ⟶ ( 0 [,] +∞ ) )
3 carsgsiga.1 ⊢ ( 𝜑 → ( 𝑀 ‘ ∅ ) = 0 )
4 carsgsiga.2 ⊢ ( ( 𝜑 ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂 ) → ( 𝑀 ‘ ∪ 𝑥 ) ≤ Σ* 𝑦 ∈ 𝑥 ( 𝑀 ‘ 𝑦 ) )
5 fiunelcarsg.1 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
6 fiunelcarsg.2 ⊢ ( 𝜑 → 𝐴 ⊆ ( toCaraSiga ‘ 𝑀 ) )
7 unieq ⊢ ( 𝑎 = ∅ → ∪ 𝑎 = ∪ ∅ )
8 eqidd ⊢ ( 𝑎 = ∅ → ( toCaraSiga ‘ 𝑀 ) = ( toCaraSiga ‘ 𝑀 ) )
9 7 8 eleq12d ⊢ ( 𝑎 = ∅ → ( ∪ 𝑎 ∈ ( toCaraSiga ‘ 𝑀 ) ↔ ∪ ∅ ∈ ( toCaraSiga ‘ 𝑀 ) ) )
10 unieq ⊢ ( 𝑎 = 𝑏 → ∪ 𝑎 = ∪ 𝑏 )
11 eqidd ⊢ ( 𝑎 = 𝑏 → ( toCaraSiga ‘ 𝑀 ) = ( toCaraSiga ‘ 𝑀 ) )
12 10 11 eleq12d ⊢ ( 𝑎 = 𝑏 → ( ∪ 𝑎 ∈ ( toCaraSiga ‘ 𝑀 ) ↔ ∪ 𝑏 ∈ ( toCaraSiga ‘ 𝑀 ) ) )
13 unieq ⊢ ( 𝑎 = ( 𝑏 ∪ { 𝑥 } ) → ∪ 𝑎 = ∪ ( 𝑏 ∪ { 𝑥 } ) )
14 eqidd ⊢ ( 𝑎 = ( 𝑏 ∪ { 𝑥 } ) → ( toCaraSiga ‘ 𝑀 ) = ( toCaraSiga ‘ 𝑀 ) )
15 13 14 eleq12d ⊢ ( 𝑎 = ( 𝑏 ∪ { 𝑥 } ) → ( ∪ 𝑎 ∈ ( toCaraSiga ‘ 𝑀 ) ↔ ∪ ( 𝑏 ∪ { 𝑥 } ) ∈ ( toCaraSiga ‘ 𝑀 ) ) )
16 unieq ⊢ ( 𝑎 = 𝐴 → ∪ 𝑎 = ∪ 𝐴 )
17 eqidd ⊢ ( 𝑎 = 𝐴 → ( toCaraSiga ‘ 𝑀 ) = ( toCaraSiga ‘ 𝑀 ) )
18 16 17 eleq12d ⊢ ( 𝑎 = 𝐴 → ( ∪ 𝑎 ∈ ( toCaraSiga ‘ 𝑀 ) ↔ ∪ 𝐴 ∈ ( toCaraSiga ‘ 𝑀 ) ) )
19 uni0 ⊢ ∪ ∅ = ∅
20 difid ⊢ ( 𝑂 ∖ 𝑂 ) = ∅
21 19 20 eqtr4i ⊢ ∪ ∅ = ( 𝑂 ∖ 𝑂 )
22 1 2 3 baselcarsg ⊢ ( 𝜑 → 𝑂 ∈ ( toCaraSiga ‘ 𝑀 ) )
23 1 2 22 difelcarsg ⊢ ( 𝜑 → ( 𝑂 ∖ 𝑂 ) ∈ ( toCaraSiga ‘ 𝑀 ) )
24 21 23 eqeltrid ⊢ ( 𝜑 → ∪ ∅ ∈ ( toCaraSiga ‘ 𝑀 ) )
25 uniun ⊢ ∪ ( 𝑏 ∪ { 𝑥 } ) = ( ∪ 𝑏 ∪ ∪ { 𝑥 } )
26 vex ⊢ 𝑥 ∈ V
27 26 unisn ⊢ ∪ { 𝑥 } = 𝑥
28 27 uneq2i ⊢ ( ∪ 𝑏 ∪ ∪ { 𝑥 } ) = ( ∪ 𝑏 ∪ 𝑥 )
29 25 28 eqtri ⊢ ∪ ( 𝑏 ∪ { 𝑥 } ) = ( ∪ 𝑏 ∪ 𝑥 )
30 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ ∪ 𝑏 ∈ ( toCaraSiga ‘ 𝑀 ) ) → 𝑂 ∈ 𝑉 )
31 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ ∪ 𝑏 ∈ ( toCaraSiga ‘ 𝑀 ) ) → 𝑀 : 𝒫 𝑂 ⟶ ( 0 [,] +∞ ) )
32 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ ∪ 𝑏 ∈ ( toCaraSiga ‘ 𝑀 ) ) → ∪ 𝑏 ∈ ( toCaraSiga ‘ 𝑀 ) )
33 simpll ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ ∪ 𝑏 ∈ ( toCaraSiga ‘ 𝑀 ) ) → 𝜑 )
34 1 2 3 4 carsgsigalem ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ∧ 𝑓 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ ( 𝑒 ∪ 𝑓 ) ) ≤ ( ( 𝑀 ‘ 𝑒 ) +𝑒 ( 𝑀 ‘ 𝑓 ) ) )
35 33 34 syl3an1 ⊢ ( ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ ∪ 𝑏 ∈ ( toCaraSiga ‘ 𝑀 ) ) ∧ 𝑒 ∈ 𝒫 𝑂 ∧ 𝑓 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ ( 𝑒 ∪ 𝑓 ) ) ≤ ( ( 𝑀 ‘ 𝑒 ) +𝑒 ( 𝑀 ‘ 𝑓 ) ) )
36 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ ∪ 𝑏 ∈ ( toCaraSiga ‘ 𝑀 ) ) → 𝐴 ⊆ ( toCaraSiga ‘ 𝑀 ) )
37 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ ∪ 𝑏 ∈ ( toCaraSiga ‘ 𝑀 ) ) → 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) )
38 37 eldifad ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ ∪ 𝑏 ∈ ( toCaraSiga ‘ 𝑀 ) ) → 𝑥 ∈ 𝐴 )
39 36 38 sseldd ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ ∪ 𝑏 ∈ ( toCaraSiga ‘ 𝑀 ) ) → 𝑥 ∈ ( toCaraSiga ‘ 𝑀 ) )
40 30 31 32 35 39 unelcarsg ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ ∪ 𝑏 ∈ ( toCaraSiga ‘ 𝑀 ) ) → ( ∪ 𝑏 ∪ 𝑥 ) ∈ ( toCaraSiga ‘ 𝑀 ) )
41 29 40 eqeltrid ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ ∪ 𝑏 ∈ ( toCaraSiga ‘ 𝑀 ) ) → ∪ ( 𝑏 ∪ { 𝑥 } ) ∈ ( toCaraSiga ‘ 𝑀 ) )
42 41 ex ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → ( ∪ 𝑏 ∈ ( toCaraSiga ‘ 𝑀 ) → ∪ ( 𝑏 ∪ { 𝑥 } ) ∈ ( toCaraSiga ‘ 𝑀 ) ) )
43 9 12 15 18 24 42 5 findcard2d ⊢ ( 𝜑 → ∪ 𝐴 ∈ ( toCaraSiga ‘ 𝑀 ) )