Theorem mvrval

Description: Value of the generating elements of the power series structure. (Contributed by Mario Carneiro, 7-Jan-2015)

	Ref	Expression
Hypotheses	mvrfval.v	$$⊢V=I\mathrm{mVar}R$$
	mvrfval.d	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
	mvrfval.z	$$⊢\underset{\dot{}}{0}=0_R$$
	mvrfval.o	$$⊢\underset{\dot{}}{1}=1_R$$
	mvrfval.i	$$⊢\phi \to I\in W$$
	mvrfval.r	$$⊢\phi \to R\in Y$$
	mvrval.x	$$⊢\phi \to X\in I$$
Assertion	mvrval	$$⊢\phi \to V\left(X\right)=\left(f\in D⟼if\left(f=\left(y\in I⟼if\left(y=X,1,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		mvrfval.v	$$⊢V=I\mathrm{mVar}R$$
2		mvrfval.d	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
3		mvrfval.z	$$⊢\underset{\dot{}}{0}=0_R$$
4		mvrfval.o	$$⊢\underset{\dot{}}{1}=1_R$$
5		mvrfval.i	$$⊢\phi \to I\in W$$
6		mvrfval.r	$$⊢\phi \to R\in Y$$
7		mvrval.x	$$⊢\phi \to X\in I$$
8	1 2 3 4 5 6	mvrfval	$$⊢\phi \to V=\left(x\in I⟼\left(f\in D⟼if\left(f=\left(y\in I⟼if\left(y=x,1,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)$$
9	8	fveq1d	$$⊢\phi \to V\left(X\right)=\left(x\in I⟼\left(f\in D⟼if\left(f=\left(y\in I⟼if\left(y=x,1,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)\left(X\right)$$
10		eqeq2	$$⊢x=X\to \left(y=x\leftrightarrow y=X\right)$$
11	10	ifbid	$$⊢x=X\to if\left(y=x,1,0\right)=if\left(y=X,1,0\right)$$
12	11	mpteq2dv	$$⊢x=X\to \left(y\in I⟼if\left(y=x,1,0\right)\right)=\left(y\in I⟼if\left(y=X,1,0\right)\right)$$
13	12	eqeq2d	$$⊢x=X\to \left(f=\left(y\in I⟼if\left(y=x,1,0\right)\right)\leftrightarrow f=\left(y\in I⟼if\left(y=X,1,0\right)\right)\right)$$
14	13	ifbid	$$⊢x=X\to if\left(f=\left(y\in I⟼if\left(y=x,1,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)=if\left(f=\left(y\in I⟼if\left(y=X,1,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)$$
15	14	mpteq2dv	$$⊢x=X\to \left(f\in D⟼if\left(f=\left(y\in I⟼if\left(y=x,1,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\left(f\in D⟼if\left(f=\left(y\in I⟼if\left(y=X,1,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
16		eqid	$$⊢\left(x\in I⟼\left(f\in D⟼if\left(f=\left(y\in I⟼if\left(y=x,1,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)=\left(x\in I⟼\left(f\in D⟼if\left(f=\left(y\in I⟼if\left(y=x,1,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)$$
17		ovex	$$⊢{{\mathbb{N}}_0}^I\in \mathrm{V}$$
18	2 17	rabex2	$$⊢D\in \mathrm{V}$$
19	18	mptex	$$⊢\left(f\in D⟼if\left(f=\left(y\in I⟼if\left(y=X,1,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\in \mathrm{V}$$
20	15 16 19	fvmpt	$$⊢X\in I\to \left(x\in I⟼\left(f\in D⟼if\left(f=\left(y\in I⟼if\left(y=x,1,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)\left(X\right)=\left(f\in D⟼if\left(f=\left(y\in I⟼if\left(y=X,1,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
21	7 20	syl	$$⊢\phi \to \left(x\in I⟼\left(f\in D⟼if\left(f=\left(y\in I⟼if\left(y=x,1,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)\left(X\right)=\left(f\in D⟼if\left(f=\left(y\in I⟼if\left(y=X,1,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
22	9 21	eqtrd	$$⊢\phi \to V\left(X\right)=\left(f\in D⟼if\left(f=\left(y\in I⟼if\left(y=X,1,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$