Metamath Proof Explorer

Theorem caragenel

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

Ref Expression
Hypotheses caragenel.o ⊢φ→O∈OutMeas
caragenel.s ⊢S=CaraGen⁡O
Assertion caragenel ⊢φ→E∈S↔E∈𝒫⋃dom⁡O∧∀a∈𝒫⋃dom⁡OO⁡a∩E+𝑒O⁡a∖E=O⁡a

Proof

Step Hyp Ref Expression
1 caragenel.o ⊢φ→O∈OutMeas
2 caragenel.s ⊢S=CaraGen⁡O
3 caragenval ⊢O∈OutMeas→CaraGen⁡O=e∈𝒫⋃dom⁡O|∀a∈𝒫⋃dom⁡OO⁡a∩e+𝑒O⁡a∖e=O⁡a
4 1 3 syl ⊢φ→CaraGen⁡O=e∈𝒫⋃dom⁡O|∀a∈𝒫⋃dom⁡OO⁡a∩e+𝑒O⁡a∖e=O⁡a
5 2 4 eqtrid ⊢φ→S=e∈𝒫⋃dom⁡O|∀a∈𝒫⋃dom⁡OO⁡a∩e+𝑒O⁡a∖e=O⁡a
6 5 eleq2d ⊢φ→E∈S↔E∈e∈𝒫⋃dom⁡O|∀a∈𝒫⋃dom⁡OO⁡a∩e+𝑒O⁡a∖e=O⁡a
7 ineq2 ⊢e=E→a∩e=a∩E
8 7 fveq2d ⊢e=E→O⁡a∩e=O⁡a∩E
9 difeq2 ⊢e=E→a∖e=a∖E
10 9 fveq2d ⊢e=E→O⁡a∖e=O⁡a∖E
11 8 10 oveq12d ⊢e=E→O⁡a∩e+𝑒O⁡a∖e=O⁡a∩E+𝑒O⁡a∖E
12 11 eqeq1d ⊢e=E→O⁡a∩e+𝑒O⁡a∖e=O⁡a↔O⁡a∩E+𝑒O⁡a∖E=O⁡a
13 12 ralbidv ⊢e=E→∀a∈𝒫⋃dom⁡OO⁡a∩e+𝑒O⁡a∖e=O⁡a↔∀a∈𝒫⋃dom⁡OO⁡a∩E+𝑒O⁡a∖E=O⁡a
14 13 elrab ⊢E∈e∈𝒫⋃dom⁡O|∀a∈𝒫⋃dom⁡OO⁡a∩e+𝑒O⁡a∖e=O⁡a↔E∈𝒫⋃dom⁡O∧∀a∈𝒫⋃dom⁡OO⁡a∩E+𝑒O⁡a∖E=O⁡a
15 14 a1i ⊢φ→E∈e∈𝒫⋃dom⁡O|∀a∈𝒫⋃dom⁡OO⁡a∩e+𝑒O⁡a∖e=O⁡a↔E∈𝒫⋃dom⁡O∧∀a∈𝒫⋃dom⁡OO⁡a∩E+𝑒O⁡a∖E=O⁡a
16 6 15 bitrd ⊢φ→E∈S↔E∈𝒫⋃dom⁡O∧∀a∈𝒫⋃dom⁡OO⁡a∩E+𝑒O⁡a∖E=O⁡a