Metamath Proof Explorer

Theorem expscllem

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

Ref Expression
Hypotheses expscllem.1 ⊢ 𝐹 ⊆ No
expscllem.2 ⊢ ( ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) → ( 𝑥 ·s 𝑦 ) ∈ 𝐹 )
expscllem.3 ⊢ 1s ∈ 𝐹
Assertion expscllem ( ( 𝐴 ∈ 𝐹 ∧ 𝑁 ∈ ℕ0s ) → ( 𝐴 ↑s 𝑁 ) ∈ 𝐹 )

Proof

Step Hyp Ref Expression
1 expscllem.1 ⊢ 𝐹 ⊆ No
2 expscllem.2 ⊢ ( ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) → ( 𝑥 ·s 𝑦 ) ∈ 𝐹 )
3 expscllem.3 ⊢ 1s ∈ 𝐹
4 oveq2 ⊢ ( 𝑚 = 0s → ( 𝐴 ↑s 𝑚 ) = ( 𝐴 ↑s 0s ) )
5 4 eleq1d ⊢ ( 𝑚 = 0s → ( ( 𝐴 ↑s 𝑚 ) ∈ 𝐹 ↔ ( 𝐴 ↑s 0s ) ∈ 𝐹 ) )
6 5 imbi2d ⊢ ( 𝑚 = 0s → ( ( 𝐴 ∈ 𝐹 → ( 𝐴 ↑s 𝑚 ) ∈ 𝐹 ) ↔ ( 𝐴 ∈ 𝐹 → ( 𝐴 ↑s 0s ) ∈ 𝐹 ) ) )
7 oveq2 ⊢ ( 𝑚 = 𝑛 → ( 𝐴 ↑s 𝑚 ) = ( 𝐴 ↑s 𝑛 ) )
8 7 eleq1d ⊢ ( 𝑚 = 𝑛 → ( ( 𝐴 ↑s 𝑚 ) ∈ 𝐹 ↔ ( 𝐴 ↑s 𝑛 ) ∈ 𝐹 ) )
9 8 imbi2d ⊢ ( 𝑚 = 𝑛 → ( ( 𝐴 ∈ 𝐹 → ( 𝐴 ↑s 𝑚 ) ∈ 𝐹 ) ↔ ( 𝐴 ∈ 𝐹 → ( 𝐴 ↑s 𝑛 ) ∈ 𝐹 ) ) )
10 oveq2 ⊢ ( 𝑚 = ( 𝑛 +s 1s ) → ( 𝐴 ↑s 𝑚 ) = ( 𝐴 ↑s ( 𝑛 +s 1s ) ) )
11 10 eleq1d ⊢ ( 𝑚 = ( 𝑛 +s 1s ) → ( ( 𝐴 ↑s 𝑚 ) ∈ 𝐹 ↔ ( 𝐴 ↑s ( 𝑛 +s 1s ) ) ∈ 𝐹 ) )
12 11 imbi2d ⊢ ( 𝑚 = ( 𝑛 +s 1s ) → ( ( 𝐴 ∈ 𝐹 → ( 𝐴 ↑s 𝑚 ) ∈ 𝐹 ) ↔ ( 𝐴 ∈ 𝐹 → ( 𝐴 ↑s ( 𝑛 +s 1s ) ) ∈ 𝐹 ) ) )
13 oveq2 ⊢ ( 𝑚 = 𝑁 → ( 𝐴 ↑s 𝑚 ) = ( 𝐴 ↑s 𝑁 ) )
14 13 eleq1d ⊢ ( 𝑚 = 𝑁 → ( ( 𝐴 ↑s 𝑚 ) ∈ 𝐹 ↔ ( 𝐴 ↑s 𝑁 ) ∈ 𝐹 ) )
15 14 imbi2d ⊢ ( 𝑚 = 𝑁 → ( ( 𝐴 ∈ 𝐹 → ( 𝐴 ↑s 𝑚 ) ∈ 𝐹 ) ↔ ( 𝐴 ∈ 𝐹 → ( 𝐴 ↑s 𝑁 ) ∈ 𝐹 ) ) )
16 1 sseli ⊢ ( 𝐴 ∈ 𝐹 → 𝐴 ∈ No )
17 exps0 ⊢ ( 𝐴 ∈ No → ( 𝐴 ↑s 0s ) = 1s )
18 16 17 syl ⊢ ( 𝐴 ∈ 𝐹 → ( 𝐴 ↑s 0s ) = 1s )
19 18 3 eqeltrdi ⊢ ( 𝐴 ∈ 𝐹 → ( 𝐴 ↑s 0s ) ∈ 𝐹 )
20 16 3ad2ant2 ⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ 𝐹 ∧ ( 𝐴 ↑s 𝑛 ) ∈ 𝐹 ) → 𝐴 ∈ No )
21 simp1 ⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ 𝐹 ∧ ( 𝐴 ↑s 𝑛 ) ∈ 𝐹 ) → 𝑛 ∈ ℕ0s )
22 expsp1 ⊢ ( ( 𝐴 ∈ No ∧ 𝑛 ∈ ℕ0s ) → ( 𝐴 ↑s ( 𝑛 +s 1s ) ) = ( ( 𝐴 ↑s 𝑛 ) ·s 𝐴 ) )
23 20 21 22 syl2anc ⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ 𝐹 ∧ ( 𝐴 ↑s 𝑛 ) ∈ 𝐹 ) → ( 𝐴 ↑s ( 𝑛 +s 1s ) ) = ( ( 𝐴 ↑s 𝑛 ) ·s 𝐴 ) )
24 2 caovcl ⊢ ( ( ( 𝐴 ↑s 𝑛 ) ∈ 𝐹 ∧ 𝐴 ∈ 𝐹 ) → ( ( 𝐴 ↑s 𝑛 ) ·s 𝐴 ) ∈ 𝐹 )
25 24 ancoms ⊢ ( ( 𝐴 ∈ 𝐹 ∧ ( 𝐴 ↑s 𝑛 ) ∈ 𝐹 ) → ( ( 𝐴 ↑s 𝑛 ) ·s 𝐴 ) ∈ 𝐹 )
26 25 3adant1 ⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ 𝐹 ∧ ( 𝐴 ↑s 𝑛 ) ∈ 𝐹 ) → ( ( 𝐴 ↑s 𝑛 ) ·s 𝐴 ) ∈ 𝐹 )
27 23 26 eqeltrd ⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝐴 ∈ 𝐹 ∧ ( 𝐴 ↑s 𝑛 ) ∈ 𝐹 ) → ( 𝐴 ↑s ( 𝑛 +s 1s ) ) ∈ 𝐹 )
28 27 3exp ⊢ ( 𝑛 ∈ ℕ0s → ( 𝐴 ∈ 𝐹 → ( ( 𝐴 ↑s 𝑛 ) ∈ 𝐹 → ( 𝐴 ↑s ( 𝑛 +s 1s ) ) ∈ 𝐹 ) ) )
29 28 a2d ⊢ ( 𝑛 ∈ ℕ0s → ( ( 𝐴 ∈ 𝐹 → ( 𝐴 ↑s 𝑛 ) ∈ 𝐹 ) → ( 𝐴 ∈ 𝐹 → ( 𝐴 ↑s ( 𝑛 +s 1s ) ) ∈ 𝐹 ) ) )
30 6 9 12 15 19 29 n0sind ⊢ ( 𝑁 ∈ ℕ0s → ( 𝐴 ∈ 𝐹 → ( 𝐴 ↑s 𝑁 ) ∈ 𝐹 ) )
31 30 impcom ⊢ ( ( 𝐴 ∈ 𝐹 ∧ 𝑁 ∈ ℕ0s ) → ( 𝐴 ↑s 𝑁 ) ∈ 𝐹 )