Theorem caragenel

Description: Membership in the Caratheodory's construction. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	caragenel.o	⊢ ( 𝜑 → 𝑂 ∈ OutMeas )
	caragenel.s	⊢ 𝑆 = ( CaraGen ‘ 𝑂 )
Assertion	caragenel	⊢ ( 𝜑 → ( 𝐸 ∈ 𝑆 ↔ ( 𝐸 ∈ 𝒫 ∪ dom 𝑂 ∧ ∀ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ( ( 𝑂 ‘ ( 𝑎 ∩ 𝐸 ) ) +𝑒 ( 𝑂 ‘ ( 𝑎 ∖ 𝐸 ) ) ) = ( 𝑂 ‘ 𝑎 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		caragenel.o	⊢ ( 𝜑 → 𝑂 ∈ OutMeas )
2		caragenel.s	⊢ 𝑆 = ( CaraGen ‘ 𝑂 )
3		caragenval	⊢ ( 𝑂 ∈ OutMeas → ( CaraGen ‘ 𝑂 ) = { 𝑒 ∈ 𝒫 ∪ dom 𝑂 ∣ ∀ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ( ( 𝑂 ‘ ( 𝑎 ∩ 𝑒 ) ) +𝑒 ( 𝑂 ‘ ( 𝑎 ∖ 𝑒 ) ) ) = ( 𝑂 ‘ 𝑎 ) } )
4	1 3	syl	⊢ ( 𝜑 → ( CaraGen ‘ 𝑂 ) = { 𝑒 ∈ 𝒫 ∪ dom 𝑂 ∣ ∀ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ( ( 𝑂 ‘ ( 𝑎 ∩ 𝑒 ) ) +𝑒 ( 𝑂 ‘ ( 𝑎 ∖ 𝑒 ) ) ) = ( 𝑂 ‘ 𝑎 ) } )
5	2 4	syl5eq	⊢ ( 𝜑 → 𝑆 = { 𝑒 ∈ 𝒫 ∪ dom 𝑂 ∣ ∀ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ( ( 𝑂 ‘ ( 𝑎 ∩ 𝑒 ) ) +𝑒 ( 𝑂 ‘ ( 𝑎 ∖ 𝑒 ) ) ) = ( 𝑂 ‘ 𝑎 ) } )
6	5	eleq2d	⊢ ( 𝜑 → ( 𝐸 ∈ 𝑆 ↔ 𝐸 ∈ { 𝑒 ∈ 𝒫 ∪ dom 𝑂 ∣ ∀ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ( ( 𝑂 ‘ ( 𝑎 ∩ 𝑒 ) ) +𝑒 ( 𝑂 ‘ ( 𝑎 ∖ 𝑒 ) ) ) = ( 𝑂 ‘ 𝑎 ) } ) )
7		ineq2	⊢ ( 𝑒 = 𝐸 → ( 𝑎 ∩ 𝑒 ) = ( 𝑎 ∩ 𝐸 ) )
8	7	fveq2d	⊢ ( 𝑒 = 𝐸 → ( 𝑂 ‘ ( 𝑎 ∩ 𝑒 ) ) = ( 𝑂 ‘ ( 𝑎 ∩ 𝐸 ) ) )
9		difeq2	⊢ ( 𝑒 = 𝐸 → ( 𝑎 ∖ 𝑒 ) = ( 𝑎 ∖ 𝐸 ) )
10	9	fveq2d	⊢ ( 𝑒 = 𝐸 → ( 𝑂 ‘ ( 𝑎 ∖ 𝑒 ) ) = ( 𝑂 ‘ ( 𝑎 ∖ 𝐸 ) ) )
11	8 10	oveq12d	⊢ ( 𝑒 = 𝐸 → ( ( 𝑂 ‘ ( 𝑎 ∩ 𝑒 ) ) +𝑒 ( 𝑂 ‘ ( 𝑎 ∖ 𝑒 ) ) ) = ( ( 𝑂 ‘ ( 𝑎 ∩ 𝐸 ) ) +𝑒 ( 𝑂 ‘ ( 𝑎 ∖ 𝐸 ) ) ) )
12	11	eqeq1d	⊢ ( 𝑒 = 𝐸 → ( ( ( 𝑂 ‘ ( 𝑎 ∩ 𝑒 ) ) +𝑒 ( 𝑂 ‘ ( 𝑎 ∖ 𝑒 ) ) ) = ( 𝑂 ‘ 𝑎 ) ↔ ( ( 𝑂 ‘ ( 𝑎 ∩ 𝐸 ) ) +𝑒 ( 𝑂 ‘ ( 𝑎 ∖ 𝐸 ) ) ) = ( 𝑂 ‘ 𝑎 ) ) )
13	12	ralbidv	⊢ ( 𝑒 = 𝐸 → ( ∀ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ( ( 𝑂 ‘ ( 𝑎 ∩ 𝑒 ) ) +𝑒 ( 𝑂 ‘ ( 𝑎 ∖ 𝑒 ) ) ) = ( 𝑂 ‘ 𝑎 ) ↔ ∀ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ( ( 𝑂 ‘ ( 𝑎 ∩ 𝐸 ) ) +𝑒 ( 𝑂 ‘ ( 𝑎 ∖ 𝐸 ) ) ) = ( 𝑂 ‘ 𝑎 ) ) )
14	13	elrab	⊢ ( 𝐸 ∈ { 𝑒 ∈ 𝒫 ∪ dom 𝑂 ∣ ∀ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ( ( 𝑂 ‘ ( 𝑎 ∩ 𝑒 ) ) +𝑒 ( 𝑂 ‘ ( 𝑎 ∖ 𝑒 ) ) ) = ( 𝑂 ‘ 𝑎 ) } ↔ ( 𝐸 ∈ 𝒫 ∪ dom 𝑂 ∧ ∀ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ( ( 𝑂 ‘ ( 𝑎 ∩ 𝐸 ) ) +𝑒 ( 𝑂 ‘ ( 𝑎 ∖ 𝐸 ) ) ) = ( 𝑂 ‘ 𝑎 ) ) )
15	14	a1i	⊢ ( 𝜑 → ( 𝐸 ∈ { 𝑒 ∈ 𝒫 ∪ dom 𝑂 ∣ ∀ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ( ( 𝑂 ‘ ( 𝑎 ∩ 𝑒 ) ) +𝑒 ( 𝑂 ‘ ( 𝑎 ∖ 𝑒 ) ) ) = ( 𝑂 ‘ 𝑎 ) } ↔ ( 𝐸 ∈ 𝒫 ∪ dom 𝑂 ∧ ∀ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ( ( 𝑂 ‘ ( 𝑎 ∩ 𝐸 ) ) +𝑒 ( 𝑂 ‘ ( 𝑎 ∖ 𝐸 ) ) ) = ( 𝑂 ‘ 𝑎 ) ) ) )
16	6 15	bitrd	⊢ ( 𝜑 → ( 𝐸 ∈ 𝑆 ↔ ( 𝐸 ∈ 𝒫 ∪ dom 𝑂 ∧ ∀ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ( ( 𝑂 ‘ ( 𝑎 ∩ 𝐸 ) ) +𝑒 ( 𝑂 ‘ ( 𝑎 ∖ 𝐸 ) ) ) = ( 𝑂 ‘ 𝑎 ) ) ) )