Theorem expscllem

Description: Lemma for proving non-negative surreal integer exponentiation closure. (Contributed by Scott Fenton, 7-Nov-2025)

	Ref	Expression
Hypotheses	expscllem.1	$$⊢F\subseteq \mathrm{No}$$
	expscllem.2	$$⊢\left(x\in F\wedge y\in F\right)\to x{\cdot }_{s}y\in F$$
	expscllem.3	$$⊢1_s\in F$$
Assertion	expscllem	Could not format assertion : No typesetting found for |- ( ( A e. F /\ N e. NN0_s ) -> ( A ^su N ) e. F ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		expscllem.1	$$⊢F\subseteq \mathrm{No}$$
2		expscllem.2	$$⊢\left(x\in F\wedge y\in F\right)\to x{\cdot }_{s}y\in F$$
3		expscllem.3	$$⊢1_s\in F$$
4		oveq2	Could not format ( m = 0s -> ( A ^su m ) = ( A ^su 0s ) ) : No typesetting found for |- ( m = 0s -> ( A ^su m ) = ( A ^su 0s ) ) with typecode |-
5	4	eleq1d	Could not format ( m = 0s -> ( ( A ^su m ) e. F <-> ( A ^su 0s ) e. F ) ) : No typesetting found for |- ( m = 0s -> ( ( A ^su m ) e. F <-> ( A ^su 0s ) e. F ) ) with typecode |-
6	5	imbi2d	Could not format ( m = 0s -> ( ( A e. F -> ( A ^su m ) e. F ) <-> ( A e. F -> ( A ^su 0s ) e. F ) ) ) : No typesetting found for |- ( m = 0s -> ( ( A e. F -> ( A ^su m ) e. F ) <-> ( A e. F -> ( A ^su 0s ) e. F ) ) ) with typecode |-
7		oveq2	Could not format ( m = n -> ( A ^su m ) = ( A ^su n ) ) : No typesetting found for |- ( m = n -> ( A ^su m ) = ( A ^su n ) ) with typecode |-
8	7	eleq1d	Could not format ( m = n -> ( ( A ^su m ) e. F <-> ( A ^su n ) e. F ) ) : No typesetting found for |- ( m = n -> ( ( A ^su m ) e. F <-> ( A ^su n ) e. F ) ) with typecode |-
9	8	imbi2d	Could not format ( m = n -> ( ( A e. F -> ( A ^su m ) e. F ) <-> ( A e. F -> ( A ^su n ) e. F ) ) ) : No typesetting found for |- ( m = n -> ( ( A e. F -> ( A ^su m ) e. F ) <-> ( A e. F -> ( A ^su n ) e. F ) ) ) with typecode |-
10		oveq2	Could not format ( m = ( n +s 1s ) -> ( A ^su m ) = ( A ^su ( n +s 1s ) ) ) : No typesetting found for |- ( m = ( n +s 1s ) -> ( A ^su m ) = ( A ^su ( n +s 1s ) ) ) with typecode |-
11	10	eleq1d	Could not format ( m = ( n +s 1s ) -> ( ( A ^su m ) e. F <-> ( A ^su ( n +s 1s ) ) e. F ) ) : No typesetting found for |- ( m = ( n +s 1s ) -> ( ( A ^su m ) e. F <-> ( A ^su ( n +s 1s ) ) e. F ) ) with typecode |-
12	11	imbi2d	Could not format ( m = ( n +s 1s ) -> ( ( A e. F -> ( A ^su m ) e. F ) <-> ( A e. F -> ( A ^su ( n +s 1s ) ) e. F ) ) ) : No typesetting found for |- ( m = ( n +s 1s ) -> ( ( A e. F -> ( A ^su m ) e. F ) <-> ( A e. F -> ( A ^su ( n +s 1s ) ) e. F ) ) ) with typecode |-
13		oveq2	Could not format ( m = N -> ( A ^su m ) = ( A ^su N ) ) : No typesetting found for |- ( m = N -> ( A ^su m ) = ( A ^su N ) ) with typecode |-
14	13	eleq1d	Could not format ( m = N -> ( ( A ^su m ) e. F <-> ( A ^su N ) e. F ) ) : No typesetting found for |- ( m = N -> ( ( A ^su m ) e. F <-> ( A ^su N ) e. F ) ) with typecode |-
15	14	imbi2d	Could not format ( m = N -> ( ( A e. F -> ( A ^su m ) e. F ) <-> ( A e. F -> ( A ^su N ) e. F ) ) ) : No typesetting found for |- ( m = N -> ( ( A e. F -> ( A ^su m ) e. F ) <-> ( A e. F -> ( A ^su N ) e. F ) ) ) with typecode |-
16	1	sseli	$$⊢A\in F\to A\in \mathrm{No}$$
17		exps0	Could not format ( A e. No -> ( A ^su 0s ) = 1s ) : No typesetting found for |- ( A e. No -> ( A ^su 0s ) = 1s ) with typecode |-
18	16 17	syl	Could not format ( A e. F -> ( A ^su 0s ) = 1s ) : No typesetting found for |- ( A e. F -> ( A ^su 0s ) = 1s ) with typecode |-
19	18 3	eqeltrdi	Could not format ( A e. F -> ( A ^su 0s ) e. F ) : No typesetting found for |- ( A e. F -> ( A ^su 0s ) e. F ) with typecode |-
20	16	3ad2ant2	Could not format ( ( n e. NN0_s /\ A e. F /\ ( A ^su n ) e. F ) -> A e. No ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. F /\ ( A ^su n ) e. F ) -> A e. No ) with typecode |-
21		simp1	Could not format ( ( n e. NN0_s /\ A e. F /\ ( A ^su n ) e. F ) -> n e. NN0_s ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. F /\ ( A ^su n ) e. F ) -> n e. NN0_s ) with typecode |-
22		expsp1	Could not format ( ( A e. No /\ n e. NN0_s ) -> ( A ^su ( n +s 1s ) ) = ( ( A ^su n ) x.s A ) ) : No typesetting found for |- ( ( A e. No /\ n e. NN0_s ) -> ( A ^su ( n +s 1s ) ) = ( ( A ^su n ) x.s A ) ) with typecode |-
23	20 21 22	syl2anc	Could not format ( ( n e. NN0_s /\ A e. F /\ ( A ^su n ) e. F ) -> ( A ^su ( n +s 1s ) ) = ( ( A ^su n ) x.s A ) ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. F /\ ( A ^su n ) e. F ) -> ( A ^su ( n +s 1s ) ) = ( ( A ^su n ) x.s A ) ) with typecode |-
24	2	caovcl	Could not format ( ( ( A ^su n ) e. F /\ A e. F ) -> ( ( A ^su n ) x.s A ) e. F ) : No typesetting found for |- ( ( ( A ^su n ) e. F /\ A e. F ) -> ( ( A ^su n ) x.s A ) e. F ) with typecode |-
25	24	ancoms	Could not format ( ( A e. F /\ ( A ^su n ) e. F ) -> ( ( A ^su n ) x.s A ) e. F ) : No typesetting found for |- ( ( A e. F /\ ( A ^su n ) e. F ) -> ( ( A ^su n ) x.s A ) e. F ) with typecode |-
26	25	3adant1	Could not format ( ( n e. NN0_s /\ A e. F /\ ( A ^su n ) e. F ) -> ( ( A ^su n ) x.s A ) e. F ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. F /\ ( A ^su n ) e. F ) -> ( ( A ^su n ) x.s A ) e. F ) with typecode |-
27	23 26	eqeltrd	Could not format ( ( n e. NN0_s /\ A e. F /\ ( A ^su n ) e. F ) -> ( A ^su ( n +s 1s ) ) e. F ) : No typesetting found for |- ( ( n e. NN0_s /\ A e. F /\ ( A ^su n ) e. F ) -> ( A ^su ( n +s 1s ) ) e. F ) with typecode |-
28	27	3exp	Could not format ( n e. NN0_s -> ( A e. F -> ( ( A ^su n ) e. F -> ( A ^su ( n +s 1s ) ) e. F ) ) ) : No typesetting found for |- ( n e. NN0_s -> ( A e. F -> ( ( A ^su n ) e. F -> ( A ^su ( n +s 1s ) ) e. F ) ) ) with typecode |-
29	28	a2d	Could not format ( n e. NN0_s -> ( ( A e. F -> ( A ^su n ) e. F ) -> ( A e. F -> ( A ^su ( n +s 1s ) ) e. F ) ) ) : No typesetting found for |- ( n e. NN0_s -> ( ( A e. F -> ( A ^su n ) e. F ) -> ( A e. F -> ( A ^su ( n +s 1s ) ) e. F ) ) ) with typecode |-
30	6 9 12 15 19 29	n0sind	Could not format ( N e. NN0_s -> ( A e. F -> ( A ^su N ) e. F ) ) : No typesetting found for |- ( N e. NN0_s -> ( A e. F -> ( A ^su N ) e. F ) ) with typecode |-
31	30	impcom	Could not format ( ( A e. F /\ N e. NN0_s ) -> ( A ^su N ) e. F ) : No typesetting found for |- ( ( A e. F /\ N e. NN0_s ) -> ( A ^su N ) e. F ) with typecode |-