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* ` (/) ) = ( x e. ~P { (/) } |-> 0 )

Proof

Step	Hyp	Ref	Expression
1		tru	|- T.
2		0fin	|- (/) e. Fin
3	2	a1i	|- ( T. -> (/) e. Fin )
4	3	ovnf	|- ( T. -> ( voln* ` (/) ) : ~P ( RR ^m (/) ) --> ( 0 [,] +oo ) )
5	4	feqmptd	|- ( T. -> ( voln* ` (/) ) = ( x e. ~P ( RR ^m (/) ) |-> ( ( voln* ` (/) ) ` x ) ) )
6	1 5	ax-mp	|- ( voln* ` (/) ) = ( x e. ~P ( RR ^m (/) ) |-> ( ( voln* ` (/) ) ` x ) )
7		reex	|- RR e. _V
8		mapdm0	|- ( RR e. _V -> ( RR ^m (/) ) = { (/) } )
9	7 8	ax-mp	|- ( RR ^m (/) ) = { (/) }
10	9	pweqi	|- ~P ( RR ^m (/) ) = ~P { (/) }
11		mpteq1	|- ( ~P ( RR ^m (/) ) = ~P { (/) } -> ( x e. ~P ( RR ^m (/) ) |-> ( ( voln* ` (/) ) ` x ) ) = ( x e. ~P { (/) } |-> ( ( voln* ` (/) ) ` x ) ) )
12	10 11	ax-mp	|- ( x e. ~P ( RR ^m (/) ) |-> ( ( voln* ` (/) ) ` x ) ) = ( x e. ~P { (/) } |-> ( ( voln* ` (/) ) ` x ) )
13		elpwi	|- ( x e. ~P { (/) } -> x C_ { (/) } )
14	9	eqcomi	|- { (/) } = ( RR ^m (/) )
15	14	a1i	|- ( x e. ~P { (/) } -> { (/) } = ( RR ^m (/) ) )
16	13 15	sseqtrd	|- ( x e. ~P { (/) } -> x C_ ( RR ^m (/) ) )
17	16	ovn0val	|- ( x e. ~P { (/) } -> ( ( voln* ` (/) ) ` x ) = 0 )
18	17	mpteq2ia	|- ( x e. ~P { (/) } |-> ( ( voln* ` (/) ) ` x ) ) = ( x e. ~P { (/) } |-> 0 )
19	6 12 18	3eqtri	|- ( voln* ` (/) ) = ( x e. ~P { (/) } |-> 0 )