Theorem caragenval

Description: The sigma-algebra generated by an outer measure. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Assertion	caragenval	⊢ ( 𝑂 ∈ OutMeas → ( CaraGen ‘ 𝑂 ) = { 𝑒 ∈ 𝒫 ∪ dom 𝑂 ∣ ∀ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ( ( 𝑂 ‘ ( 𝑎 ∩ 𝑒 ) ) +𝑒 ( 𝑂 ‘ ( 𝑎 ∖ 𝑒 ) ) ) = ( 𝑂 ‘ 𝑎 ) } )

Proof

Step	Hyp	Ref	Expression
1		id	⊢ ( 𝑂 ∈ OutMeas → 𝑂 ∈ OutMeas )
2		dmexg	⊢ ( 𝑂 ∈ OutMeas → dom 𝑂 ∈ V )
3	2	uniexd	⊢ ( 𝑂 ∈ OutMeas → ∪ dom 𝑂 ∈ V )
4	3	pwexd	⊢ ( 𝑂 ∈ OutMeas → 𝒫 ∪ dom 𝑂 ∈ V )
5		rabexg	⊢ ( 𝒫 ∪ dom 𝑂 ∈ V → { 𝑒 ∈ 𝒫 ∪ dom 𝑂 ∣ ∀ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ( ( 𝑂 ‘ ( 𝑎 ∩ 𝑒 ) ) +𝑒 ( 𝑂 ‘ ( 𝑎 ∖ 𝑒 ) ) ) = ( 𝑂 ‘ 𝑎 ) } ∈ V )
6	4 5	syl	⊢ ( 𝑂 ∈ OutMeas → { 𝑒 ∈ 𝒫 ∪ dom 𝑂 ∣ ∀ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ( ( 𝑂 ‘ ( 𝑎 ∩ 𝑒 ) ) +𝑒 ( 𝑂 ‘ ( 𝑎 ∖ 𝑒 ) ) ) = ( 𝑂 ‘ 𝑎 ) } ∈ V )
7		dmeq	⊢ ( 𝑜 = 𝑂 → dom 𝑜 = dom 𝑂 )
8	7	unieqd	⊢ ( 𝑜 = 𝑂 → ∪ dom 𝑜 = ∪ dom 𝑂 )
9	8	pweqd	⊢ ( 𝑜 = 𝑂 → 𝒫 ∪ dom 𝑜 = 𝒫 ∪ dom 𝑂 )
10	9	raleqdv	⊢ ( 𝑜 = 𝑂 → ( ∀ 𝑎 ∈ 𝒫 ∪ dom 𝑜 ( ( 𝑜 ‘ ( 𝑎 ∩ 𝑒 ) ) +𝑒 ( 𝑜 ‘ ( 𝑎 ∖ 𝑒 ) ) ) = ( 𝑜 ‘ 𝑎 ) ↔ ∀ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ( ( 𝑜 ‘ ( 𝑎 ∩ 𝑒 ) ) +𝑒 ( 𝑜 ‘ ( 𝑎 ∖ 𝑒 ) ) ) = ( 𝑜 ‘ 𝑎 ) ) )
11		fveq1	⊢ ( 𝑜 = 𝑂 → ( 𝑜 ‘ ( 𝑎 ∩ 𝑒 ) ) = ( 𝑂 ‘ ( 𝑎 ∩ 𝑒 ) ) )
12		fveq1	⊢ ( 𝑜 = 𝑂 → ( 𝑜 ‘ ( 𝑎 ∖ 𝑒 ) ) = ( 𝑂 ‘ ( 𝑎 ∖ 𝑒 ) ) )
13	11 12	oveq12d	⊢ ( 𝑜 = 𝑂 → ( ( 𝑜 ‘ ( 𝑎 ∩ 𝑒 ) ) +𝑒 ( 𝑜 ‘ ( 𝑎 ∖ 𝑒 ) ) ) = ( ( 𝑂 ‘ ( 𝑎 ∩ 𝑒 ) ) +𝑒 ( 𝑂 ‘ ( 𝑎 ∖ 𝑒 ) ) ) )
14		fveq1	⊢ ( 𝑜 = 𝑂 → ( 𝑜 ‘ 𝑎 ) = ( 𝑂 ‘ 𝑎 ) )
15	13 14	eqeq12d	⊢ ( 𝑜 = 𝑂 → ( ( ( 𝑜 ‘ ( 𝑎 ∩ 𝑒 ) ) +𝑒 ( 𝑜 ‘ ( 𝑎 ∖ 𝑒 ) ) ) = ( 𝑜 ‘ 𝑎 ) ↔ ( ( 𝑂 ‘ ( 𝑎 ∩ 𝑒 ) ) +𝑒 ( 𝑂 ‘ ( 𝑎 ∖ 𝑒 ) ) ) = ( 𝑂 ‘ 𝑎 ) ) )
16	15	ralbidv	⊢ ( 𝑜 = 𝑂 → ( ∀ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ( ( 𝑜 ‘ ( 𝑎 ∩ 𝑒 ) ) +𝑒 ( 𝑜 ‘ ( 𝑎 ∖ 𝑒 ) ) ) = ( 𝑜 ‘ 𝑎 ) ↔ ∀ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ( ( 𝑂 ‘ ( 𝑎 ∩ 𝑒 ) ) +𝑒 ( 𝑂 ‘ ( 𝑎 ∖ 𝑒 ) ) ) = ( 𝑂 ‘ 𝑎 ) ) )
17	10 16	bitrd	⊢ ( 𝑜 = 𝑂 → ( ∀ 𝑎 ∈ 𝒫 ∪ dom 𝑜 ( ( 𝑜 ‘ ( 𝑎 ∩ 𝑒 ) ) +𝑒 ( 𝑜 ‘ ( 𝑎 ∖ 𝑒 ) ) ) = ( 𝑜 ‘ 𝑎 ) ↔ ∀ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ( ( 𝑂 ‘ ( 𝑎 ∩ 𝑒 ) ) +𝑒 ( 𝑂 ‘ ( 𝑎 ∖ 𝑒 ) ) ) = ( 𝑂 ‘ 𝑎 ) ) )
18	9 17	rabeqbidv	⊢ ( 𝑜 = 𝑂 → { 𝑒 ∈ 𝒫 ∪ dom 𝑜 ∣ ∀ 𝑎 ∈ 𝒫 ∪ dom 𝑜 ( ( 𝑜 ‘ ( 𝑎 ∩ 𝑒 ) ) +𝑒 ( 𝑜 ‘ ( 𝑎 ∖ 𝑒 ) ) ) = ( 𝑜 ‘ 𝑎 ) } = { 𝑒 ∈ 𝒫 ∪ dom 𝑂 ∣ ∀ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ( ( 𝑂 ‘ ( 𝑎 ∩ 𝑒 ) ) +𝑒 ( 𝑂 ‘ ( 𝑎 ∖ 𝑒 ) ) ) = ( 𝑂 ‘ 𝑎 ) } )
19		df-caragen	⊢ CaraGen = ( 𝑜 ∈ OutMeas ↦ { 𝑒 ∈ 𝒫 ∪ dom 𝑜 ∣ ∀ 𝑎 ∈ 𝒫 ∪ dom 𝑜 ( ( 𝑜 ‘ ( 𝑎 ∩ 𝑒 ) ) +𝑒 ( 𝑜 ‘ ( 𝑎 ∖ 𝑒 ) ) ) = ( 𝑜 ‘ 𝑎 ) } )
20	18 19	fvmptg	⊢ ( ( 𝑂 ∈ OutMeas ∧ { 𝑒 ∈ 𝒫 ∪ dom 𝑂 ∣ ∀ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ( ( 𝑂 ‘ ( 𝑎 ∩ 𝑒 ) ) +𝑒 ( 𝑂 ‘ ( 𝑎 ∖ 𝑒 ) ) ) = ( 𝑂 ‘ 𝑎 ) } ∈ V ) → ( CaraGen ‘ 𝑂 ) = { 𝑒 ∈ 𝒫 ∪ dom 𝑂 ∣ ∀ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ( ( 𝑂 ‘ ( 𝑎 ∩ 𝑒 ) ) +𝑒 ( 𝑂 ‘ ( 𝑎 ∖ 𝑒 ) ) ) = ( 𝑂 ‘ 𝑎 ) } )
21	1 6 20	syl2anc	⊢ ( 𝑂 ∈ OutMeas → ( CaraGen ‘ 𝑂 ) = { 𝑒 ∈ 𝒫 ∪ dom 𝑂 ∣ ∀ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ( ( 𝑂 ‘ ( 𝑎 ∩ 𝑒 ) ) +𝑒 ( 𝑂 ‘ ( 𝑎 ∖ 𝑒 ) ) ) = ( 𝑂 ‘ 𝑎 ) } )