Metamath Proof Explorer


Theorem elcarsgss

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

Ref Expression
Hypotheses carsgval.1 φ O V
carsgval.2 φ M : 𝒫 O 0 +∞
difelcarsg.1 φ A toCaraSiga M
Assertion elcarsgss φ A O

Proof

Step Hyp Ref Expression
1 carsgval.1 φ O V
2 carsgval.2 φ M : 𝒫 O 0 +∞
3 difelcarsg.1 φ A toCaraSiga M
4 1 2 carsgcl φ toCaraSiga M 𝒫 O
5 4 3 sseldd φ A 𝒫 O
6 5 elpwid φ A O