Definition df-exp 4676

Description: Define exponentiation to natural number powers. This definition is not intended to be used directly. Instead, exp1t 4679 and expp1t 4678 provide the the standard recursive definition. The up-arrow notation is used by Donald Knuth for iterated exponentiation (Science 194, 1235-1242, 1976) and is convenient for us since we don't have superscripts. See expvalt 4677 for a description of how the sequence builder is used.

Assertion

Ref	Expression
df-exp	|- ^ = {<.<.x, y>., z>. | ((x e. CC /\ y e. NN) /\ z = (( x. seq(NN X. {x}))` y))}

Distinct variable group(s):   x,y,z

Detailed syntax breakdown of Definition df-exp

Step	Hyp	Ref	Expression
1		cexp 4675	. 2 class ^
2		vx	. . . . . . 7 set x
3	2	cv 1089	. . . . . 6 class x
4		cc 4026	. . . . . 6 class CC
5	3, 4	wcel 1092	. . . . 5 wff x e. CC
6		vy	. . . . . . 7 set y
7	6	cv 1089	. . . . . 6 class y
8		cn 4093	. . . . . 6 class NN
9	7, 8	wcel 1092	. . . . 5 wff y e. NN
10	5, 9	wa 196	. . . 4 wff (x e. CC /\ y e. NN)
11		vz	. . . . . 6 set z
12	11	cv 1089	. . . . 5 class z
13		cmulc 4032	. . . . . . 7 class x.
14	3	csn 1808	. . . . . . . 8 class {x}
15	8, 14	cxp 2408	. . . . . . 7 class (NN X. {x})
16		cseq 4660	. . . . . . 7 class seq
17	13, 15, 16	co 3001	. . . . . 6 class ( x. seq(NN X. {x}))
18	7, 17	cfv 2422	. . . . 5 class (( x. seq(NN X. {x}))` y)
19	12, 18	wceq 1091	. . . 4 wff z = (( x. seq(NN X. {x}))` y)
20	10, 19	wa 196	. . 3 wff ((x e. CC /\ y e. NN) /\ z = (( x. seq(NN X. {x}))` y))
21	20, 2, 6, 11	copab2 3002	. 2 class {<.<.x, y>., z>. | ((x e. CC /\ y e. NN) /\ z = (( x. seq(NN X. {x}))` y))}
22	1, 21	wceq 1091	1 wff ^ = {<.<.x, y>., z>. | ((x e. CC /\ y e. NN) /\ z = (( x. seq(NN X. {x}))` y))}

This definition is referenced by:  expvalt 4677

metamath.org