Theorem caragensal

Description: Caratheodory's method generates a sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	caragensal.o	|- ( ph -> O e. OutMeas )
	caragensal.s	|- S = ( CaraGen ` O )
Assertion	caragensal	|- ( ph -> S e. SAlg )

Proof

Step	Hyp	Ref	Expression
1		caragensal.o	|- ( ph -> O e. OutMeas )
2		caragensal.s	|- S = ( CaraGen ` O )
3	1 2	caragen0	|- ( ph -> (/) e. S )
4	1	adantr	|- ( ( ph /\ x e. S ) -> O e. OutMeas )
5		simpr	|- ( ( ph /\ x e. S ) -> x e. S )
6	4 2 5	caragendifcl	|- ( ( ph /\ x e. S ) -> ( U. S \ x ) e. S )
7	6	ralrimiva	|- ( ph -> A. x e. S ( U. S \ x ) e. S )
8	1	ad2antrr	|- ( ( ( ph /\ x e. ~P S ) /\ x ~<_ _om ) -> O e. OutMeas )
9		elpwi	|- ( x e. ~P S -> x C_ S )
10	9	ad2antlr	|- ( ( ( ph /\ x e. ~P S ) /\ x ~<_ _om ) -> x C_ S )
11		simpr	|- ( ( ( ph /\ x e. ~P S ) /\ x ~<_ _om ) -> x ~<_ _om )
12	8 2 10 11	caragenunicl	|- ( ( ( ph /\ x e. ~P S ) /\ x ~<_ _om ) -> U. x e. S )
13	12	ex	|- ( ( ph /\ x e. ~P S ) -> ( x ~<_ _om -> U. x e. S ) )
14	13	ralrimiva	|- ( ph -> A. x e. ~P S ( x ~<_ _om -> U. x e. S ) )
15	3 7 14	3jca	|- ( ph -> ( (/) e. S /\ A. x e. S ( U. S \ x ) e. S /\ A. x e. ~P S ( x ~<_ _om -> U. x e. S ) ) )
16	2	fvexi	|- S e. _V
17	16	a1i	|- ( ph -> S e. _V )
18		issal	|- ( S e. _V -> ( S e. SAlg <-> ( (/) e. S /\ A. x e. S ( U. S \ x ) e. S /\ A. x e. ~P S ( x ~<_ _om -> U. x e. S ) ) ) )
19	17 18	syl	|- ( ph -> ( S e. SAlg <-> ( (/) e. S /\ A. x e. S ( U. S \ x ) e. S /\ A. x e. ~P S ( x ~<_ _om -> U. x e. S ) ) ) )
20	15 19	mpbird	|- ( ph -> S e. SAlg )