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	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝐹 ‘ 𝑡 ) ∈ ℝ )
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	⊢ ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑁 ) ) ∈ 𝐴 )