Theorem carsguni

Description: The union of all Caratheodory measurable sets is the universe. (Contributed by Thierry Arnoux, 22-May-2020)

	Ref	Expression
Hypotheses	carsgval.1	|- ( ph -> O e. V )
	carsgval.2	|- ( ph -> M : ~P O --> ( 0 [,] +oo ) )
	baselcarsg.1	|- ( ph -> ( M ` (/) ) = 0 )
Assertion	carsguni	|- ( ph -> U. ( toCaraSiga ` M ) = O )

Proof

Step	Hyp	Ref	Expression
1		carsgval.1	|- ( ph -> O e. V )
2		carsgval.2	|- ( ph -> M : ~P O --> ( 0 [,] +oo ) )
3		baselcarsg.1	|- ( ph -> ( M ` (/) ) = 0 )
4	1 2	carsgcl	|- ( ph -> ( toCaraSiga ` M ) C_ ~P O )
5	4	sselda	|- ( ( ph /\ a e. ( toCaraSiga ` M ) ) -> a e. ~P O )
6	5	elpwid	|- ( ( ph /\ a e. ( toCaraSiga ` M ) ) -> a C_ O )
7	6	ralrimiva	|- ( ph -> A. a e. ( toCaraSiga ` M ) a C_ O )
8		unissb	|- ( U. ( toCaraSiga ` M ) C_ O <-> A. a e. ( toCaraSiga ` M ) a C_ O )
9	7 8	sylibr	|- ( ph -> U. ( toCaraSiga ` M ) C_ O )
10	1 2 3	baselcarsg	|- ( ph -> O e. ( toCaraSiga ` M ) )
11		unissel	|- ( ( U. ( toCaraSiga ` M ) C_ O /\ O e. ( toCaraSiga ` M ) ) -> U. ( toCaraSiga ` M ) = O )
12	9 10 11	syl2anc	|- ( ph -> U. ( toCaraSiga ` M ) = O )