Theorem caragencmpl

Description: A measure built with the Caratheodory's construction is complete. See Definition 112Df of Fremlin1 p. 19. This is Exercise 113Xa of Fremlin1 p. 21. (Contributed by Glauco Siliprandi, 24-Dec-2020)

	Ref	Expression
Hypotheses	caragencmpl.o	|- ( ph -> O e. OutMeas )
	caragencmpl.x	|- X = U. dom O
	caragencmpl.e	|- ( ph -> E C_ X )
	caragencmpl.z	|- ( ph -> ( O ` E ) = 0 )
	caragencmpl.s	|- S = ( CaraGen ` O )
Assertion	caragencmpl	|- ( ph -> E e. S )

Proof

Step	Hyp	Ref	Expression
1		caragencmpl.o	|- ( ph -> O e. OutMeas )
2		caragencmpl.x	|- X = U. dom O
3		caragencmpl.e	|- ( ph -> E C_ X )
4		caragencmpl.z	|- ( ph -> ( O ` E ) = 0 )
5		caragencmpl.s	|- S = ( CaraGen ` O )
6	1 2	unidmex	|- ( ph -> X e. _V )
7	6 3	ssexd	|- ( ph -> E e. _V )
8		elpwg	|- ( E e. _V -> ( E e. ~P X <-> E C_ X ) )
9	7 8	syl	|- ( ph -> ( E e. ~P X <-> E C_ X ) )
10	3 9	mpbird	|- ( ph -> E e. ~P X )
11	1	adantr	|- ( ( ph /\ a e. ~P X ) -> O e. OutMeas )
12	3	adantr	|- ( ( ph /\ a e. ~P X ) -> E C_ X )
13	4	adantr	|- ( ( ph /\ a e. ~P X ) -> ( O ` E ) = 0 )
14		inss2	|- ( a i^i E ) C_ E
15	14	a1i	|- ( ( ph /\ a e. ~P X ) -> ( a i^i E ) C_ E )
16	11 2 12 13 15	omess0	|- ( ( ph /\ a e. ~P X ) -> ( O ` ( a i^i E ) ) = 0 )
17	16	oveq1d	|- ( ( ph /\ a e. ~P X ) -> ( ( O ` ( a i^i E ) ) +e ( O ` ( a \ E ) ) ) = ( 0 +e ( O ` ( a \ E ) ) ) )
18		difssd	|- ( a e. ~P X -> ( a \ E ) C_ a )
19		elpwi	|- ( a e. ~P X -> a C_ X )
20	18 19	sstrd	|- ( a e. ~P X -> ( a \ E ) C_ X )
21	20	adantl	|- ( ( ph /\ a e. ~P X ) -> ( a \ E ) C_ X )
22	11 2 21	omexrcl	|- ( ( ph /\ a e. ~P X ) -> ( O ` ( a \ E ) ) e. RR* )
23		xaddid2	|- ( ( O ` ( a \ E ) ) e. RR* -> ( 0 +e ( O ` ( a \ E ) ) ) = ( O ` ( a \ E ) ) )
24	22 23	syl	|- ( ( ph /\ a e. ~P X ) -> ( 0 +e ( O ` ( a \ E ) ) ) = ( O ` ( a \ E ) ) )
25	17 24	eqtrd	|- ( ( ph /\ a e. ~P X ) -> ( ( O ` ( a i^i E ) ) +e ( O ` ( a \ E ) ) ) = ( O ` ( a \ E ) ) )
26	19	adantl	|- ( ( ph /\ a e. ~P X ) -> a C_ X )
27	18	adantl	|- ( ( ph /\ a e. ~P X ) -> ( a \ E ) C_ a )
28	11 2 26 27	omessle	|- ( ( ph /\ a e. ~P X ) -> ( O ` ( a \ E ) ) <_ ( O ` a ) )
29	25 28	eqbrtrd	|- ( ( ph /\ a e. ~P X ) -> ( ( O ` ( a i^i E ) ) +e ( O ` ( a \ E ) ) ) <_ ( O ` a ) )
30	1 2 5 10 29	caragenel2d	|- ( ph -> E e. S )