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	⊢ mVar = ( 𝑖 ∈ V , 𝑟 ∈ V ↦ ( 𝑥 ∈ 𝑖 ↦ ( 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑓 = ( 𝑦 ∈ 𝑖 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) , ( 1r ‘ 𝑟 ) , ( 0g ‘ 𝑟 ) ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmvr	⊢ mVar
1		vi	⊢ 𝑖
2		cvv	⊢ V
3		vr	⊢ 𝑟
4		vx	⊢ 𝑥
5	1	cv	⊢ 𝑖
6		vf	⊢ 𝑓
7		vh	⊢ ℎ
8		cn0	⊢ ℕ0
9		cmap	⊢ ↑m
10	8 5 9	co	⊢ ( ℕ0 ↑m 𝑖 )
11	7	cv	⊢ ℎ
12	11	ccnv	⊢ ◡ ℎ
13		cn	⊢ ℕ
14	12 13	cima	⊢ ( ◡ ℎ “ ℕ )
15		cfn	⊢ Fin
16	14 15	wcel	⊢ ( ◡ ℎ “ ℕ ) ∈ Fin
17	16 7 10	crab	⊢ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
18	6	cv	⊢ 𝑓
19		vy	⊢ 𝑦
20	19	cv	⊢ 𝑦
21	4	cv	⊢ 𝑥
22	20 21	wceq	⊢ 𝑦 = 𝑥
23		c1	⊢ 1
24		cc0	⊢ 0
25	22 23 24	cif	⊢ if ( 𝑦 = 𝑥 , 1 , 0 )
26	19 5 25	cmpt	⊢ ( 𝑦 ∈ 𝑖 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) )
27	18 26	wceq	⊢ 𝑓 = ( 𝑦 ∈ 𝑖 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) )
28		cur	⊢ 1r
29	3	cv	⊢ 𝑟
30	29 28	cfv	⊢ ( 1r ‘ 𝑟 )
31		c0g	⊢ 0g
32	29 31	cfv	⊢ ( 0g ‘ 𝑟 )
33	27 30 32	cif	⊢ if ( 𝑓 = ( 𝑦 ∈ 𝑖 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) , ( 1r ‘ 𝑟 ) , ( 0g ‘ 𝑟 ) )
34	6 17 33	cmpt	⊢ ( 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑓 = ( 𝑦 ∈ 𝑖 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) , ( 1r ‘ 𝑟 ) , ( 0g ‘ 𝑟 ) ) )
35	4 5 34	cmpt	⊢ ( 𝑥 ∈ 𝑖 ↦ ( 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑓 = ( 𝑦 ∈ 𝑖 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) , ( 1r ‘ 𝑟 ) , ( 0g ‘ 𝑟 ) ) ) )
36	1 3 2 2 35	cmpo	⊢ ( 𝑖 ∈ V , 𝑟 ∈ V ↦ ( 𝑥 ∈ 𝑖 ↦ ( 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑓 = ( 𝑦 ∈ 𝑖 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) , ( 1r ‘ 𝑟 ) , ( 0g ‘ 𝑟 ) ) ) ) )
37	0 36	wceq	⊢ mVar = ( 𝑖 ∈ V , 𝑟 ∈ V ↦ ( 𝑥 ∈ 𝑖 ↦ ( 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑓 = ( 𝑦 ∈ 𝑖 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) , ( 1r ‘ 𝑟 ) , ( 0g ‘ 𝑟 ) ) ) ) )