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 ⁡ O O ⁡ 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 ⁡ O O ⁡ a ∩ e + 𝑒 O ⁡ a ∖ e = O ⁡ a
4 1 3 syl ⊢ φ → CaraGen ⁡ O = e ∈ 𝒫 ⋃ dom ⁡ O | ∀ a ∈ 𝒫 ⋃ dom ⁡ O O ⁡ a ∩ e + 𝑒 O ⁡ a ∖ e = O ⁡ a
5 2 4 syl5eq ⊢ φ → S = e ∈ 𝒫 ⋃ dom ⁡ O | ∀ a ∈ 𝒫 ⋃ dom ⁡ O O ⁡ a ∩ e + 𝑒 O ⁡ a ∖ e = O ⁡ a
6 5 eleq2d ⊢ φ → E ∈ S ↔ E ∈ e ∈ 𝒫 ⋃ dom ⁡ O | ∀ a ∈ 𝒫 ⋃ dom ⁡ O O ⁡ 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 ⁡ O O ⁡ a ∩ e + 𝑒 O ⁡ a ∖ e = O ⁡ a ↔ ∀ a ∈ 𝒫 ⋃ dom ⁡ O O ⁡ a ∩ E + 𝑒 O ⁡ a ∖ E = O ⁡ a
14 13 elrab ⊢ E ∈ e ∈ 𝒫 ⋃ dom ⁡ O | ∀ a ∈ 𝒫 ⋃ dom ⁡ O O ⁡ a ∩ e + 𝑒 O ⁡ a ∖ e = O ⁡ a ↔ E ∈ 𝒫 ⋃ dom ⁡ O ∧ ∀ a ∈ 𝒫 ⋃ dom ⁡ O O ⁡ a ∩ E + 𝑒 O ⁡ a ∖ E = O ⁡ a
15 14 a1i ⊢ φ → E ∈ e ∈ 𝒫 ⋃ dom ⁡ O | ∀ a ∈ 𝒫 ⋃ dom ⁡ O O ⁡ a ∩ e + 𝑒 O ⁡ a ∖ e = O ⁡ a ↔ E ∈ 𝒫 ⋃ dom ⁡ O ∧ ∀ a ∈ 𝒫 ⋃ dom ⁡ O O ⁡ a ∩ E + 𝑒 O ⁡ a ∖ E = O ⁡ a
16 6 15 bitrd ⊢ φ → E ∈ S ↔ E ∈ 𝒫 ⋃ dom ⁡ O ∧ ∀ a ∈ 𝒫 ⋃ dom ⁡ O O ⁡ a ∩ E + 𝑒 O ⁡ a ∖ E = O ⁡ a