Metamath Proof Explorer

Theorem nnecl

Description: Closure of exponentiation of natural numbers. Proposition 8.17 of TakeutiZaring p. 63. Theorem 2.20 of Schloeder p. 6. (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 )