Theorem elcarsgss

Description: Caratheodory measurable sets are subsets of the universe. (Contributed by Thierry Arnoux, 21-May-2020)

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

Proof

Step	Hyp	Ref	Expression
1		carsgval.1	⊢ ( 𝜑 → 𝑂 ∈ 𝑉 )
2		carsgval.2	⊢ ( 𝜑 → 𝑀 : 𝒫 𝑂 ⟶ ( 0 [,] +∞ ) )
3		difelcarsg.1	⊢ ( 𝜑 → 𝐴 ∈ ( toCaraSiga ‘ 𝑀 ) )
4	1 2	carsgcl	⊢ ( 𝜑 → ( toCaraSiga ‘ 𝑀 ) ⊆ 𝒫 𝑂 )
5	4 3	sseldd	⊢ ( 𝜑 → 𝐴 ∈ 𝒫 𝑂 )
6	5	elpwid	⊢ ( 𝜑 → 𝐴 ⊆ 𝑂 )