Theorem mvrfval

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$$
Assertion	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)$$

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	5	elexd	$$⊢\phi \to I\in \mathrm{V}$$
8	6	elexd	$$⊢\phi \to R\in \mathrm{V}$$
9	5	mptexd	$$⊢\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)\in \mathrm{V}$$
10		simpl	$$⊢\left(i=I\wedge r=R\right)\to i=I$$
11	10	oveq2d	$$⊢\left(i=I\wedge r=R\right)\to {{\mathbb{N}}_0}^i={{\mathbb{N}}_0}^I$$
12	11	rabeqdv	$$⊢\left(i=I\wedge r=R\right)\to \left\{h\in \left({{\mathbb{N}}_0}^i\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
13	12 2	eqtr4di	$$⊢\left(i=I\wedge r=R\right)\to \left\{h\in \left({{\mathbb{N}}_0}^i\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}=D$$
14		mpteq1	$$⊢i=I\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)$$
15	14	adantr	$$⊢\left(i=I\wedge r=R\right)\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)$$
16	15	eqeq2d	$$⊢\left(i=I\wedge r=R\right)\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)$$
17		simpr	$$⊢\left(i=I\wedge r=R\right)\to r=R$$
18	17	fveq2d	$$⊢\left(i=I\wedge r=R\right)\to 1_r=1_R$$
19	18 4	eqtr4di	$$⊢\left(i=I\wedge r=R\right)\to 1_r=\underset{\dot{}}{1}$$
20	17	fveq2d	$$⊢\left(i=I\wedge r=R\right)\to 0_r=0_R$$
21	20 3	eqtr4di	$$⊢\left(i=I\wedge r=R\right)\to 0_r=\underset{\dot{}}{0}$$
22	16 19 21	ifbieq12d	$$⊢\left(i=I\wedge r=R\right)\to if\left(f=\left(y\in i⟼if\left(y=x,1,0\right)\right),1_r,0_r\right)=if\left(f=\left(y\in I⟼if\left(y=x,1,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)$$
23	13 22	mpteq12dv	$$⊢\left(i=I\wedge r=R\right)\to \left(f\in \left\{h\in \left({{\mathbb{N}}_0}^i\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼if\left(f=\left(y\in i⟼if\left(y=x,1,0\right)\right),1_r,0_r\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)$$
24	10 23	mpteq12dv	$$⊢\left(i=I\wedge r=R\right)\to \left(x\in i⟼\left(f\in \left\{h\in \left({{\mathbb{N}}_0}^i\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼if\left(f=\left(y\in i⟼if\left(y=x,1,0\right)\right),1_r,0_r\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)$$
25		df-mvr	$$⊢\mathrm{mVar}=\left(i\in \mathrm{V},r\in \mathrm{V}⟼\left(x\in i⟼\left(f\in \left\{h\in \left({{\mathbb{N}}_0}^i\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼if\left(f=\left(y\in i⟼if\left(y=x,1,0\right)\right),1_r,0_r\right)\right)\right)\right)$$
26	24 25	ovmpoga	$$⊢\left(I\in \mathrm{V}\wedge R\in \mathrm{V}\wedge \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)\in \mathrm{V}\right)\to I\mathrm{mVar}R=\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)$$
27	7 8 9 26	syl3anc	$$⊢\phi \to I\mathrm{mVar}R=\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)$$
28	1 27	syl5eq	$$⊢\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)$$