Theorem elcarsgss

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

	Ref	Expression
Hypotheses	carsgval.1	$$⊢\phi \to O\in V$$
	carsgval.2	$$⊢\phi \to M:𝒫O⟶\left[0,\mathrm{+\infty }\right]$$
	difelcarsg.1	$$⊢\phi \to A\in \mathrm{toCaraSiga}\left(M\right)$$
Assertion	elcarsgss	$$⊢\phi \to A\subseteq O$$

Proof

Step	Hyp	Ref	Expression
1		carsgval.1	$$⊢\phi \to O\in V$$
2		carsgval.2	$$⊢\phi \to M:𝒫O⟶\left[0,\mathrm{+\infty }\right]$$
3		difelcarsg.1	$$⊢\phi \to A\in \mathrm{toCaraSiga}\left(M\right)$$
4	1 2	carsgcl	$$⊢\phi \to \mathrm{toCaraSiga}\left(M\right)\subseteq 𝒫O$$
5	4 3	sseldd	$$⊢\phi \to A\in 𝒫O$$
6	5	elpwid	$$⊢\phi \to A\subseteq O$$