Metamath Proof Explorer

Theorem stoweidlem19

Description: If a set of real functions is closed under multiplication and it contains constants, then it is closed under finite exponentiation. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses stoweidlem19.1 ⊢ Ⅎ 𝑡 𝐹
stoweidlem19.2 ⊢ Ⅎ 𝑡 𝜑
stoweidlem19.3 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) → 𝑓 : 𝑇 ⟶ ℝ )
stoweidlem19.4 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
stoweidlem19.5 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝑥 ) ∈ 𝐴 )
stoweidlem19.6 ⊢ ( 𝜑 → 𝐹 ∈ 𝐴 )
stoweidlem19.7 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
Assertion stoweidlem19 ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑁 ) ) ∈ 𝐴 )

Proof

Step Hyp Ref Expression
1 stoweidlem19.1 ⊢ Ⅎ 𝑡 𝐹
2 stoweidlem19.2 ⊢ Ⅎ 𝑡 𝜑
3 stoweidlem19.3 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) → 𝑓 : 𝑇 ⟶ ℝ )
4 stoweidlem19.4 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
5 stoweidlem19.5 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝑥 ) ∈ 𝐴 )
6 stoweidlem19.6 ⊢ ( 𝜑 → 𝐹 ∈ 𝐴 )
7 stoweidlem19.7 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
8 oveq2 ⊢ ( 𝑛 = 0 → ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑛 ) = ( ( 𝐹 ‘ 𝑡 ) ↑ 0 ) )
9 8 mpteq2dv ⊢ ( 𝑛 = 0 → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑛 ) ) = ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) ↑ 0 ) ) )
10 9 eleq1d ⊢ ( 𝑛 = 0 → ( ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑛 ) ) ∈ 𝐴 ↔ ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) ↑ 0 ) ) ∈ 𝐴 ) )
11 10 imbi2d ⊢ ( 𝑛 = 0 → ( ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑛 ) ) ∈ 𝐴 ) ↔ ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) ↑ 0 ) ) ∈ 𝐴 ) ) )
12 oveq2 ⊢ ( 𝑛 = 𝑚 → ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑛 ) = ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑚 ) )
13 12 mpteq2dv ⊢ ( 𝑛 = 𝑚 → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑛 ) ) = ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑚 ) ) )
14 13 eleq1d ⊢ ( 𝑛 = 𝑚 → ( ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑛 ) ) ∈ 𝐴 ↔ ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑚 ) ) ∈ 𝐴 ) )
15 14 imbi2d ⊢ ( 𝑛 = 𝑚 → ( ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑛 ) ) ∈ 𝐴 ) ↔ ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑚 ) ) ∈ 𝐴 ) ) )
16 oveq2 ⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑛 ) = ( ( 𝐹 ‘ 𝑡 ) ↑ ( 𝑚 + 1 ) ) )
17 16 mpteq2dv ⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑛 ) ) = ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) ↑ ( 𝑚 + 1 ) ) ) )
18 17 eleq1d ⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑛 ) ) ∈ 𝐴 ↔ ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) ↑ ( 𝑚 + 1 ) ) ) ∈ 𝐴 ) )
19 18 imbi2d ⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑛 ) ) ∈ 𝐴 ) ↔ ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) ↑ ( 𝑚 + 1 ) ) ) ∈ 𝐴 ) ) )
20 oveq2 ⊢ ( 𝑛 = 𝑁 → ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑛 ) = ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑁 ) )
21 20 mpteq2dv ⊢ ( 𝑛 = 𝑁 → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑛 ) ) = ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑁 ) ) )
22 21 eleq1d ⊢ ( 𝑛 = 𝑁 → ( ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑛 ) ) ∈ 𝐴 ↔ ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑁 ) ) ∈ 𝐴 ) )
23 22 imbi2d ⊢ ( 𝑛 = 𝑁 → ( ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑛 ) ) ∈ 𝐴 ) ↔ ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑁 ) ) ∈ 𝐴 ) ) )
24 6 ancli ⊢ ( 𝜑 → ( 𝜑 ∧ 𝐹 ∈ 𝐴 ) )
25 eleq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ∈ 𝐴 ↔ 𝐹 ∈ 𝐴 ) )
26 25 anbi2d ⊢ ( 𝑓 = 𝐹 → ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) ↔ ( 𝜑 ∧ 𝐹 ∈ 𝐴 ) ) )
27 feq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 : 𝑇 ⟶ ℝ ↔ 𝐹 : 𝑇 ⟶ ℝ ) )
28 26 27 imbi12d ⊢ ( 𝑓 = 𝐹 → ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) → 𝑓 : 𝑇 ⟶ ℝ ) ↔ ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ) → 𝐹 : 𝑇 ⟶ ℝ ) ) )
29 28 3 vtoclg ⊢ ( 𝐹 ∈ 𝐴 → ( ( 𝜑 ∧ 𝐹 ∈ 𝐴 ) → 𝐹 : 𝑇 ⟶ ℝ ) )
30 6 24 29 sylc ⊢ ( 𝜑 → 𝐹 : 𝑇 ⟶ ℝ )
31 30 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝐹 ‘ 𝑡 ) ∈ ℝ )
32 recn ⊢ ( ( 𝐹 ‘ 𝑡 ) ∈ ℝ → ( 𝐹 ‘ 𝑡 ) ∈ ℂ )
33 exp0 ⊢ ( ( 𝐹 ‘ 𝑡 ) ∈ ℂ → ( ( 𝐹 ‘ 𝑡 ) ↑ 0 ) = 1 )
34 31 32 33 3syl ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝐹 ‘ 𝑡 ) ↑ 0 ) = 1 )
35 34 eqcomd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 1 = ( ( 𝐹 ‘ 𝑡 ) ↑ 0 ) )
36 2 35 mpteq2da ⊢ ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ 1 ) = ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) ↑ 0 ) ) )
37 1re ⊢ 1 ∈ ℝ
38 5 stoweidlem4 ⊢ ( ( 𝜑 ∧ 1 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 1 ) ∈ 𝐴 )
39 37 38 mpan2 ⊢ ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ 1 ) ∈ 𝐴 )
40 36 39 eqeltrrd ⊢ ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) ↑ 0 ) ) ∈ 𝐴 )
41 simpr ⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑚 ) ) ∈ 𝐴 ) ) ∧ 𝜑 ) → 𝜑 )
42 simpll ⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑚 ) ) ∈ 𝐴 ) ) ∧ 𝜑 ) → 𝑚 ∈ ℕ0 )
43 simplr ⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑚 ) ) ∈ 𝐴 ) ) ∧ 𝜑 ) → ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑚 ) ) ∈ 𝐴 ) )
44 41 43 mpd ⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑚 ) ) ∈ 𝐴 ) ) ∧ 𝜑 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑚 ) ) ∈ 𝐴 )
45 nfv ⊢ Ⅎ 𝑡 𝑚 ∈ ℕ0
46 nfmpt1 ⊢ Ⅎ 𝑡 ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑚 ) )
47 46 nfel1 ⊢ Ⅎ 𝑡 ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑚 ) ) ∈ 𝐴
48 2 45 47 nf3an ⊢ Ⅎ 𝑡 ( 𝜑 ∧ 𝑚 ∈ ℕ0 ∧ ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑚 ) ) ∈ 𝐴 )
49 simpl1 ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ∧ ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑚 ) ) ∈ 𝐴 ) ∧ 𝑡 ∈ 𝑇 ) → 𝜑 )
50 simpr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ∧ ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑚 ) ) ∈ 𝐴 ) ∧ 𝑡 ∈ 𝑇 ) → 𝑡 ∈ 𝑇 )
51 31 recnd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝐹 ‘ 𝑡 ) ∈ ℂ )
52 49 50 51 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ∧ ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑚 ) ) ∈ 𝐴 ) ∧ 𝑡 ∈ 𝑇 ) → ( 𝐹 ‘ 𝑡 ) ∈ ℂ )
53 simpl2 ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ∧ ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑚 ) ) ∈ 𝐴 ) ∧ 𝑡 ∈ 𝑇 ) → 𝑚 ∈ ℕ0 )
54 52 53 expp1d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ∧ ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑚 ) ) ∈ 𝐴 ) ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝐹 ‘ 𝑡 ) ↑ ( 𝑚 + 1 ) ) = ( ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑚 ) · ( 𝐹 ‘ 𝑡 ) ) )
55 48 54 mpteq2da ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ∧ ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑚 ) ) ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) ↑ ( 𝑚 + 1 ) ) ) = ( 𝑡 ∈ 𝑇 ↦ ( ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑚 ) · ( 𝐹 ‘ 𝑡 ) ) ) )
56 31 3adant2 ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ∧ 𝑡 ∈ 𝑇 ) → ( 𝐹 ‘ 𝑡 ) ∈ ℝ )
57 simp2 ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ∧ 𝑡 ∈ 𝑇 ) → 𝑚 ∈ ℕ0 )
58 56 57 reexpcld ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑚 ) ∈ ℝ )
59 49 53 50 58 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ∧ ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑚 ) ) ∈ 𝐴 ) ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑚 ) ∈ ℝ )
60 eqid ⊢ ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑚 ) ) = ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑚 ) )
61 60 fvmpt2 ⊢ ( ( 𝑡 ∈ 𝑇 ∧ ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑚 ) ∈ ℝ ) → ( ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑚 ) ) ‘ 𝑡 ) = ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑚 ) )
62 61 eqcomd ⊢ ( ( 𝑡 ∈ 𝑇 ∧ ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑚 ) ∈ ℝ ) → ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑚 ) = ( ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑚 ) ) ‘ 𝑡 ) )
63 50 59 62 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ∧ ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑚 ) ) ∈ 𝐴 ) ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑚 ) = ( ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑚 ) ) ‘ 𝑡 ) )
64 63 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ∧ ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑚 ) ) ∈ 𝐴 ) ∧ 𝑡 ∈ 𝑇 ) → ( ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑚 ) · ( 𝐹 ‘ 𝑡 ) ) = ( ( ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑚 ) ) ‘ 𝑡 ) · ( 𝐹 ‘ 𝑡 ) ) )
65 48 64 mpteq2da ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ∧ ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑚 ) ) ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑚 ) · ( 𝐹 ‘ 𝑡 ) ) ) = ( 𝑡 ∈ 𝑇 ↦ ( ( ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑚 ) ) ‘ 𝑡 ) · ( 𝐹 ‘ 𝑡 ) ) ) )
66 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑚 ) ) ∈ 𝐴 ) → 𝐹 ∈ 𝐴 )
67 46 nfeq2 ⊢ Ⅎ 𝑡 𝑓 = ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑚 ) )
68 1 nfeq2 ⊢ Ⅎ 𝑡 𝑔 = 𝐹
69 67 68 4 stoweidlem6 ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑚 ) ) ∈ 𝐴 ∧ 𝐹 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑚 ) ) ‘ 𝑡 ) · ( 𝐹 ‘ 𝑡 ) ) ) ∈ 𝐴 )
70 66 69 mpd3an3 ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑚 ) ) ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑚 ) ) ‘ 𝑡 ) · ( 𝐹 ‘ 𝑡 ) ) ) ∈ 𝐴 )
71 70 3adant2 ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ∧ ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑚 ) ) ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑚 ) ) ‘ 𝑡 ) · ( 𝐹 ‘ 𝑡 ) ) ) ∈ 𝐴 )
72 65 71 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ∧ ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑚 ) ) ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑚 ) · ( 𝐹 ‘ 𝑡 ) ) ) ∈ 𝐴 )
73 55 72 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ∧ ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑚 ) ) ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) ↑ ( 𝑚 + 1 ) ) ) ∈ 𝐴 )
74 41 42 44 73 syl3anc ⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑚 ) ) ∈ 𝐴 ) ) ∧ 𝜑 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) ↑ ( 𝑚 + 1 ) ) ) ∈ 𝐴 )
75 74 exp31 ⊢ ( 𝑚 ∈ ℕ0 → ( ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑚 ) ) ∈ 𝐴 ) → ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) ↑ ( 𝑚 + 1 ) ) ) ∈ 𝐴 ) ) )
76 11 15 19 23 40 75 nn0ind ⊢ ( 𝑁 ∈ ℕ0 → ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑁 ) ) ∈ 𝐴 ) )
77 7 76 mpcom ⊢ ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑁 ) ) ∈ 𝐴 )