Theorem carageneld

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

	Ref	Expression
Hypotheses	carageneld.o	⊢ ( 𝜑 → 𝑂 ∈ OutMeas )
	carageneld.x	⊢ 𝑋 = ∪ dom 𝑂
	carageneld.s	⊢ 𝑆 = ( CaraGen ‘ 𝑂 )
	carageneld.e	⊢ ( 𝜑 → 𝐸 ∈ 𝒫 𝑋 )
	carageneld.a	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 𝑋 ) → ( ( 𝑂 ‘ ( 𝑎 ∩ 𝐸 ) ) +𝑒 ( 𝑂 ‘ ( 𝑎 ∖ 𝐸 ) ) ) = ( 𝑂 ‘ 𝑎 ) )
Assertion	carageneld	⊢ ( 𝜑 → 𝐸 ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		carageneld.o	⊢ ( 𝜑 → 𝑂 ∈ OutMeas )
2		carageneld.x	⊢ 𝑋 = ∪ dom 𝑂
3		carageneld.s	⊢ 𝑆 = ( CaraGen ‘ 𝑂 )
4		carageneld.e	⊢ ( 𝜑 → 𝐸 ∈ 𝒫 𝑋 )
5		carageneld.a	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 𝑋 ) → ( ( 𝑂 ‘ ( 𝑎 ∩ 𝐸 ) ) +𝑒 ( 𝑂 ‘ ( 𝑎 ∖ 𝐸 ) ) ) = ( 𝑂 ‘ 𝑎 ) )
6	2	pweqi	⊢ 𝒫 𝑋 = 𝒫 ∪ dom 𝑂
7	4 6	eleqtrdi	⊢ ( 𝜑 → 𝐸 ∈ 𝒫 ∪ dom 𝑂 )
8		simpl	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) → 𝜑 )
9	6	eleq2i	⊢ ( 𝑎 ∈ 𝒫 𝑋 ↔ 𝑎 ∈ 𝒫 ∪ dom 𝑂 )
10	9	bicomi	⊢ ( 𝑎 ∈ 𝒫 ∪ dom 𝑂 ↔ 𝑎 ∈ 𝒫 𝑋 )
11	10	biimpi	⊢ ( 𝑎 ∈ 𝒫 ∪ dom 𝑂 → 𝑎 ∈ 𝒫 𝑋 )
12	11	adantl	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) → 𝑎 ∈ 𝒫 𝑋 )
13	8 12 5	syl2anc	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) → ( ( 𝑂 ‘ ( 𝑎 ∩ 𝐸 ) ) +𝑒 ( 𝑂 ‘ ( 𝑎 ∖ 𝐸 ) ) ) = ( 𝑂 ‘ 𝑎 ) )
14	13	ralrimiva	⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ( ( 𝑂 ‘ ( 𝑎 ∩ 𝐸 ) ) +𝑒 ( 𝑂 ‘ ( 𝑎 ∖ 𝐸 ) ) ) = ( 𝑂 ‘ 𝑎 ) )
15	7 14	jca	⊢ ( 𝜑 → ( 𝐸 ∈ 𝒫 ∪ dom 𝑂 ∧ ∀ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ( ( 𝑂 ‘ ( 𝑎 ∩ 𝐸 ) ) +𝑒 ( 𝑂 ‘ ( 𝑎 ∖ 𝐸 ) ) ) = ( 𝑂 ‘ 𝑎 ) ) )
16	1 3	caragenel	⊢ ( 𝜑 → ( 𝐸 ∈ 𝑆 ↔ ( 𝐸 ∈ 𝒫 ∪ dom 𝑂 ∧ ∀ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ( ( 𝑂 ‘ ( 𝑎 ∩ 𝐸 ) ) +𝑒 ( 𝑂 ‘ ( 𝑎 ∖ 𝐸 ) ) ) = ( 𝑂 ‘ 𝑎 ) ) ) )
17	15 16	mpbird	⊢ ( 𝜑 → 𝐸 ∈ 𝑆 )