Theorem caragenel2d

Description: Membership in the Caratheodory's construction. Similar to carageneld , but here "less then or equal to" is used, instead of equality. This is Remark 113D of Fremlin1 p. 21. (Contributed by Glauco Siliprandi, 24-Dec-2020)

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

Proof

Step	Hyp	Ref	Expression
1		caragenel2d.o	|- ( ph -> O e. OutMeas )
2		caragenel2d.x	|- X = U. dom O
3		caragenel2d.s	|- S = ( CaraGen ` O )
4		caragenel2d.e	|- ( ph -> E e. ~P X )
5		caragenel2d.a	|- ( ( ph /\ a e. ~P X ) -> ( ( O ` ( a i^i E ) ) +e ( O ` ( a \ E ) ) ) <_ ( O ` a ) )
6	1	adantr	|- ( ( ph /\ a e. ~P X ) -> O e. OutMeas )
7		inss1	|- ( a i^i E ) C_ a
8		elpwi	|- ( a e. ~P X -> a C_ X )
9	7 8	sstrid	|- ( a e. ~P X -> ( a i^i E ) C_ X )
10	9	adantl	|- ( ( ph /\ a e. ~P X ) -> ( a i^i E ) C_ X )
11	6 2 10	omexrcl	|- ( ( ph /\ a e. ~P X ) -> ( O ` ( a i^i E ) ) e. RR* )
12	8	ssdifssd	|- ( a e. ~P X -> ( a \ E ) C_ X )
13	12	adantl	|- ( ( ph /\ a e. ~P X ) -> ( a \ E ) C_ X )
14	6 2 13	omexrcl	|- ( ( ph /\ a e. ~P X ) -> ( O ` ( a \ E ) ) e. RR* )
15		xaddcl	|- ( ( ( O ` ( a i^i E ) ) e. RR* /\ ( O ` ( a \ E ) ) e. RR* ) -> ( ( O ` ( a i^i E ) ) +e ( O ` ( a \ E ) ) ) e. RR* )
16	11 14 15	syl2anc	|- ( ( ph /\ a e. ~P X ) -> ( ( O ` ( a i^i E ) ) +e ( O ` ( a \ E ) ) ) e. RR* )
17	8	adantl	|- ( ( ph /\ a e. ~P X ) -> a C_ X )
18	6 2 17	omexrcl	|- ( ( ph /\ a e. ~P X ) -> ( O ` a ) e. RR* )
19	6 2 17	omelesplit	|- ( ( ph /\ a e. ~P X ) -> ( O ` a ) <_ ( ( O ` ( a i^i E ) ) +e ( O ` ( a \ E ) ) ) )
20	16 18 5 19	xrletrid	|- ( ( ph /\ a e. ~P X ) -> ( ( O ` ( a i^i E ) ) +e ( O ` ( a \ E ) ) ) = ( O ` a ) )
21	1 2 3 4 20	carageneld	|- ( ph -> E e. S )