Metamath Proof Explorer


Theorem nnecl

Description: Closure of exponentiation of natural numbers. Proposition 8.17 of TakeutiZaring p. 63. (Contributed by NM, 24-Mar-2007) (Proof shortened by Andrew Salmon, 22-Oct-2011)

Ref Expression
Assertion nnecl A ω B ω A 𝑜 B ω

Proof

Step Hyp Ref Expression
1 oveq2 x = B A 𝑜 x = A 𝑜 B
2 1 eleq1d x = B A 𝑜 x ω A 𝑜 B ω
3 2 imbi2d x = B A ω A 𝑜 x ω A ω A 𝑜 B ω
4 oveq2 x = A 𝑜 x = A 𝑜
5 4 eleq1d x = A 𝑜 x ω A 𝑜 ω
6 oveq2 x = y A 𝑜 x = A 𝑜 y
7 6 eleq1d x = y A 𝑜 x ω A 𝑜 y ω
8 oveq2 x = suc y A 𝑜 x = A 𝑜 suc y
9 8 eleq1d x = suc y A 𝑜 x ω A 𝑜 suc y ω
10 nnon A ω A On
11 oe0 A On A 𝑜 = 1 𝑜
12 10 11 syl A ω A 𝑜 = 1 𝑜
13 df-1o 1 𝑜 = suc
14 peano1 ω
15 peano2 ω suc ω
16 14 15 ax-mp suc ω
17 13 16 eqeltri 1 𝑜 ω
18 12 17 eqeltrdi A ω A 𝑜 ω
19 nnmcl A 𝑜 y ω A ω A 𝑜 y 𝑜 A ω
20 19 expcom A ω A 𝑜 y ω A 𝑜 y 𝑜 A ω
21 20 adantr A ω y ω A 𝑜 y ω A 𝑜 y 𝑜 A ω
22 nnesuc A ω y ω A 𝑜 suc y = A 𝑜 y 𝑜 A
23 22 eleq1d A ω y ω A 𝑜 suc y ω A 𝑜 y 𝑜 A ω
24 21 23 sylibrd A ω y ω A 𝑜 y ω A 𝑜 suc y ω
25 24 expcom y ω A ω A 𝑜 y ω A 𝑜 suc y ω
26 5 7 9 18 25 finds2 x ω A ω A 𝑜 x ω
27 3 26 vtoclga B ω A ω A 𝑜 B ω
28 27 impcom A ω B ω A 𝑜 B ω