Theorem carsguni

Description: The union of all Caratheodory measurable sets is the universe. (Contributed by Thierry Arnoux, 22-May-2020)

	Ref	Expression
Hypotheses	carsgval.1	⊢ ( 𝜑 → 𝑂 ∈ 𝑉 )
	carsgval.2	⊢ ( 𝜑 → 𝑀 : 𝒫 𝑂 ⟶ ( 0 [,] +∞ ) )
	baselcarsg.1	⊢ ( 𝜑 → ( 𝑀 ‘ ∅ ) = 0 )
Assertion	carsguni	⊢ ( 𝜑 → ∪ ( toCaraSiga ‘ 𝑀 ) = 𝑂 )

Proof

Step	Hyp	Ref	Expression
1		carsgval.1	⊢ ( 𝜑 → 𝑂 ∈ 𝑉 )
2		carsgval.2	⊢ ( 𝜑 → 𝑀 : 𝒫 𝑂 ⟶ ( 0 [,] +∞ ) )
3		baselcarsg.1	⊢ ( 𝜑 → ( 𝑀 ‘ ∅ ) = 0 )
4	1 2	carsgcl	⊢ ( 𝜑 → ( toCaraSiga ‘ 𝑀 ) ⊆ 𝒫 𝑂 )
5	4	sselda	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( toCaraSiga ‘ 𝑀 ) ) → 𝑎 ∈ 𝒫 𝑂 )
6	5	elpwid	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( toCaraSiga ‘ 𝑀 ) ) → 𝑎 ⊆ 𝑂 )
7	6	ralrimiva	⊢ ( 𝜑 → ∀ 𝑎 ∈ ( toCaraSiga ‘ 𝑀 ) 𝑎 ⊆ 𝑂 )
8		unissb	⊢ ( ∪ ( toCaraSiga ‘ 𝑀 ) ⊆ 𝑂 ↔ ∀ 𝑎 ∈ ( toCaraSiga ‘ 𝑀 ) 𝑎 ⊆ 𝑂 )
9	7 8	sylibr	⊢ ( 𝜑 → ∪ ( toCaraSiga ‘ 𝑀 ) ⊆ 𝑂 )
10	1 2 3	baselcarsg	⊢ ( 𝜑 → 𝑂 ∈ ( toCaraSiga ‘ 𝑀 ) )
11		unissel	⊢ ( ( ∪ ( toCaraSiga ‘ 𝑀 ) ⊆ 𝑂 ∧ 𝑂 ∈ ( toCaraSiga ‘ 𝑀 ) ) → ∪ ( toCaraSiga ‘ 𝑀 ) = 𝑂 )
12	9 10 11	syl2anc	⊢ ( 𝜑 → ∪ ( toCaraSiga ‘ 𝑀 ) = 𝑂 )