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
|- ( ph -> O e. V )
carsgval.2
|- ( ph -> M : ~P O --> ( 0 [,] +oo ) )
difelcarsg.1
|- ( ph -> A e. ( toCaraSiga ` M ) )
Assertion elcarsgss
|- ( ph -> A C_ O )

Proof

Step Hyp Ref Expression
1 carsgval.1
 |-  ( ph -> O e. V )
2 carsgval.2
 |-  ( ph -> M : ~P O --> ( 0 [,] +oo ) )
3 difelcarsg.1
 |-  ( ph -> A e. ( toCaraSiga ` M ) )
4 1 2 carsgcl
 |-  ( ph -> ( toCaraSiga ` M ) C_ ~P O )
5 4 3 sseldd
 |-  ( ph -> A e. ~P O )
6 5 elpwid
 |-  ( ph -> A C_ O )