Theorem 0elcarsg

Description: The empty set is Caratheodory measurable. (Contributed by Thierry Arnoux, 30-May-2020)

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

Proof

Step	Hyp	Ref	Expression
1		carsgval.1	⊢ ( 𝜑 → 𝑂 ∈ 𝑉 )
2		carsgval.2	⊢ ( 𝜑 → 𝑀 : 𝒫 𝑂 ⟶ ( 0 [,] +∞ ) )
3		baselcarsg.1	⊢ ( 𝜑 → ( 𝑀 ‘ ∅ ) = 0 )
4		0ss	⊢ ∅ ⊆ 𝑂
5	4	a1i	⊢ ( 𝜑 → ∅ ⊆ 𝑂 )
6		in0	⊢ ( 𝑒 ∩ ∅ ) = ∅
7	6	fveq2i	⊢ ( 𝑀 ‘ ( 𝑒 ∩ ∅ ) ) = ( 𝑀 ‘ ∅ )
8	7 3	syl5eq	⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝑒 ∩ ∅ ) ) = 0 )
9		dif0	⊢ ( 𝑒 ∖ ∅ ) = 𝑒
10	9	fveq2i	⊢ ( 𝑀 ‘ ( 𝑒 ∖ ∅ ) ) = ( 𝑀 ‘ 𝑒 )
11	10	a1i	⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝑒 ∖ ∅ ) ) = ( 𝑀 ‘ 𝑒 ) )
12	8 11	oveq12d	⊢ ( 𝜑 → ( ( 𝑀 ‘ ( 𝑒 ∩ ∅ ) ) +𝑒 ( 𝑀 ‘ ( 𝑒 ∖ ∅ ) ) ) = ( 0 +𝑒 ( 𝑀 ‘ 𝑒 ) ) )
13	12	adantr	⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( ( 𝑀 ‘ ( 𝑒 ∩ ∅ ) ) +𝑒 ( 𝑀 ‘ ( 𝑒 ∖ ∅ ) ) ) = ( 0 +𝑒 ( 𝑀 ‘ 𝑒 ) ) )
14		iccssxr	⊢ ( 0 [,] +∞ ) ⊆ ℝ*
15	2	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ 𝑒 ) ∈ ( 0 [,] +∞ ) )
16	14 15	sselid	⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ 𝑒 ) ∈ ℝ* )
17		xaddid2	⊢ ( ( 𝑀 ‘ 𝑒 ) ∈ ℝ* → ( 0 +𝑒 ( 𝑀 ‘ 𝑒 ) ) = ( 𝑀 ‘ 𝑒 ) )
18	16 17	syl	⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( 0 +𝑒 ( 𝑀 ‘ 𝑒 ) ) = ( 𝑀 ‘ 𝑒 ) )
19	13 18	eqtrd	⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ) → ( ( 𝑀 ‘ ( 𝑒 ∩ ∅ ) ) +𝑒 ( 𝑀 ‘ ( 𝑒 ∖ ∅ ) ) ) = ( 𝑀 ‘ 𝑒 ) )
20	19	ralrimiva	⊢ ( 𝜑 → ∀ 𝑒 ∈ 𝒫 𝑂 ( ( 𝑀 ‘ ( 𝑒 ∩ ∅ ) ) +𝑒 ( 𝑀 ‘ ( 𝑒 ∖ ∅ ) ) ) = ( 𝑀 ‘ 𝑒 ) )
21	1 2	elcarsg	⊢ ( 𝜑 → ( ∅ ∈ ( toCaraSiga ‘ 𝑀 ) ↔ ( ∅ ⊆ 𝑂 ∧ ∀ 𝑒 ∈ 𝒫 𝑂 ( ( 𝑀 ‘ ( 𝑒 ∩ ∅ ) ) +𝑒 ( 𝑀 ‘ ( 𝑒 ∖ ∅ ) ) ) = ( 𝑀 ‘ 𝑒 ) ) ) )
22	5 20 21	mpbir2and	⊢ ( 𝜑 → ∅ ∈ ( toCaraSiga ‘ 𝑀 ) )