Theorem caragenelss

Description: An element of the Caratheodory's construction is a subset of the base set of the outer measure. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	caragenelss.o	|- ( ph -> O e. OutMeas )
	caragenelss.s	|- S = ( CaraGen ` O )
	caragenelss.a	|- ( ph -> A e. S )
	caragenelss.x	|- X = U. dom O
Assertion	caragenelss	|- ( ph -> A C_ X )

Proof

Step	Hyp	Ref	Expression
1		caragenelss.o	|- ( ph -> O e. OutMeas )
2		caragenelss.s	|- S = ( CaraGen ` O )
3		caragenelss.a	|- ( ph -> A e. S )
4		caragenelss.x	|- X = U. dom O
5	1 2	caragenel	|- ( ph -> ( A e. S <-> ( A e. ~P U. dom O /\ A. x e. ~P U. dom O ( ( O ` ( x i^i A ) ) +e ( O ` ( x \ A ) ) ) = ( O ` x ) ) ) )
6	3 5	mpbid	|- ( ph -> ( A e. ~P U. dom O /\ A. x e. ~P U. dom O ( ( O ` ( x i^i A ) ) +e ( O ` ( x \ A ) ) ) = ( O ` x ) ) )
7	6	simpld	|- ( ph -> A e. ~P U. dom O )
8	4	eqcomi	|- U. dom O = X
9	8	pweqi	|- ~P U. dom O = ~P X
10	9	a1i	|- ( ph -> ~P U. dom O = ~P X )
11	7 10	eleqtrd	|- ( ph -> A e. ~P X )
12		elpwg	|- ( A e. S -> ( A e. ~P X <-> A C_ X ) )
13	3 12	syl	|- ( ph -> ( A e. ~P X <-> A C_ X ) )
14	11 13	mpbid	|- ( ph -> A C_ X )