Theorem baselcarsg

Description: The universe set, O , is Caratheodory measurable. (Contributed by Thierry Arnoux, 17-May-2020)

	Ref	Expression
Hypotheses	carsgval.1	⊢ ( 𝜑 → 𝑂 ∈ 𝑉 )
	carsgval.2	⊢ ( 𝜑 → 𝑀 : 𝒫 𝑂 ⟶ ( 0 [,] +∞ ) )
	baselcarsg.1	⊢ ( 𝜑 → ( 𝑀 ‘ ∅ ) = 0 )
Assertion	baselcarsg	⊢ ( 𝜑 → 𝑂 ∈ ( toCaraSiga ‘ 𝑀 ) )

Proof

Step	Hyp	Ref	Expression
1		carsgval.1	⊢ ( 𝜑 → 𝑂 ∈ 𝑉 )
2		carsgval.2	⊢ ( 𝜑 → 𝑀 : 𝒫 𝑂 ⟶ ( 0 [,] +∞ ) )
3		baselcarsg.1	⊢ ( 𝜑 → ( 𝑀 ‘ ∅ ) = 0 )
4		ssidd	⊢ ( 𝜑 → 𝑂 ⊆ 𝑂 )
5		elpwi	⊢ ( 𝑒 ∈ 𝒫 𝑂 → 𝑒 ⊆ 𝑂 )
6	5	adantl	⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → 𝑒 ⊆ 𝑂 )
7		df-ss	⊢ ( 𝑒 ⊆ 𝑂 ↔ ( 𝑒 ∩ 𝑂 ) = 𝑒 )
8	6 7	sylib	⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( 𝑒 ∩ 𝑂 ) = 𝑒 )
9	8	fveq2d	⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ ( 𝑒 ∩ 𝑂 ) ) = ( 𝑀 ‘ 𝑒 ) )
10		ssdif0	⊢ ( 𝑒 ⊆ 𝑂 ↔ ( 𝑒 ∖ 𝑂 ) = ∅ )
11	6 10	sylib	⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( 𝑒 ∖ 𝑂 ) = ∅ )
12	11	fveq2d	⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ ( 𝑒 ∖ 𝑂 ) ) = ( 𝑀 ‘ ∅ ) )
13	3	adantr	⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ ∅ ) = 0 )
14	12 13	eqtrd	⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ ( 𝑒 ∖ 𝑂 ) ) = 0 )
15	9 14	oveq12d	⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( ( 𝑀 ‘ ( 𝑒 ∩ 𝑂 ) ) +𝑒 ( 𝑀 ‘ ( 𝑒 ∖ 𝑂 ) ) ) = ( ( 𝑀 ‘ 𝑒 ) +𝑒 0 ) )
16		iccssxr	⊢ ( 0 [,] +∞ ) ⊆ ℝ*
17	2	adantr	⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → 𝑀 : 𝒫 𝑂 ⟶ ( 0 [,] +∞ ) )
18		simpr	⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → 𝑒 ∈ 𝒫 𝑂 )
19	17 18	ffvelrnd	⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ 𝑒 ) ∈ ( 0 [,] +∞ ) )
20	16 19	sselid	⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ 𝑒 ) ∈ ℝ* )
21		xaddid1	⊢ ( ( 𝑀 ‘ 𝑒 ) ∈ ℝ* → ( ( 𝑀 ‘ 𝑒 ) +𝑒 0 ) = ( 𝑀 ‘ 𝑒 ) )
22	20 21	syl	⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( ( 𝑀 ‘ 𝑒 ) +𝑒 0 ) = ( 𝑀 ‘ 𝑒 ) )
23	15 22	eqtrd	⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( ( 𝑀 ‘ ( 𝑒 ∩ 𝑂 ) ) +𝑒 ( 𝑀 ‘ ( 𝑒 ∖ 𝑂 ) ) ) = ( 𝑀 ‘ 𝑒 ) )
24	23	ralrimiva	⊢ ( 𝜑 → ∀ 𝑒 ∈ 𝒫 𝑂 ( ( 𝑀 ‘ ( 𝑒 ∩ 𝑂 ) ) +𝑒 ( 𝑀 ‘ ( 𝑒 ∖ 𝑂 ) ) ) = ( 𝑀 ‘ 𝑒 ) )
25	4 24	jca	⊢ ( 𝜑 → ( 𝑂 ⊆ 𝑂 ∧ ∀ 𝑒 ∈ 𝒫 𝑂 ( ( 𝑀 ‘ ( 𝑒 ∩ 𝑂 ) ) +𝑒 ( 𝑀 ‘ ( 𝑒 ∖ 𝑂 ) ) ) = ( 𝑀 ‘ 𝑒 ) ) )
26	1 2	elcarsg	⊢ ( 𝜑 → ( 𝑂 ∈ ( toCaraSiga ‘ 𝑀 ) ↔ ( 𝑂 ⊆ 𝑂 ∧ ∀ 𝑒 ∈ 𝒫 𝑂 ( ( 𝑀 ‘ ( 𝑒 ∩ 𝑂 ) ) +𝑒 ( 𝑀 ‘ ( 𝑒 ∖ 𝑂 ) ) ) = ( 𝑀 ‘ 𝑒 ) ) ) )
27	25 26	mpbird	⊢ ( 𝜑 → 𝑂 ∈ ( toCaraSiga ‘ 𝑀 ) )