Definition df-exps

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cexps	⊢ ↑s
1		vx	⊢ 𝑥
2		csur	⊢ No
3		vy	⊢ 𝑦
4		czs	⊢ ℤs
5	3	cv	⊢ 𝑦
6		c0s	⊢ 0s
7	5 6	wceq	⊢ 𝑦 = 0s
8		c1s	⊢ 1s
9		cslt	⊢ <s
10	6 5 9	wbr	⊢ 0s <s 𝑦
11		cmuls	⊢ ·s
12		cnns	⊢ ℕs
13	1	cv	⊢ 𝑥
14	13	csn	⊢ { 𝑥 }
15	12 14	cxp	⊢ ( ℕs × { 𝑥 } )
16	11 15 8	cseqs	⊢ seqs 1s ( ·s , ( ℕs × { 𝑥 } ) )
17	5 16	cfv	⊢ ( seqs 1s ( ·s , ( ℕs × { 𝑥 } ) ) ‘ 𝑦 )
18		cdivs	⊢ /su
19		cnegs	⊢ -us
20	5 19	cfv	⊢ ( -us ‘ 𝑦 )
21	20 16	cfv	⊢ ( seqs 1s ( ·s , ( ℕs × { 𝑥 } ) ) ‘ ( -us ‘ 𝑦 ) )
22	8 21 18	co	⊢ ( 1s /su ( seqs 1s ( ·s , ( ℕs × { 𝑥 } ) ) ‘ ( -us ‘ 𝑦 ) ) )
23	10 17 22	cif	⊢ if ( 0s <s 𝑦 , ( seqs 1s ( ·s , ( ℕs × { 𝑥 } ) ) ‘ 𝑦 ) , ( 1s /su ( seqs 1s ( ·s , ( ℕs × { 𝑥 } ) ) ‘ ( -us ‘ 𝑦 ) ) ) )
24	7 8 23	cif	⊢ if ( 𝑦 = 0s , 1s , if ( 0s <s 𝑦 , ( seqs 1s ( ·s , ( ℕs × { 𝑥 } ) ) ‘ 𝑦 ) , ( 1s /su ( seqs 1s ( ·s , ( ℕs × { 𝑥 } ) ) ‘ ( -us ‘ 𝑦 ) ) ) ) )
25	1 3 2 4 24	cmpo	⊢ ( 𝑥 ∈ No , 𝑦 ∈ ℤs ↦ if ( 𝑦 = 0s , 1s , if ( 0s <s 𝑦 , ( seqs 1s ( ·s , ( ℕs × { 𝑥 } ) ) ‘ 𝑦 ) , ( 1s /su ( seqs 1s ( ·s , ( ℕs × { 𝑥 } ) ) ‘ ( -us ‘ 𝑦 ) ) ) ) ) )
26	0 25	wceq	⊢ ↑s = ( 𝑥 ∈ No , 𝑦 ∈ ℤs ↦ if ( 𝑦 = 0s , 1s , if ( 0s <s 𝑦 , ( seqs 1s ( ·s , ( ℕs × { 𝑥 } ) ) ‘ 𝑦 ) , ( 1s /su ( seqs 1s ( ·s , ( ℕs × { 𝑥 } ) ) ‘ ( -us ‘ 𝑦 ) ) ) ) ) )