Definition df-exps

Description: Define surreal exponentiation. Compare df-exp . (Contributed by Scott Fenton, 27-May-2025)

	Ref	Expression
Assertion	df-exps	Could not format assertion : No typesetting found for |- ^su = ( x e. No , y e. ZZ_s |-> if ( y = 0s , 1s , if ( 0s

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cexps	Could not format ^su : No typesetting found for class ^su with typecode class
1		vx	$$setvarx$$
2		csur	$$class\mathrm{No}$$
3		vy	$$setvary$$
4		czs	$$class{\mathbb{Z}}_s$$
5	3	cv	$$setvary$$
6		c0s	$$class{0}_s$$
7	5 6	wceq	$$wffy=0_s$$
8		c1s	$$class{1}_s$$
9		cslt	$$class{<}_s$$
10	6 5 9	wbr	$$wff{0}_s{<}_{s}y$$
11		cmuls	$$class{\cdot }_s$$
12		cnns	$$class{\mathbb{N}}_s$$
13	1	cv	$$setvarx$$
14	13	csn	$$class\left\{x\right\}$$
15	12 14	cxp	$$class\left({\mathbb{N}}_s\times \left\{x\right\}\right)$$
16	11 15 8	cseqs	$$class{seq}_s{1}_s\left({\cdot }_s,\left({\mathbb{N}}_s\times \left\{x\right\}\right)\right)$$
17	5 16	cfv	$$class{seq}_s{1}_s\left({\cdot }_s,\left({\mathbb{N}}_s\times \left\{x\right\}\right)\right)\left(y\right)$$
18		cdivs	$$class{/}_{\mathrm{su}}$$
19		cnegs	$$class{+}_s$$
20	5 19	cfv	$$class{+}_s\left(y\right)$$
21	20 16	cfv	$$class{seq}_s{1}_s\left({\cdot }_s,\left({\mathbb{N}}_s\times \left\{x\right\}\right)\right)\left({+}_s\left(y\right)\right)$$
22	8 21 18	co	$$class\left(1_s{/}_{\mathrm{su}}{seq}_s{1}_s\left({\cdot }_s,\left({\mathbb{N}}_s\times \left\{x\right\}\right)\right)\left({+}_s\left(y\right)\right)\right)$$
23	10 17 22	cif	$$classif\left(0_s{<}_{s}y,{seq}_s{1}_s\left({\cdot }_s,\left({\mathbb{N}}_s\times \left\{x\right\}\right)\right)\left(y\right),1_s{/}_{\mathrm{su}}{seq}_s{1}_s\left({\cdot }_s,\left({\mathbb{N}}_s\times \left\{x\right\}\right)\right)\left({+}_s\left(y\right)\right)\right)$$
24	7 8 23	cif	$$classif\left(y=0_s,1_s,if\left(0_s{<}_{s}y,{seq}_s{1}_s\left({\cdot }_s,\left({\mathbb{N}}_s\times \left\{x\right\}\right)\right)\left(y\right),1_s{/}_{\mathrm{su}}{seq}_s{1}_s\left({\cdot }_s,\left({\mathbb{N}}_s\times \left\{x\right\}\right)\right)\left({+}_s\left(y\right)\right)\right)\right)$$
25	1 3 2 4 24	cmpo	$$class\left(x\in \mathrm{No},y\in {\mathbb{Z}}_s⟼if\left(y=0_s,1_s,if\left(0_s{<}_{s}y,{seq}_s{1}_s\left({\cdot }_s,\left({\mathbb{N}}_s\times \left\{x\right\}\right)\right)\left(y\right),1_s{/}_{\mathrm{su}}{seq}_s{1}_s\left({\cdot }_s,\left({\mathbb{N}}_s\times \left\{x\right\}\right)\right)\left({+}_s\left(y\right)\right)\right)\right)\right)$$
26	0 25	wceq	Could not format ^su = ( x e. No , y e. ZZ_s |-> if ( y = 0s , 1s , if ( 0s if ( y = 0s , 1s , if ( 0s