Definition df-exps 28799

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

Assertion

Ref	Expression
df-exps	⊢ ↑s = (𝑥 ∈ No, 𝑦 ∈ ℤs ↦ if(𝑦 = 0s , 1s , if( 0s <s 𝑦, (seqs 1s ( ·s , (ℕs × {𝑥}))‘𝑦), ( 1s /su (seqs 1s ( ·s , (ℕs × {𝑥}))‘( -s‘𝑦))))))

Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Definition df-exps

Step	Hyp	Ref	Expression
1		cexps 28798	. 2 class ↑s
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		csur 27997	. . 3 class No
5		czs 28764	. . 3 class ℤs
6	3	cv 1568	. . . . 5 class 𝑦
7		c0s 28191	. . . . 5 class 0s
8	6, 7	wceq 1569	. . . 4 wff 𝑦 = 0s
9		c1s 28192	. . . 4 class 1s
10		clts 27998	. . . . . 6 class <s
11	7, 6, 10	wbr 5102	. . . . 5 wff 0s <s 𝑦
12		cmuls 28492	. . . . . . 7 class ·s
13		cnns 28699	. . . . . . . 8 class ℕs
14	2	cv 1568	. . . . . . . . 9 class 𝑥
15	14	csn 4583	. . . . . . . 8 class {𝑥}
16	13, 15	cxp 5648	. . . . . . 7 class (ℕs × {𝑥})
17	12, 16, 9	cseqs 28669	. . . . . 6 class seqs 1s ( ·s , (ℕs × {𝑥}))
18	6, 17	cfv 6538	. . . . 5 class (seqs 1s ( ·s , (ℕs × {𝑥}))‘𝑦)
19		cnegs 28405	. . . . . . . 8 class -s
20	6, 19	cfv 6538	. . . . . . 7 class ( -s‘𝑦)
21	20, 17	cfv 6538	. . . . . 6 class (seqs 1s ( ·s , (ℕs × {𝑥}))‘( -s‘𝑦))
22		cdivs 28573	. . . . . 6 class /su
23	9, 21, 22	co 7420	. . . . 5 class ( 1s /su (seqs 1s ( ·s , (ℕs × {𝑥}))‘( -s‘𝑦)))
24	11, 18, 23	cif 4481	. . . 4 class if( 0s <s 𝑦, (seqs 1s ( ·s , (ℕs × {𝑥}))‘𝑦), ( 1s /su (seqs 1s ( ·s , (ℕs × {𝑥}))‘( -s‘𝑦))))
25	8, 9, 24	cif 4481	. . 3 class if(𝑦 = 0s , 1s , if( 0s <s 𝑦, (seqs 1s ( ·s , (ℕs × {𝑥}))‘𝑦), ( 1s /su (seqs 1s ( ·s , (ℕs × {𝑥}))‘( -s‘𝑦)))))
26	2, 3, 4, 5, 25	cmpo 7422	. 2 class (𝑥 ∈ No, 𝑦 ∈ ℤs ↦ if(𝑦 = 0s , 1s , if( 0s <s 𝑦, (seqs 1s ( ·s , (ℕs × {𝑥}))‘𝑦), ( 1s /su (seqs 1s ( ·s , (ℕs × {𝑥}))‘( -s‘𝑦))))))
27	1, 26	wceq 1569	1 wff ↑s = (𝑥 ∈ No, 𝑦 ∈ ℤs ↦ if(𝑦 = 0s , 1s , if( 0s <s 𝑦, (seqs 1s ( ·s , (ℕs × {𝑥}))‘𝑦), ( 1s /su (seqs 1s ( ·s , (ℕs × {𝑥}))‘( -s‘𝑦))))))

This definition is used by:  expsval  28811