Metamath Proof Explorer


Theorem caragensal

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

Ref Expression
Hypotheses caragensal.o φ O OutMeas
caragensal.s S = CaraGen O
Assertion caragensal φ S SAlg

Proof

Step Hyp Ref Expression
1 caragensal.o φ O OutMeas
2 caragensal.s S = CaraGen O
3 1 2 caragen0 φ S
4 1 adantr φ x S O OutMeas
5 simpr φ x S x S
6 4 2 5 caragendifcl φ x S S x S
7 6 ralrimiva φ x S S x S
8 1 ad2antrr φ x 𝒫 S x ω O OutMeas
9 elpwi x 𝒫 S x S
10 9 ad2antlr φ x 𝒫 S x ω x S
11 simpr φ x 𝒫 S x ω x ω
12 8 2 10 11 caragenunicl φ x 𝒫 S x ω x S
13 12 ex φ x 𝒫 S x ω x S
14 13 ralrimiva φ x 𝒫 S x ω x S
15 3 7 14 3jca φ S x S S x S x 𝒫 S x ω x S
16 2 fvexi S V
17 16 a1i φ S V
18 issal S V S SAlg S x S S x S x 𝒫 S x ω x S
19 17 18 syl φ S SAlg S x S S x S x 𝒫 S x ω x S
20 15 19 mpbird φ S SAlg