This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ovolcl

Description: The volume of a set is an extended real number. (Contributed by Mario Carneiro, 16-Mar-2014)

		Ref	Expression
	Assertion	ovolcl	⊢ ( 𝐴 ⊆ ℝ → ( vol* ‘ 𝐴 ) ∈ ℝ^* )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ { 𝑦 ∈ ℝ^* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ^* , < ) ) } = { 𝑦 ∈ ℝ^* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ^* , < ) ) }
2	1	ovolval	⊢ ( 𝐴 ⊆ ℝ → ( vol* ‘ 𝐴 ) = inf ( { 𝑦 ∈ ℝ^* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ^* , < ) ) } , ℝ^* , < ) )
3		ssrab2	⊢ { 𝑦 ∈ ℝ^* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ^* , < ) ) } ⊆ ℝ^*
4		infxrcl	⊢ ( { 𝑦 ∈ ℝ^* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ^* , < ) ) } ⊆ ℝ^* → inf ( { 𝑦 ∈ ℝ^* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ^* , < ) ) } , ℝ^* , < ) ∈ ℝ^* )
5	3 4	ax-mp	⊢ inf ( { 𝑦 ∈ ℝ^* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ^* , < ) ) } , ℝ^* , < ) ∈ ℝ^*
6	2 5	eqeltrdi	⊢ ( 𝐴 ⊆ ℝ → ( vol* ‘ 𝐴 ) ∈ ℝ^* )