caragensal

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

Step	Hyp	Ref	Expression
1		caragensal.o	$⊢ φ \to O \in OutMeas$
2		caragensal.s	$⊢ S = CaraGen (O)$
3	1 2	caragen0	$⊢ φ \to \emptyset \in S$
4	1	adantr	$⊢ (φ \land x \in S) \to O \in OutMeas$
5		simpr	$⊢ (φ \land x \in S) \to x \in S$
6	4 2 5	caragendifcl	$⊢ (φ \land x \in S) \to ⋃ S ∖ x \in S$
7	6	ralrimiva	$⊢ φ \to \forall x \in S ⋃ S ∖ x \in S$
8	1	ad2antrr	$⊢ ((φ \land x \in 𝒫 S) \land x ≼ ω) \to O \in OutMeas$
9		elpwi	$⊢ x \in 𝒫 S \to x \subseteq S$
10	9	ad2antlr	$⊢ ((φ \land x \in 𝒫 S) \land x ≼ ω) \to x \subseteq S$
11		simpr	$⊢ ((φ \land x \in 𝒫 S) \land x ≼ ω) \to x ≼ ω$
12	8 2 10 11	caragenunicl	$⊢ ((φ \land x \in 𝒫 S) \land x ≼ ω) \to ⋃ x \in S$
13	12	ex	$⊢ (φ \land x \in 𝒫 S) \to (x ≼ ω \to ⋃ x \in S)$
14	13	ralrimiva	$⊢ φ \to \forall x \in 𝒫 S (x ≼ ω \to ⋃ x \in S)$
15	3 7 14	3jca	$⊢ φ \to (\emptyset \in S \land \forall x \in S ⋃ S ∖ x \in S \land \forall x \in 𝒫 S (x ≼ ω \to ⋃ x \in S))$
16	2	fvexi	$⊢ S \in V$
17	16	a1i	$⊢ φ \to S \in V$
18		issal	$⊢ S \in V \to (S \in SAlg \leftrightarrow (\emptyset \in S \land \forall x \in S ⋃ S ∖ x \in S \land \forall x \in 𝒫 S (x ≼ ω \to ⋃ x \in S)))$
19	17 18	syl	$⊢ φ \to (S \in SAlg \leftrightarrow (\emptyset \in S \land \forall x \in S ⋃ S ∖ x \in S \land \forall x \in 𝒫 S (x ≼ ω \to ⋃ x \in S)))$
20	15 19	mpbird	$⊢ φ \to S \in SAlg$

Metamath Proof Explorer