Theorem caragenelss

Description: An element of the Caratheodory's construction is a subset of the base set of the outer measure. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	caragenelss.o	⊢ ( 𝜑 → 𝑂 ∈ OutMeas )
	caragenelss.s	⊢ 𝑆 = ( CaraGen ‘ 𝑂 )
	caragenelss.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑆 )
	caragenelss.x	⊢ 𝑋 = ∪ dom 𝑂
Assertion	caragenelss	⊢ ( 𝜑 → 𝐴 ⊆ 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		caragenelss.o	⊢ ( 𝜑 → 𝑂 ∈ OutMeas )
2		caragenelss.s	⊢ 𝑆 = ( CaraGen ‘ 𝑂 )
3		caragenelss.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑆 )
4		caragenelss.x	⊢ 𝑋 = ∪ dom 𝑂
5	1 2	caragenel	⊢ ( 𝜑 → ( 𝐴 ∈ 𝑆 ↔ ( 𝐴 ∈ 𝒫 ∪ dom 𝑂 ∧ ∀ 𝑥 ∈ 𝒫 ∪ dom 𝑂 ( ( 𝑂 ‘ ( 𝑥 ∩ 𝐴 ) ) +e ( 𝑂 ‘ ( 𝑥 ∖ 𝐴 ) ) ) = ( 𝑂 ‘ 𝑥 ) ) ) )
6	3 5	mpbid	⊢ ( 𝜑 → ( 𝐴 ∈ 𝒫 ∪ dom 𝑂 ∧ ∀ 𝑥 ∈ 𝒫 ∪ dom 𝑂 ( ( 𝑂 ‘ ( 𝑥 ∩ 𝐴 ) ) +e ( 𝑂 ‘ ( 𝑥 ∖ 𝐴 ) ) ) = ( 𝑂 ‘ 𝑥 ) ) )
7	6	simpld	⊢ ( 𝜑 → 𝐴 ∈ 𝒫 ∪ dom 𝑂 )
8	4	eqcomi	⊢ ∪ dom 𝑂 = 𝑋
9	8	pweqi	⊢ 𝒫 ∪ dom 𝑂 = 𝒫 𝑋
10	9	a1i	⊢ ( 𝜑 → 𝒫 ∪ dom 𝑂 = 𝒫 𝑋 )
11	7 10	eleqtrd	⊢ ( 𝜑 → 𝐴 ∈ 𝒫 𝑋 )
12		elpwg	⊢ ( 𝐴 ∈ 𝑆 → ( 𝐴 ∈ 𝒫 𝑋 ↔ 𝐴 ⊆ 𝑋 ) )
13	3 12	syl	⊢ ( 𝜑 → ( 𝐴 ∈ 𝒫 𝑋 ↔ 𝐴 ⊆ 𝑋 ) )
14	11 13	mpbid	⊢ ( 𝜑 → 𝐴 ⊆ 𝑋 )