Theorem expsval

Description: The value of surreal exponentiation. (Contributed by Scott Fenton, 24-Jul-2025)

	Ref	Expression
Assertion	expsval	Could not format assertion : No typesetting found for |- ( ( A e. No /\ B e. ZZ_s ) -> ( A ^su B ) = if ( B = 0s , 1s , if ( 0s

Proof

Step	Hyp	Ref	Expression
1		eqidd	$$⊢x=A\to 1_s=1_s$$
2		eqidd	$$⊢x=A\to {\cdot }_s={\cdot }_s$$
3		sneq	$$⊢x=A\to \left\{x\right\}=\left\{A\right\}$$
4	3	xpeq2d	$$⊢x=A\to {\mathbb{N}}_s\times \left\{x\right\}={\mathbb{N}}_s\times \left\{A\right\}$$
5	1 2 4	seqseq123d	$$⊢x=A\to {seq}_s{1}_s\left({\cdot }_s,\left({\mathbb{N}}_s\times \left\{x\right\}\right)\right)={seq}_s{1}_s\left({\cdot }_s,\left({\mathbb{N}}_s\times \left\{A\right\}\right)\right)$$
6	5	fveq1d	$$⊢x=A\to {seq}_s{1}_s\left({\cdot }_s,\left({\mathbb{N}}_s\times \left\{x\right\}\right)\right)\left(y\right)={seq}_s{1}_s\left({\cdot }_s,\left({\mathbb{N}}_s\times \left\{A\right\}\right)\right)\left(y\right)$$
7	5	fveq1d	$$⊢x=A\to {seq}_s{1}_s\left({\cdot }_s,\left({\mathbb{N}}_s\times \left\{x\right\}\right)\right)\left({+}_s\left(y\right)\right)={seq}_s{1}_s\left({\cdot }_s,\left({\mathbb{N}}_s\times \left\{A\right\}\right)\right)\left({+}_s\left(y\right)\right)$$
8	7	oveq2d	$$⊢x=A\to 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)=1_s{/}_{\mathrm{su}}{seq}_s{1}_s\left({\cdot }_s,\left({\mathbb{N}}_s\times \left\{A\right\}\right)\right)\left({+}_s\left(y\right)\right)$$
9	6 8	ifeq12d	$$⊢x=A\to 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)=if\left(0_s{<}_{s}y,{seq}_s{1}_s\left({\cdot }_s,\left({\mathbb{N}}_s\times \left\{A\right\}\right)\right)\left(y\right),1_s{/}_{\mathrm{su}}{seq}_s{1}_s\left({\cdot }_s,\left({\mathbb{N}}_s\times \left\{A\right\}\right)\right)\left({+}_s\left(y\right)\right)\right)$$
10	9	ifeq2d	$$⊢x=A\to 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)=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\{A\right\}\right)\right)\left(y\right),1_s{/}_{\mathrm{su}}{seq}_s{1}_s\left({\cdot }_s,\left({\mathbb{N}}_s\times \left\{A\right\}\right)\right)\left({+}_s\left(y\right)\right)\right)\right)$$
11		eqeq1	$$⊢y=B\to \left(y=0_s\leftrightarrow B=0_s\right)$$
12		breq2	$$⊢y=B\to \left(0_s{<}_{s}y\leftrightarrow 0_s{<}_{s}B\right)$$
13		fveq2	$$⊢y=B\to {seq}_s{1}_s\left({\cdot }_s,\left({\mathbb{N}}_s\times \left\{A\right\}\right)\right)\left(y\right)={seq}_s{1}_s\left({\cdot }_s,\left({\mathbb{N}}_s\times \left\{A\right\}\right)\right)\left(B\right)$$
14		2fveq3	$$⊢y=B\to {seq}_s{1}_s\left({\cdot }_s,\left({\mathbb{N}}_s\times \left\{A\right\}\right)\right)\left({+}_s\left(y\right)\right)={seq}_s{1}_s\left({\cdot }_s,\left({\mathbb{N}}_s\times \left\{A\right\}\right)\right)\left({+}_s\left(B\right)\right)$$
15	14	oveq2d	$$⊢y=B\to 1_s{/}_{\mathrm{su}}{seq}_s{1}_s\left({\cdot }_s,\left({\mathbb{N}}_s\times \left\{A\right\}\right)\right)\left({+}_s\left(y\right)\right)=1_s{/}_{\mathrm{su}}{seq}_s{1}_s\left({\cdot }_s,\left({\mathbb{N}}_s\times \left\{A\right\}\right)\right)\left({+}_s\left(B\right)\right)$$
16	12 13 15	ifbieq12d	$$⊢y=B\to if\left(0_s{<}_{s}y,{seq}_s{1}_s\left({\cdot }_s,\left({\mathbb{N}}_s\times \left\{A\right\}\right)\right)\left(y\right),1_s{/}_{\mathrm{su}}{seq}_s{1}_s\left({\cdot }_s,\left({\mathbb{N}}_s\times \left\{A\right\}\right)\right)\left({+}_s\left(y\right)\right)\right)=if\left(0_s{<}_{s}B,{seq}_s{1}_s\left({\cdot }_s,\left({\mathbb{N}}_s\times \left\{A\right\}\right)\right)\left(B\right),1_s{/}_{\mathrm{su}}{seq}_s{1}_s\left({\cdot }_s,\left({\mathbb{N}}_s\times \left\{A\right\}\right)\right)\left({+}_s\left(B\right)\right)\right)$$
17	11 16	ifbieq2d	$$⊢y=B\to 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\{A\right\}\right)\right)\left(y\right),1_s{/}_{\mathrm{su}}{seq}_s{1}_s\left({\cdot }_s,\left({\mathbb{N}}_s\times \left\{A\right\}\right)\right)\left({+}_s\left(y\right)\right)\right)\right)=if\left(B=0_s,1_s,if\left(0_s{<}_{s}B,{seq}_s{1}_s\left({\cdot }_s,\left({\mathbb{N}}_s\times \left\{A\right\}\right)\right)\left(B\right),1_s{/}_{\mathrm{su}}{seq}_s{1}_s\left({\cdot }_s,\left({\mathbb{N}}_s\times \left\{A\right\}\right)\right)\left({+}_s\left(B\right)\right)\right)\right)$$
18		df-exps	Could not format ^su = ( x e. No , y e. ZZ_s |-> if ( y = 0s , 1s , if ( 0s if ( y = 0s , 1s , if ( 0s
19		1no	$$⊢1_s\in \mathrm{No}$$
20	19	elexi	$$⊢1_s\in \mathrm{V}$$
21		fvex	$$⊢{seq}_s{1}_s\left({\cdot }_s,\left({\mathbb{N}}_s\times \left\{A\right\}\right)\right)\left(B\right)\in \mathrm{V}$$
22		ovex	$$⊢1_s{/}_{\mathrm{su}}{seq}_s{1}_s\left({\cdot }_s,\left({\mathbb{N}}_s\times \left\{A\right\}\right)\right)\left({+}_s\left(B\right)\right)\in \mathrm{V}$$
23	21 22	ifex	$$⊢if\left(0_s{<}_{s}B,{seq}_s{1}_s\left({\cdot }_s,\left({\mathbb{N}}_s\times \left\{A\right\}\right)\right)\left(B\right),1_s{/}_{\mathrm{su}}{seq}_s{1}_s\left({\cdot }_s,\left({\mathbb{N}}_s\times \left\{A\right\}\right)\right)\left({+}_s\left(B\right)\right)\right)\in \mathrm{V}$$
24	20 23	ifex	$$⊢if\left(B=0_s,1_s,if\left(0_s{<}_{s}B,{seq}_s{1}_s\left({\cdot }_s,\left({\mathbb{N}}_s\times \left\{A\right\}\right)\right)\left(B\right),1_s{/}_{\mathrm{su}}{seq}_s{1}_s\left({\cdot }_s,\left({\mathbb{N}}_s\times \left\{A\right\}\right)\right)\left({+}_s\left(B\right)\right)\right)\right)\in \mathrm{V}$$
25	10 17 18 24	ovmpo	Could not format ( ( A e. No /\ B e. ZZ_s ) -> ( A ^su B ) = if ( B = 0s , 1s , if ( 0s ( A ^su B ) = if ( B = 0s , 1s , if ( 0s