Definition df-mvr

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmvr	$$class\mathrm{mVar}$$
1		vi	$$setvari$$
2		cvv	$$class\mathrm{V}$$
3		vr	$$setvarr$$
4		vx	$$setvarx$$
5	1	cv	$$setvari$$
6		vf	$$setvarf$$
7		vh	$$setvarh$$
8		cn0	$$class{\mathbb{N}}_0$$
9		cmap	$$class{\uparrow }_{𝑚}$$
10	8 5 9	co	$$class\left({{\mathbb{N}}_0}^i\right)$$
11	7	cv	$$setvarh$$
12	11	ccnv	$$class{h}^{-1}$$
13		cn	$$class\mathbb{N}$$
14	12 13	cima	$$class{h}^{-1}\left[\mathbb{N}\right]$$
15		cfn	$$class\mathrm{Fin}$$
16	14 15	wcel	$$wff{h}^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}$$
17	16 7 10	crab	$$class\left\{h\in \left({{\mathbb{N}}_0}^i\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
18	6	cv	$$setvarf$$
19		vy	$$setvary$$
20	19	cv	$$setvary$$
21	4	cv	$$setvarx$$
22	20 21	wceq	$$wffy=x$$
23		c1	$$class1$$
24		cc0	$$class0$$
25	22 23 24	cif	$$classif\left(y=x,1,0\right)$$
26	19 5 25	cmpt	$$class\left(y\in i⟼if\left(y=x,1,0\right)\right)$$
27	18 26	wceq	$$wfff=\left(y\in i⟼if\left(y=x,1,0\right)\right)$$
28		cur	$$class{1}_r$$
29	3	cv	$$setvarr$$
30	29 28	cfv	$$class{1}_r$$
31		c0g	$$class{0}_{𝑔}$$
32	29 31	cfv	$$class{0}_r$$
33	27 30 32	cif	$$classif\left(f=\left(y\in i⟼if\left(y=x,1,0\right)\right),1_r,0_r\right)$$
34	6 17 33	cmpt	$$class\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)$$
35	4 5 34	cmpt	$$class\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)$$
36	1 3 2 2 35	cmpo	$$class\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)$$
37	0 36	wceq	$$wff\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)$$