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* (\emptyset) = (x \in 𝒫 \{\emptyset\} ⟼ 0)$

Step	Hyp	Ref	Expression
1		tru	$⊢ ⊤$
2		0fin	$⊢ \emptyset \in Fin$
3	2	a1i	$⊢ ⊤ \to \emptyset \in Fin$
4	3	ovnf	$⊢ ⊤ \to voln* (\emptyset) : 𝒫 (ℝ^{\emptyset}) ⟶ [0, +∞]$
5	4	feqmptd	$⊢ ⊤ \to voln* (\emptyset) = (x \in 𝒫 (ℝ^{\emptyset}) ⟼ voln* (\emptyset) (x))$
6	1 5	ax-mp	$⊢ voln* (\emptyset) = (x \in 𝒫 (ℝ^{\emptyset}) ⟼ voln* (\emptyset) (x))$
7		reex	$⊢ ℝ \in V$
8		mapdm0	$⊢ ℝ \in V \to ℝ^{\emptyset} = \{\emptyset\}$
9	7 8	ax-mp	$⊢ ℝ^{\emptyset} = \{\emptyset\}$
10	9	pweqi	$⊢ 𝒫 (ℝ^{\emptyset}) = 𝒫 \{\emptyset\}$
11		mpteq1	$⊢ 𝒫 (ℝ^{\emptyset}) = 𝒫 \{\emptyset\} \to (x \in 𝒫 (ℝ^{\emptyset}) ⟼ voln* (\emptyset) (x)) = (x \in 𝒫 \{\emptyset\} ⟼ voln* (\emptyset) (x))$
12	10 11	ax-mp	$⊢ (x \in 𝒫 (ℝ^{\emptyset}) ⟼ voln* (\emptyset) (x)) = (x \in 𝒫 \{\emptyset\} ⟼ voln* (\emptyset) (x))$
13		elpwi	$⊢ x \in 𝒫 \{\emptyset\} \to x \subseteq \{\emptyset\}$
14	9	eqcomi	$⊢ \{\emptyset\} = ℝ^{\emptyset}$
15	14	a1i	$⊢ x \in 𝒫 \{\emptyset\} \to \{\emptyset\} = ℝ^{\emptyset}$
16	13 15	sseqtrd	$⊢ x \in 𝒫 \{\emptyset\} \to x \subseteq ℝ^{\emptyset}$
17	16	ovn0val	$⊢ x \in 𝒫 \{\emptyset\} \to voln* (\emptyset) (x) = 0$
18	17	mpteq2ia	$⊢ (x \in 𝒫 \{\emptyset\} ⟼ voln* (\emptyset) (x)) = (x \in 𝒫 \{\emptyset\} ⟼ 0)$
19	6 12 18	3eqtri	$⊢ voln* (\emptyset) = (x \in 𝒫 \{\emptyset\} ⟼ 0)$

Metamath Proof Explorer