This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴 ↑o 𝐵 ) ∈ ω )

Proof

Step Hyp Ref Expression
1 oveq2 ⊢ ( 𝑥 = 𝐵 → ( 𝐴 ↑o 𝑥 ) = ( 𝐴 ↑o 𝐵 ) )
2 1 eleq1d ⊢ ( 𝑥 = 𝐵 → ( ( 𝐴 ↑o 𝑥 ) ∈ ω ↔ ( 𝐴 ↑o 𝐵 ) ∈ ω ) )
3 2 imbi2d ⊢ ( 𝑥 = 𝐵 → ( ( 𝐴 ∈ ω → ( 𝐴 ↑o 𝑥 ) ∈ ω ) ↔ ( 𝐴 ∈ ω → ( 𝐴 ↑o 𝐵 ) ∈ ω ) ) )
4 oveq2 ⊢ ( 𝑥 = ∅ → ( 𝐴 ↑o 𝑥 ) = ( 𝐴 ↑o ∅ ) )
5 4 eleq1d ⊢ ( 𝑥 = ∅ → ( ( 𝐴 ↑o 𝑥 ) ∈ ω ↔ ( 𝐴 ↑o ∅ ) ∈ ω ) )
6 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐴 ↑o 𝑥 ) = ( 𝐴 ↑o 𝑦 ) )
7 6 eleq1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐴 ↑o 𝑥 ) ∈ ω ↔ ( 𝐴 ↑o 𝑦 ) ∈ ω ) )
8 oveq2 ⊢ ( 𝑥 = suc 𝑦 → ( 𝐴 ↑o 𝑥 ) = ( 𝐴 ↑o suc 𝑦 ) )
9 8 eleq1d ⊢ ( 𝑥 = suc 𝑦 → ( ( 𝐴 ↑o 𝑥 ) ∈ ω ↔ ( 𝐴 ↑o suc 𝑦 ) ∈ ω ) )
10 nnon ⊢ ( 𝐴 ∈ ω → 𝐴 ∈ On )
11 oe0 ⊢ ( 𝐴 ∈ On → ( 𝐴 ↑o ∅ ) = 1o )
12 10 11 syl ⊢ ( 𝐴 ∈ ω → ( 𝐴 ↑o ∅ ) = 1o )
13 df-1o ⊢ 1o = suc ∅
14 peano1 ⊢ ∅ ∈ ω
15 peano2 ⊢ ( ∅ ∈ ω → suc ∅ ∈ ω )
16 14 15 ax-mp ⊢ suc ∅ ∈ ω
17 13 16 eqeltri ⊢ 1o ∈ ω
18 12 17 eqeltrdi ⊢ ( 𝐴 ∈ ω → ( 𝐴 ↑o ∅ ) ∈ ω )
19 nnmcl ⊢ ( ( ( 𝐴 ↑o 𝑦 ) ∈ ω ∧ 𝐴 ∈ ω ) → ( ( 𝐴 ↑o 𝑦 ) ·o 𝐴 ) ∈ ω )
20 19 expcom ⊢ ( 𝐴 ∈ ω → ( ( 𝐴 ↑o 𝑦 ) ∈ ω → ( ( 𝐴 ↑o 𝑦 ) ·o 𝐴 ) ∈ ω ) )
21 20 adantr ⊢ ( ( 𝐴 ∈ ω ∧ 𝑦 ∈ ω ) → ( ( 𝐴 ↑o 𝑦 ) ∈ ω → ( ( 𝐴 ↑o 𝑦 ) ·o 𝐴 ) ∈ ω ) )
22 nnesuc ⊢ ( ( 𝐴 ∈ ω ∧ 𝑦 ∈ ω ) → ( 𝐴 ↑o suc 𝑦 ) = ( ( 𝐴 ↑o 𝑦 ) ·o 𝐴 ) )
23 22 eleq1d ⊢ ( ( 𝐴 ∈ ω ∧ 𝑦 ∈ ω ) → ( ( 𝐴 ↑o suc 𝑦 ) ∈ ω ↔ ( ( 𝐴 ↑o 𝑦 ) ·o 𝐴 ) ∈ ω ) )
24 21 23 sylibrd ⊢ ( ( 𝐴 ∈ ω ∧ 𝑦 ∈ ω ) → ( ( 𝐴 ↑o 𝑦 ) ∈ ω → ( 𝐴 ↑o suc 𝑦 ) ∈ ω ) )
25 24 expcom ⊢ ( 𝑦 ∈ ω → ( 𝐴 ∈ ω → ( ( 𝐴 ↑o 𝑦 ) ∈ ω → ( 𝐴 ↑o suc 𝑦 ) ∈ ω ) ) )
26 5 7 9 18 25 finds2 ⊢ ( 𝑥 ∈ ω → ( 𝐴 ∈ ω → ( 𝐴 ↑o 𝑥 ) ∈ ω ) )
27 3 26 vtoclga ⊢ ( 𝐵 ∈ ω → ( 𝐴 ∈ ω → ( 𝐴 ↑o 𝐵 ) ∈ ω ) )
28 27 impcom ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴 ↑o 𝐵 ) ∈ ω )