Theorem carageneld

Description: Membership in the Caratheodory's construction. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	carageneld.o	|- ( ph -> O e. OutMeas )
	carageneld.x	|- X = U. dom O
	carageneld.s	|- S = ( CaraGen ` O )
	carageneld.e	|- ( ph -> E e. ~P X )
	carageneld.a	|- ( ( ph /\ a e. ~P X ) -> ( ( O ` ( a i^i E ) ) +e ( O ` ( a \ E ) ) ) = ( O ` a ) )
Assertion	carageneld	|- ( ph -> E e. S )

Proof

Step	Hyp	Ref	Expression
1		carageneld.o	|- ( ph -> O e. OutMeas )
2		carageneld.x	|- X = U. dom O
3		carageneld.s	|- S = ( CaraGen ` O )
4		carageneld.e	|- ( ph -> E e. ~P X )
5		carageneld.a	|- ( ( ph /\ a e. ~P X ) -> ( ( O ` ( a i^i E ) ) +e ( O ` ( a \ E ) ) ) = ( O ` a ) )
6	2	pweqi	|- ~P X = ~P U. dom O
7	4 6	eleqtrdi	|- ( ph -> E e. ~P U. dom O )
8		simpl	|- ( ( ph /\ a e. ~P U. dom O ) -> ph )
9	6	eleq2i	|- ( a e. ~P X <-> a e. ~P U. dom O )
10	9	bicomi	|- ( a e. ~P U. dom O <-> a e. ~P X )
11	10	biimpi	|- ( a e. ~P U. dom O -> a e. ~P X )
12	11	adantl	|- ( ( ph /\ a e. ~P U. dom O ) -> a e. ~P X )
13	8 12 5	syl2anc	|- ( ( ph /\ a e. ~P U. dom O ) -> ( ( O ` ( a i^i E ) ) +e ( O ` ( a \ E ) ) ) = ( O ` a ) )
14	13	ralrimiva	|- ( ph -> A. a e. ~P U. dom O ( ( O ` ( a i^i E ) ) +e ( O ` ( a \ E ) ) ) = ( O ` a ) )
15	7 14	jca	|- ( ph -> ( E e. ~P U. dom O /\ A. a e. ~P U. dom O ( ( O ` ( a i^i E ) ) +e ( O ` ( a \ E ) ) ) = ( O ` a ) ) )
16	1 3	caragenel	|- ( ph -> ( E e. S <-> ( E e. ~P U. dom O /\ A. a e. ~P U. dom O ( ( O ` ( a i^i E ) ) +e ( O ` ( a \ E ) ) ) = ( O ` a ) ) ) )
17	15 16	mpbird	|- ( ph -> E e. S )