Theorem caragensal

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

	Ref	Expression
Hypotheses	caragensal.o	⊢ ( 𝜑 → 𝑂 ∈ OutMeas )
	caragensal.s	⊢ 𝑆 = ( CaraGen ‘ 𝑂 )
Assertion	caragensal	⊢ ( 𝜑 → 𝑆 ∈ SAlg )

Proof

Step	Hyp	Ref	Expression
1		caragensal.o	⊢ ( 𝜑 → 𝑂 ∈ OutMeas )
2		caragensal.s	⊢ 𝑆 = ( CaraGen ‘ 𝑂 )
3	1 2	caragen0	⊢ ( 𝜑 → ∅ ∈ 𝑆 )
4	1	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝑂 ∈ OutMeas )
5		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ 𝑆 )
6	4 2 5	caragendifcl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( ∪ 𝑆 ∖ 𝑥 ) ∈ 𝑆 )
7	6	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑆 ( ∪ 𝑆 ∖ 𝑥 ) ∈ 𝑆 )
8	1	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 𝑆 ) ∧ 𝑥 ≼ ω ) → 𝑂 ∈ OutMeas )
9		elpwi	⊢ ( 𝑥 ∈ 𝒫 𝑆 → 𝑥 ⊆ 𝑆 )
10	9	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 𝑆 ) ∧ 𝑥 ≼ ω ) → 𝑥 ⊆ 𝑆 )
11		simpr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 𝑆 ) ∧ 𝑥 ≼ ω ) → 𝑥 ≼ ω )
12	8 2 10 11	caragenunicl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 𝑆 ) ∧ 𝑥 ≼ ω ) → ∪ 𝑥 ∈ 𝑆 )
13	12	ex	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 𝑆 ) → ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) )
14	13	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) )
15	3 7 14	3jca	⊢ ( 𝜑 → ( ∅ ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( ∪ 𝑆 ∖ 𝑥 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) ) )
16	2	fvexi	⊢ 𝑆 ∈ V
17	16	a1i	⊢ ( 𝜑 → 𝑆 ∈ V )
18		issal	⊢ ( 𝑆 ∈ V → ( 𝑆 ∈ SAlg ↔ ( ∅ ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( ∪ 𝑆 ∖ 𝑥 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) ) ) )
19	17 18	syl	⊢ ( 𝜑 → ( 𝑆 ∈ SAlg ↔ ( ∅ ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( ∪ 𝑆 ∖ 𝑥 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) ) ) )
20	15 19	mpbird	⊢ ( 𝜑 → 𝑆 ∈ SAlg )