Theorem ovn02

Description: For the zero-dimensional space, voln* assigns zero to every subset. (Contributed by Glauco Siliprandi, 11-Oct-2020)

	Ref	Expression
Assertion	ovn02	⊢ ( voln* ‘ ∅ ) = ( 𝑥 ∈ 𝒫 { ∅ } ↦ 0 )

Proof

Step	Hyp	Ref	Expression
1		tru	⊢ ⊤
2		0fi	⊢ ∅ ∈ Fin
3	2	a1i	⊢ ( ⊤ → ∅ ∈ Fin )
4	3	ovnf	⊢ ( ⊤ → ( voln* ‘ ∅ ) : 𝒫 ( ℝ ↑m ∅ ) ⟶ ( 0 [,] +∞ ) )
5	4	feqmptd	⊢ ( ⊤ → ( voln* ‘ ∅ ) = ( 𝑥 ∈ 𝒫 ( ℝ ↑m ∅ ) ↦ ( ( voln* ‘ ∅ ) ‘ 𝑥 ) ) )
6	1 5	ax-mp	⊢ ( voln* ‘ ∅ ) = ( 𝑥 ∈ 𝒫 ( ℝ ↑m ∅ ) ↦ ( ( voln* ‘ ∅ ) ‘ 𝑥 ) )
7		reex	⊢ ℝ ∈ V
8		mapdm0	⊢ ( ℝ ∈ V → ( ℝ ↑m ∅ ) = { ∅ } )
9	7 8	ax-mp	⊢ ( ℝ ↑m ∅ ) = { ∅ }
10	9	pweqi	⊢ 𝒫 ( ℝ ↑m ∅ ) = 𝒫 { ∅ }
11		mpteq1	⊢ ( 𝒫 ( ℝ ↑m ∅ ) = 𝒫 { ∅ } → ( 𝑥 ∈ 𝒫 ( ℝ ↑m ∅ ) ↦ ( ( voln* ‘ ∅ ) ‘ 𝑥 ) ) = ( 𝑥 ∈ 𝒫 { ∅ } ↦ ( ( voln* ‘ ∅ ) ‘ 𝑥 ) ) )
12	10 11	ax-mp	⊢ ( 𝑥 ∈ 𝒫 ( ℝ ↑m ∅ ) ↦ ( ( voln* ‘ ∅ ) ‘ 𝑥 ) ) = ( 𝑥 ∈ 𝒫 { ∅ } ↦ ( ( voln* ‘ ∅ ) ‘ 𝑥 ) )
13		elpwi	⊢ ( 𝑥 ∈ 𝒫 { ∅ } → 𝑥 ⊆ { ∅ } )
14	9	eqcomi	⊢ { ∅ } = ( ℝ ↑m ∅ )
15	14	a1i	⊢ ( 𝑥 ∈ 𝒫 { ∅ } → { ∅ } = ( ℝ ↑m ∅ ) )
16	13 15	sseqtrd	⊢ ( 𝑥 ∈ 𝒫 { ∅ } → 𝑥 ⊆ ( ℝ ↑m ∅ ) )
17	16	ovn0val	⊢ ( 𝑥 ∈ 𝒫 { ∅ } → ( ( voln* ‘ ∅ ) ‘ 𝑥 ) = 0 )
18	17	mpteq2ia	⊢ ( 𝑥 ∈ 𝒫 { ∅ } ↦ ( ( voln* ‘ ∅ ) ‘ 𝑥 ) ) = ( 𝑥 ∈ 𝒫 { ∅ } ↦ 0 )
19	6 12 18	3eqtri	⊢ ( voln* ‘ ∅ ) = ( 𝑥 ∈ 𝒫 { ∅ } ↦ 0 )