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 e. _om /\ B e. _om ) -> ( A ^o B ) e. _om )

Proof

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