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

Metamath Proof Explorer

Theorem seqf1o

Description: Rearrange a sum via an arbitrary bijection on ( M ... N ) . (Contributed by Mario Carneiro, 27-Feb-2014) (Revised by Mario Carneiro, 24-Apr-2016)

Ref Expression
Hypotheses seqf1o.1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
seqf1o.2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) )
seqf1o.3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) )
seqf1o.4 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
seqf1o.5 ⊢ ( 𝜑 → 𝐶 ⊆ 𝑆 )
seqf1o.6 ⊢ ( 𝜑 → 𝐹 : ( 𝑀 ... 𝑁 ) –1-1-onto→ ( 𝑀 ... 𝑁 ) )
seqf1o.7 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐺 ‘ 𝑥 ) ∈ 𝐶 )
seqf1o.8 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐻 ‘ 𝑘 ) = ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) )
Assertion seqf1o ( 𝜑 → ( seq 𝑀 ( + , 𝐻 ) ‘ 𝑁 ) = ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 seqf1o.1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
2 seqf1o.2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) )
3 seqf1o.3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) )
4 seqf1o.4 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
5 seqf1o.5 ⊢ ( 𝜑 → 𝐶 ⊆ 𝑆 )
6 seqf1o.6 ⊢ ( 𝜑 → 𝐹 : ( 𝑀 ... 𝑁 ) –1-1-onto→ ( 𝑀 ... 𝑁 ) )
7 seqf1o.7 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐺 ‘ 𝑥 ) ∈ 𝐶 )
8 seqf1o.8 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐻 ‘ 𝑘 ) = ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) )
9 7 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝐺 ‘ 𝑥 ) ) : ( 𝑀 ... 𝑁 ) ⟶ 𝐶 )
10 oveq2 ⊢ ( 𝑥 = 𝑀 → ( 𝑀 ... 𝑥 ) = ( 𝑀 ... 𝑀 ) )
11 f1oeq23 ⊢ ( ( ( 𝑀 ... 𝑥 ) = ( 𝑀 ... 𝑀 ) ∧ ( 𝑀 ... 𝑥 ) = ( 𝑀 ... 𝑀 ) ) → ( 𝑓 : ( 𝑀 ... 𝑥 ) –1-1-onto→ ( 𝑀 ... 𝑥 ) ↔ 𝑓 : ( 𝑀 ... 𝑀 ) –1-1-onto→ ( 𝑀 ... 𝑀 ) ) )
12 10 10 11 syl2anc ⊢ ( 𝑥 = 𝑀 → ( 𝑓 : ( 𝑀 ... 𝑥 ) –1-1-onto→ ( 𝑀 ... 𝑥 ) ↔ 𝑓 : ( 𝑀 ... 𝑀 ) –1-1-onto→ ( 𝑀 ... 𝑀 ) ) )
13 10 feq2d ⊢ ( 𝑥 = 𝑀 → ( 𝑔 : ( 𝑀 ... 𝑥 ) ⟶ 𝐶 ↔ 𝑔 : ( 𝑀 ... 𝑀 ) ⟶ 𝐶 ) )
14 12 13 anbi12d ⊢ ( 𝑥 = 𝑀 → ( ( 𝑓 : ( 𝑀 ... 𝑥 ) –1-1-onto→ ( 𝑀 ... 𝑥 ) ∧ 𝑔 : ( 𝑀 ... 𝑥 ) ⟶ 𝐶 ) ↔ ( 𝑓 : ( 𝑀 ... 𝑀 ) –1-1-onto→ ( 𝑀 ... 𝑀 ) ∧ 𝑔 : ( 𝑀 ... 𝑀 ) ⟶ 𝐶 ) ) )
15 fveq2 ⊢ ( 𝑥 = 𝑀 → ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ 𝑥 ) = ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ 𝑀 ) )
16 fveq2 ⊢ ( 𝑥 = 𝑀 → ( seq 𝑀 ( + , 𝑔 ) ‘ 𝑥 ) = ( seq 𝑀 ( + , 𝑔 ) ‘ 𝑀 ) )
17 15 16 eqeq12d ⊢ ( 𝑥 = 𝑀 → ( ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ 𝑥 ) = ( seq 𝑀 ( + , 𝑔 ) ‘ 𝑥 ) ↔ ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ 𝑀 ) = ( seq 𝑀 ( + , 𝑔 ) ‘ 𝑀 ) ) )
18 14 17 imbi12d ⊢ ( 𝑥 = 𝑀 → ( ( ( 𝑓 : ( 𝑀 ... 𝑥 ) –1-1-onto→ ( 𝑀 ... 𝑥 ) ∧ 𝑔 : ( 𝑀 ... 𝑥 ) ⟶ 𝐶 ) → ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ 𝑥 ) = ( seq 𝑀 ( + , 𝑔 ) ‘ 𝑥 ) ) ↔ ( ( 𝑓 : ( 𝑀 ... 𝑀 ) –1-1-onto→ ( 𝑀 ... 𝑀 ) ∧ 𝑔 : ( 𝑀 ... 𝑀 ) ⟶ 𝐶 ) → ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ 𝑀 ) = ( seq 𝑀 ( + , 𝑔 ) ‘ 𝑀 ) ) ) )
19 18 2albidv ⊢ ( 𝑥 = 𝑀 → ( ∀ 𝑔 ∀ 𝑓 ( ( 𝑓 : ( 𝑀 ... 𝑥 ) –1-1-onto→ ( 𝑀 ... 𝑥 ) ∧ 𝑔 : ( 𝑀 ... 𝑥 ) ⟶ 𝐶 ) → ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ 𝑥 ) = ( seq 𝑀 ( + , 𝑔 ) ‘ 𝑥 ) ) ↔ ∀ 𝑔 ∀ 𝑓 ( ( 𝑓 : ( 𝑀 ... 𝑀 ) –1-1-onto→ ( 𝑀 ... 𝑀 ) ∧ 𝑔 : ( 𝑀 ... 𝑀 ) ⟶ 𝐶 ) → ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ 𝑀 ) = ( seq 𝑀 ( + , 𝑔 ) ‘ 𝑀 ) ) ) )
20 19 imbi2d ⊢ ( 𝑥 = 𝑀 → ( ( 𝜑 → ∀ 𝑔 ∀ 𝑓 ( ( 𝑓 : ( 𝑀 ... 𝑥 ) –1-1-onto→ ( 𝑀 ... 𝑥 ) ∧ 𝑔 : ( 𝑀 ... 𝑥 ) ⟶ 𝐶 ) → ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ 𝑥 ) = ( seq 𝑀 ( + , 𝑔 ) ‘ 𝑥 ) ) ) ↔ ( 𝜑 → ∀ 𝑔 ∀ 𝑓 ( ( 𝑓 : ( 𝑀 ... 𝑀 ) –1-1-onto→ ( 𝑀 ... 𝑀 ) ∧ 𝑔 : ( 𝑀 ... 𝑀 ) ⟶ 𝐶 ) → ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ 𝑀 ) = ( seq 𝑀 ( + , 𝑔 ) ‘ 𝑀 ) ) ) ) )
21 oveq2 ⊢ ( 𝑥 = 𝑘 → ( 𝑀 ... 𝑥 ) = ( 𝑀 ... 𝑘 ) )
22 f1oeq23 ⊢ ( ( ( 𝑀 ... 𝑥 ) = ( 𝑀 ... 𝑘 ) ∧ ( 𝑀 ... 𝑥 ) = ( 𝑀 ... 𝑘 ) ) → ( 𝑓 : ( 𝑀 ... 𝑥 ) –1-1-onto→ ( 𝑀 ... 𝑥 ) ↔ 𝑓 : ( 𝑀 ... 𝑘 ) –1-1-onto→ ( 𝑀 ... 𝑘 ) ) )
23 21 21 22 syl2anc ⊢ ( 𝑥 = 𝑘 → ( 𝑓 : ( 𝑀 ... 𝑥 ) –1-1-onto→ ( 𝑀 ... 𝑥 ) ↔ 𝑓 : ( 𝑀 ... 𝑘 ) –1-1-onto→ ( 𝑀 ... 𝑘 ) ) )
24 21 feq2d ⊢ ( 𝑥 = 𝑘 → ( 𝑔 : ( 𝑀 ... 𝑥 ) ⟶ 𝐶 ↔ 𝑔 : ( 𝑀 ... 𝑘 ) ⟶ 𝐶 ) )
25 23 24 anbi12d ⊢ ( 𝑥 = 𝑘 → ( ( 𝑓 : ( 𝑀 ... 𝑥 ) –1-1-onto→ ( 𝑀 ... 𝑥 ) ∧ 𝑔 : ( 𝑀 ... 𝑥 ) ⟶ 𝐶 ) ↔ ( 𝑓 : ( 𝑀 ... 𝑘 ) –1-1-onto→ ( 𝑀 ... 𝑘 ) ∧ 𝑔 : ( 𝑀 ... 𝑘 ) ⟶ 𝐶 ) ) )
26 fveq2 ⊢ ( 𝑥 = 𝑘 → ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ 𝑥 ) = ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ 𝑘 ) )
27 fveq2 ⊢ ( 𝑥 = 𝑘 → ( seq 𝑀 ( + , 𝑔 ) ‘ 𝑥 ) = ( seq 𝑀 ( + , 𝑔 ) ‘ 𝑘 ) )
28 26 27 eqeq12d ⊢ ( 𝑥 = 𝑘 → ( ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ 𝑥 ) = ( seq 𝑀 ( + , 𝑔 ) ‘ 𝑥 ) ↔ ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ 𝑘 ) = ( seq 𝑀 ( + , 𝑔 ) ‘ 𝑘 ) ) )
29 25 28 imbi12d ⊢ ( 𝑥 = 𝑘 → ( ( ( 𝑓 : ( 𝑀 ... 𝑥 ) –1-1-onto→ ( 𝑀 ... 𝑥 ) ∧ 𝑔 : ( 𝑀 ... 𝑥 ) ⟶ 𝐶 ) → ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ 𝑥 ) = ( seq 𝑀 ( + , 𝑔 ) ‘ 𝑥 ) ) ↔ ( ( 𝑓 : ( 𝑀 ... 𝑘 ) –1-1-onto→ ( 𝑀 ... 𝑘 ) ∧ 𝑔 : ( 𝑀 ... 𝑘 ) ⟶ 𝐶 ) → ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ 𝑘 ) = ( seq 𝑀 ( + , 𝑔 ) ‘ 𝑘 ) ) ) )
30 29 2albidv ⊢ ( 𝑥 = 𝑘 → ( ∀ 𝑔 ∀ 𝑓 ( ( 𝑓 : ( 𝑀 ... 𝑥 ) –1-1-onto→ ( 𝑀 ... 𝑥 ) ∧ 𝑔 : ( 𝑀 ... 𝑥 ) ⟶ 𝐶 ) → ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ 𝑥 ) = ( seq 𝑀 ( + , 𝑔 ) ‘ 𝑥 ) ) ↔ ∀ 𝑔 ∀ 𝑓 ( ( 𝑓 : ( 𝑀 ... 𝑘 ) –1-1-onto→ ( 𝑀 ... 𝑘 ) ∧ 𝑔 : ( 𝑀 ... 𝑘 ) ⟶ 𝐶 ) → ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ 𝑘 ) = ( seq 𝑀 ( + , 𝑔 ) ‘ 𝑘 ) ) ) )
31 30 imbi2d ⊢ ( 𝑥 = 𝑘 → ( ( 𝜑 → ∀ 𝑔 ∀ 𝑓 ( ( 𝑓 : ( 𝑀 ... 𝑥 ) –1-1-onto→ ( 𝑀 ... 𝑥 ) ∧ 𝑔 : ( 𝑀 ... 𝑥 ) ⟶ 𝐶 ) → ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ 𝑥 ) = ( seq 𝑀 ( + , 𝑔 ) ‘ 𝑥 ) ) ) ↔ ( 𝜑 → ∀ 𝑔 ∀ 𝑓 ( ( 𝑓 : ( 𝑀 ... 𝑘 ) –1-1-onto→ ( 𝑀 ... 𝑘 ) ∧ 𝑔 : ( 𝑀 ... 𝑘 ) ⟶ 𝐶 ) → ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ 𝑘 ) = ( seq 𝑀 ( + , 𝑔 ) ‘ 𝑘 ) ) ) ) )
32 oveq2 ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( 𝑀 ... 𝑥 ) = ( 𝑀 ... ( 𝑘 + 1 ) ) )
33 f1oeq23 ⊢ ( ( ( 𝑀 ... 𝑥 ) = ( 𝑀 ... ( 𝑘 + 1 ) ) ∧ ( 𝑀 ... 𝑥 ) = ( 𝑀 ... ( 𝑘 + 1 ) ) ) → ( 𝑓 : ( 𝑀 ... 𝑥 ) –1-1-onto→ ( 𝑀 ... 𝑥 ) ↔ 𝑓 : ( 𝑀 ... ( 𝑘 + 1 ) ) –1-1-onto→ ( 𝑀 ... ( 𝑘 + 1 ) ) ) )
34 32 32 33 syl2anc ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( 𝑓 : ( 𝑀 ... 𝑥 ) –1-1-onto→ ( 𝑀 ... 𝑥 ) ↔ 𝑓 : ( 𝑀 ... ( 𝑘 + 1 ) ) –1-1-onto→ ( 𝑀 ... ( 𝑘 + 1 ) ) ) )
35 32 feq2d ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( 𝑔 : ( 𝑀 ... 𝑥 ) ⟶ 𝐶 ↔ 𝑔 : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐶 ) )
36 34 35 anbi12d ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( ( 𝑓 : ( 𝑀 ... 𝑥 ) –1-1-onto→ ( 𝑀 ... 𝑥 ) ∧ 𝑔 : ( 𝑀 ... 𝑥 ) ⟶ 𝐶 ) ↔ ( 𝑓 : ( 𝑀 ... ( 𝑘 + 1 ) ) –1-1-onto→ ( 𝑀 ... ( 𝑘 + 1 ) ) ∧ 𝑔 : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐶 ) ) )
37 fveq2 ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ 𝑥 ) = ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ ( 𝑘 + 1 ) ) )
38 fveq2 ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( seq 𝑀 ( + , 𝑔 ) ‘ 𝑥 ) = ( seq 𝑀 ( + , 𝑔 ) ‘ ( 𝑘 + 1 ) ) )
39 37 38 eqeq12d ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ 𝑥 ) = ( seq 𝑀 ( + , 𝑔 ) ‘ 𝑥 ) ↔ ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ ( 𝑘 + 1 ) ) = ( seq 𝑀 ( + , 𝑔 ) ‘ ( 𝑘 + 1 ) ) ) )
40 36 39 imbi12d ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( ( ( 𝑓 : ( 𝑀 ... 𝑥 ) –1-1-onto→ ( 𝑀 ... 𝑥 ) ∧ 𝑔 : ( 𝑀 ... 𝑥 ) ⟶ 𝐶 ) → ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ 𝑥 ) = ( seq 𝑀 ( + , 𝑔 ) ‘ 𝑥 ) ) ↔ ( ( 𝑓 : ( 𝑀 ... ( 𝑘 + 1 ) ) –1-1-onto→ ( 𝑀 ... ( 𝑘 + 1 ) ) ∧ 𝑔 : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐶 ) → ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ ( 𝑘 + 1 ) ) = ( seq 𝑀 ( + , 𝑔 ) ‘ ( 𝑘 + 1 ) ) ) ) )
41 40 2albidv ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( ∀ 𝑔 ∀ 𝑓 ( ( 𝑓 : ( 𝑀 ... 𝑥 ) –1-1-onto→ ( 𝑀 ... 𝑥 ) ∧ 𝑔 : ( 𝑀 ... 𝑥 ) ⟶ 𝐶 ) → ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ 𝑥 ) = ( seq 𝑀 ( + , 𝑔 ) ‘ 𝑥 ) ) ↔ ∀ 𝑔 ∀ 𝑓 ( ( 𝑓 : ( 𝑀 ... ( 𝑘 + 1 ) ) –1-1-onto→ ( 𝑀 ... ( 𝑘 + 1 ) ) ∧ 𝑔 : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐶 ) → ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ ( 𝑘 + 1 ) ) = ( seq 𝑀 ( + , 𝑔 ) ‘ ( 𝑘 + 1 ) ) ) ) )
42 41 imbi2d ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( ( 𝜑 → ∀ 𝑔 ∀ 𝑓 ( ( 𝑓 : ( 𝑀 ... 𝑥 ) –1-1-onto→ ( 𝑀 ... 𝑥 ) ∧ 𝑔 : ( 𝑀 ... 𝑥 ) ⟶ 𝐶 ) → ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ 𝑥 ) = ( seq 𝑀 ( + , 𝑔 ) ‘ 𝑥 ) ) ) ↔ ( 𝜑 → ∀ 𝑔 ∀ 𝑓 ( ( 𝑓 : ( 𝑀 ... ( 𝑘 + 1 ) ) –1-1-onto→ ( 𝑀 ... ( 𝑘 + 1 ) ) ∧ 𝑔 : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐶 ) → ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ ( 𝑘 + 1 ) ) = ( seq 𝑀 ( + , 𝑔 ) ‘ ( 𝑘 + 1 ) ) ) ) ) )
43 oveq2 ⊢ ( 𝑥 = 𝑁 → ( 𝑀 ... 𝑥 ) = ( 𝑀 ... 𝑁 ) )
44 f1oeq23 ⊢ ( ( ( 𝑀 ... 𝑥 ) = ( 𝑀 ... 𝑁 ) ∧ ( 𝑀 ... 𝑥 ) = ( 𝑀 ... 𝑁 ) ) → ( 𝑓 : ( 𝑀 ... 𝑥 ) –1-1-onto→ ( 𝑀 ... 𝑥 ) ↔ 𝑓 : ( 𝑀 ... 𝑁 ) –1-1-onto→ ( 𝑀 ... 𝑁 ) ) )
45 43 43 44 syl2anc ⊢ ( 𝑥 = 𝑁 → ( 𝑓 : ( 𝑀 ... 𝑥 ) –1-1-onto→ ( 𝑀 ... 𝑥 ) ↔ 𝑓 : ( 𝑀 ... 𝑁 ) –1-1-onto→ ( 𝑀 ... 𝑁 ) ) )
46 43 feq2d ⊢ ( 𝑥 = 𝑁 → ( 𝑔 : ( 𝑀 ... 𝑥 ) ⟶ 𝐶 ↔ 𝑔 : ( 𝑀 ... 𝑁 ) ⟶ 𝐶 ) )
47 45 46 anbi12d ⊢ ( 𝑥 = 𝑁 → ( ( 𝑓 : ( 𝑀 ... 𝑥 ) –1-1-onto→ ( 𝑀 ... 𝑥 ) ∧ 𝑔 : ( 𝑀 ... 𝑥 ) ⟶ 𝐶 ) ↔ ( 𝑓 : ( 𝑀 ... 𝑁 ) –1-1-onto→ ( 𝑀 ... 𝑁 ) ∧ 𝑔 : ( 𝑀 ... 𝑁 ) ⟶ 𝐶 ) ) )
48 fveq2 ⊢ ( 𝑥 = 𝑁 → ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ 𝑥 ) = ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ 𝑁 ) )
49 fveq2 ⊢ ( 𝑥 = 𝑁 → ( seq 𝑀 ( + , 𝑔 ) ‘ 𝑥 ) = ( seq 𝑀 ( + , 𝑔 ) ‘ 𝑁 ) )
50 48 49 eqeq12d ⊢ ( 𝑥 = 𝑁 → ( ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ 𝑥 ) = ( seq 𝑀 ( + , 𝑔 ) ‘ 𝑥 ) ↔ ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ 𝑁 ) = ( seq 𝑀 ( + , 𝑔 ) ‘ 𝑁 ) ) )
51 47 50 imbi12d ⊢ ( 𝑥 = 𝑁 → ( ( ( 𝑓 : ( 𝑀 ... 𝑥 ) –1-1-onto→ ( 𝑀 ... 𝑥 ) ∧ 𝑔 : ( 𝑀 ... 𝑥 ) ⟶ 𝐶 ) → ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ 𝑥 ) = ( seq 𝑀 ( + , 𝑔 ) ‘ 𝑥 ) ) ↔ ( ( 𝑓 : ( 𝑀 ... 𝑁 ) –1-1-onto→ ( 𝑀 ... 𝑁 ) ∧ 𝑔 : ( 𝑀 ... 𝑁 ) ⟶ 𝐶 ) → ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ 𝑁 ) = ( seq 𝑀 ( + , 𝑔 ) ‘ 𝑁 ) ) ) )
52 51 2albidv ⊢ ( 𝑥 = 𝑁 → ( ∀ 𝑔 ∀ 𝑓 ( ( 𝑓 : ( 𝑀 ... 𝑥 ) –1-1-onto→ ( 𝑀 ... 𝑥 ) ∧ 𝑔 : ( 𝑀 ... 𝑥 ) ⟶ 𝐶 ) → ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ 𝑥 ) = ( seq 𝑀 ( + , 𝑔 ) ‘ 𝑥 ) ) ↔ ∀ 𝑔 ∀ 𝑓 ( ( 𝑓 : ( 𝑀 ... 𝑁 ) –1-1-onto→ ( 𝑀 ... 𝑁 ) ∧ 𝑔 : ( 𝑀 ... 𝑁 ) ⟶ 𝐶 ) → ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ 𝑁 ) = ( seq 𝑀 ( + , 𝑔 ) ‘ 𝑁 ) ) ) )
53 52 imbi2d ⊢ ( 𝑥 = 𝑁 → ( ( 𝜑 → ∀ 𝑔 ∀ 𝑓 ( ( 𝑓 : ( 𝑀 ... 𝑥 ) –1-1-onto→ ( 𝑀 ... 𝑥 ) ∧ 𝑔 : ( 𝑀 ... 𝑥 ) ⟶ 𝐶 ) → ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ 𝑥 ) = ( seq 𝑀 ( + , 𝑔 ) ‘ 𝑥 ) ) ) ↔ ( 𝜑 → ∀ 𝑔 ∀ 𝑓 ( ( 𝑓 : ( 𝑀 ... 𝑁 ) –1-1-onto→ ( 𝑀 ... 𝑁 ) ∧ 𝑔 : ( 𝑀 ... 𝑁 ) ⟶ 𝐶 ) → ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ 𝑁 ) = ( seq 𝑀 ( + , 𝑔 ) ‘ 𝑁 ) ) ) ) )
54 f1of ⊢ ( 𝑓 : ( 𝑀 ... 𝑀 ) –1-1-onto→ ( 𝑀 ... 𝑀 ) → 𝑓 : ( 𝑀 ... 𝑀 ) ⟶ ( 𝑀 ... 𝑀 ) )
55 54 adantr ⊢ ( ( 𝑓 : ( 𝑀 ... 𝑀 ) –1-1-onto→ ( 𝑀 ... 𝑀 ) ∧ 𝑔 : ( 𝑀 ... 𝑀 ) ⟶ 𝐶 ) → 𝑓 : ( 𝑀 ... 𝑀 ) ⟶ ( 𝑀 ... 𝑀 ) )
56 elfz3 ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ( 𝑀 ... 𝑀 ) )
57 fvco3 ⊢ ( ( 𝑓 : ( 𝑀 ... 𝑀 ) ⟶ ( 𝑀 ... 𝑀 ) ∧ 𝑀 ∈ ( 𝑀 ... 𝑀 ) ) → ( ( 𝑔 ∘ 𝑓 ) ‘ 𝑀 ) = ( 𝑔 ‘ ( 𝑓 ‘ 𝑀 ) ) )
58 55 56 57 syl2anr ⊢ ( ( 𝑀 ∈ ℤ ∧ ( 𝑓 : ( 𝑀 ... 𝑀 ) –1-1-onto→ ( 𝑀 ... 𝑀 ) ∧ 𝑔 : ( 𝑀 ... 𝑀 ) ⟶ 𝐶 ) ) → ( ( 𝑔 ∘ 𝑓 ) ‘ 𝑀 ) = ( 𝑔 ‘ ( 𝑓 ‘ 𝑀 ) ) )
59 ffvelcdm ⊢ ( ( 𝑓 : ( 𝑀 ... 𝑀 ) ⟶ ( 𝑀 ... 𝑀 ) ∧ 𝑀 ∈ ( 𝑀 ... 𝑀 ) ) → ( 𝑓 ‘ 𝑀 ) ∈ ( 𝑀 ... 𝑀 ) )
60 54 56 59 syl2anr ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑓 : ( 𝑀 ... 𝑀 ) –1-1-onto→ ( 𝑀 ... 𝑀 ) ) → ( 𝑓 ‘ 𝑀 ) ∈ ( 𝑀 ... 𝑀 ) )
61 fzsn ⊢ ( 𝑀 ∈ ℤ → ( 𝑀 ... 𝑀 ) = { 𝑀 } )
62 61 eleq2d ⊢ ( 𝑀 ∈ ℤ → ( ( 𝑓 ‘ 𝑀 ) ∈ ( 𝑀 ... 𝑀 ) ↔ ( 𝑓 ‘ 𝑀 ) ∈ { 𝑀 } ) )
63 elsni ⊢ ( ( 𝑓 ‘ 𝑀 ) ∈ { 𝑀 } → ( 𝑓 ‘ 𝑀 ) = 𝑀 )
64 62 63 biimtrdi ⊢ ( 𝑀 ∈ ℤ → ( ( 𝑓 ‘ 𝑀 ) ∈ ( 𝑀 ... 𝑀 ) → ( 𝑓 ‘ 𝑀 ) = 𝑀 ) )
65 64 imp ⊢ ( ( 𝑀 ∈ ℤ ∧ ( 𝑓 ‘ 𝑀 ) ∈ ( 𝑀 ... 𝑀 ) ) → ( 𝑓 ‘ 𝑀 ) = 𝑀 )
66 60 65 syldan ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑓 : ( 𝑀 ... 𝑀 ) –1-1-onto→ ( 𝑀 ... 𝑀 ) ) → ( 𝑓 ‘ 𝑀 ) = 𝑀 )
67 66 adantrr ⊢ ( ( 𝑀 ∈ ℤ ∧ ( 𝑓 : ( 𝑀 ... 𝑀 ) –1-1-onto→ ( 𝑀 ... 𝑀 ) ∧ 𝑔 : ( 𝑀 ... 𝑀 ) ⟶ 𝐶 ) ) → ( 𝑓 ‘ 𝑀 ) = 𝑀 )
68 67 fveq2d ⊢ ( ( 𝑀 ∈ ℤ ∧ ( 𝑓 : ( 𝑀 ... 𝑀 ) –1-1-onto→ ( 𝑀 ... 𝑀 ) ∧ 𝑔 : ( 𝑀 ... 𝑀 ) ⟶ 𝐶 ) ) → ( 𝑔 ‘ ( 𝑓 ‘ 𝑀 ) ) = ( 𝑔 ‘ 𝑀 ) )
69 58 68 eqtrd ⊢ ( ( 𝑀 ∈ ℤ ∧ ( 𝑓 : ( 𝑀 ... 𝑀 ) –1-1-onto→ ( 𝑀 ... 𝑀 ) ∧ 𝑔 : ( 𝑀 ... 𝑀 ) ⟶ 𝐶 ) ) → ( ( 𝑔 ∘ 𝑓 ) ‘ 𝑀 ) = ( 𝑔 ‘ 𝑀 ) )
70 seq1 ⊢ ( 𝑀 ∈ ℤ → ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ 𝑀 ) = ( ( 𝑔 ∘ 𝑓 ) ‘ 𝑀 ) )
71 70 adantr ⊢ ( ( 𝑀 ∈ ℤ ∧ ( 𝑓 : ( 𝑀 ... 𝑀 ) –1-1-onto→ ( 𝑀 ... 𝑀 ) ∧ 𝑔 : ( 𝑀 ... 𝑀 ) ⟶ 𝐶 ) ) → ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ 𝑀 ) = ( ( 𝑔 ∘ 𝑓 ) ‘ 𝑀 ) )
72 seq1 ⊢ ( 𝑀 ∈ ℤ → ( seq 𝑀 ( + , 𝑔 ) ‘ 𝑀 ) = ( 𝑔 ‘ 𝑀 ) )
73 72 adantr ⊢ ( ( 𝑀 ∈ ℤ ∧ ( 𝑓 : ( 𝑀 ... 𝑀 ) –1-1-onto→ ( 𝑀 ... 𝑀 ) ∧ 𝑔 : ( 𝑀 ... 𝑀 ) ⟶ 𝐶 ) ) → ( seq 𝑀 ( + , 𝑔 ) ‘ 𝑀 ) = ( 𝑔 ‘ 𝑀 ) )
74 69 71 73 3eqtr4d ⊢ ( ( 𝑀 ∈ ℤ ∧ ( 𝑓 : ( 𝑀 ... 𝑀 ) –1-1-onto→ ( 𝑀 ... 𝑀 ) ∧ 𝑔 : ( 𝑀 ... 𝑀 ) ⟶ 𝐶 ) ) → ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ 𝑀 ) = ( seq 𝑀 ( + , 𝑔 ) ‘ 𝑀 ) )
75 74 ex ⊢ ( 𝑀 ∈ ℤ → ( ( 𝑓 : ( 𝑀 ... 𝑀 ) –1-1-onto→ ( 𝑀 ... 𝑀 ) ∧ 𝑔 : ( 𝑀 ... 𝑀 ) ⟶ 𝐶 ) → ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ 𝑀 ) = ( seq 𝑀 ( + , 𝑔 ) ‘ 𝑀 ) ) )
76 75 alrimivv ⊢ ( 𝑀 ∈ ℤ → ∀ 𝑔 ∀ 𝑓 ( ( 𝑓 : ( 𝑀 ... 𝑀 ) –1-1-onto→ ( 𝑀 ... 𝑀 ) ∧ 𝑔 : ( 𝑀 ... 𝑀 ) ⟶ 𝐶 ) → ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ 𝑀 ) = ( seq 𝑀 ( + , 𝑔 ) ‘ 𝑀 ) ) )
77 76 a1d ⊢ ( 𝑀 ∈ ℤ → ( 𝜑 → ∀ 𝑔 ∀ 𝑓 ( ( 𝑓 : ( 𝑀 ... 𝑀 ) –1-1-onto→ ( 𝑀 ... 𝑀 ) ∧ 𝑔 : ( 𝑀 ... 𝑀 ) ⟶ 𝐶 ) → ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ 𝑀 ) = ( seq 𝑀 ( + , 𝑔 ) ‘ 𝑀 ) ) ) )
78 f1oeq1 ⊢ ( 𝑓 = 𝑡 → ( 𝑓 : ( 𝑀 ... 𝑘 ) –1-1-onto→ ( 𝑀 ... 𝑘 ) ↔ 𝑡 : ( 𝑀 ... 𝑘 ) –1-1-onto→ ( 𝑀 ... 𝑘 ) ) )
79 feq1 ⊢ ( 𝑔 = 𝑠 → ( 𝑔 : ( 𝑀 ... 𝑘 ) ⟶ 𝐶 ↔ 𝑠 : ( 𝑀 ... 𝑘 ) ⟶ 𝐶 ) )
80 78 79 bi2anan9r ⊢ ( ( 𝑔 = 𝑠 ∧ 𝑓 = 𝑡 ) → ( ( 𝑓 : ( 𝑀 ... 𝑘 ) –1-1-onto→ ( 𝑀 ... 𝑘 ) ∧ 𝑔 : ( 𝑀 ... 𝑘 ) ⟶ 𝐶 ) ↔ ( 𝑡 : ( 𝑀 ... 𝑘 ) –1-1-onto→ ( 𝑀 ... 𝑘 ) ∧ 𝑠 : ( 𝑀 ... 𝑘 ) ⟶ 𝐶 ) ) )
81 coeq1 ⊢ ( 𝑔 = 𝑠 → ( 𝑔 ∘ 𝑓 ) = ( 𝑠 ∘ 𝑓 ) )
82 coeq2 ⊢ ( 𝑓 = 𝑡 → ( 𝑠 ∘ 𝑓 ) = ( 𝑠 ∘ 𝑡 ) )
83 81 82 sylan9eq ⊢ ( ( 𝑔 = 𝑠 ∧ 𝑓 = 𝑡 ) → ( 𝑔 ∘ 𝑓 ) = ( 𝑠 ∘ 𝑡 ) )
84 83 seqeq3d ⊢ ( ( 𝑔 = 𝑠 ∧ 𝑓 = 𝑡 ) → seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) = seq 𝑀 ( + , ( 𝑠 ∘ 𝑡 ) ) )
85 84 fveq1d ⊢ ( ( 𝑔 = 𝑠 ∧ 𝑓 = 𝑡 ) → ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ 𝑘 ) = ( seq 𝑀 ( + , ( 𝑠 ∘ 𝑡 ) ) ‘ 𝑘 ) )
86 simpl ⊢ ( ( 𝑔 = 𝑠 ∧ 𝑓 = 𝑡 ) → 𝑔 = 𝑠 )
87 86 seqeq3d ⊢ ( ( 𝑔 = 𝑠 ∧ 𝑓 = 𝑡 ) → seq 𝑀 ( + , 𝑔 ) = seq 𝑀 ( + , 𝑠 ) )
88 87 fveq1d ⊢ ( ( 𝑔 = 𝑠 ∧ 𝑓 = 𝑡 ) → ( seq 𝑀 ( + , 𝑔 ) ‘ 𝑘 ) = ( seq 𝑀 ( + , 𝑠 ) ‘ 𝑘 ) )
89 85 88 eqeq12d ⊢ ( ( 𝑔 = 𝑠 ∧ 𝑓 = 𝑡 ) → ( ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ 𝑘 ) = ( seq 𝑀 ( + , 𝑔 ) ‘ 𝑘 ) ↔ ( seq 𝑀 ( + , ( 𝑠 ∘ 𝑡 ) ) ‘ 𝑘 ) = ( seq 𝑀 ( + , 𝑠 ) ‘ 𝑘 ) ) )
90 80 89 imbi12d ⊢ ( ( 𝑔 = 𝑠 ∧ 𝑓 = 𝑡 ) → ( ( ( 𝑓 : ( 𝑀 ... 𝑘 ) –1-1-onto→ ( 𝑀 ... 𝑘 ) ∧ 𝑔 : ( 𝑀 ... 𝑘 ) ⟶ 𝐶 ) → ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ 𝑘 ) = ( seq 𝑀 ( + , 𝑔 ) ‘ 𝑘 ) ) ↔ ( ( 𝑡 : ( 𝑀 ... 𝑘 ) –1-1-onto→ ( 𝑀 ... 𝑘 ) ∧ 𝑠 : ( 𝑀 ... 𝑘 ) ⟶ 𝐶 ) → ( seq 𝑀 ( + , ( 𝑠 ∘ 𝑡 ) ) ‘ 𝑘 ) = ( seq 𝑀 ( + , 𝑠 ) ‘ 𝑘 ) ) ) )
91 90 cbval2vw ⊢ ( ∀ 𝑔 ∀ 𝑓 ( ( 𝑓 : ( 𝑀 ... 𝑘 ) –1-1-onto→ ( 𝑀 ... 𝑘 ) ∧ 𝑔 : ( 𝑀 ... 𝑘 ) ⟶ 𝐶 ) → ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ 𝑘 ) = ( seq 𝑀 ( + , 𝑔 ) ‘ 𝑘 ) ) ↔ ∀ 𝑠 ∀ 𝑡 ( ( 𝑡 : ( 𝑀 ... 𝑘 ) –1-1-onto→ ( 𝑀 ... 𝑘 ) ∧ 𝑠 : ( 𝑀 ... 𝑘 ) ⟶ 𝐶 ) → ( seq 𝑀 ( + , ( 𝑠 ∘ 𝑡 ) ) ‘ 𝑘 ) = ( seq 𝑀 ( + , 𝑠 ) ‘ 𝑘 ) ) )
92 simplll ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ ∀ 𝑔 ∀ 𝑓 ( ( 𝑓 : ( 𝑀 ... 𝑘 ) –1-1-onto→ ( 𝑀 ... 𝑘 ) ∧ 𝑔 : ( 𝑀 ... 𝑘 ) ⟶ 𝐶 ) → ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ 𝑘 ) = ( seq 𝑀 ( + , 𝑔 ) ‘ 𝑘 ) ) ) ∧ ( 𝑓 : ( 𝑀 ... ( 𝑘 + 1 ) ) –1-1-onto→ ( 𝑀 ... ( 𝑘 + 1 ) ) ∧ 𝑔 : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐶 ) ) → 𝜑 )
93 92 1 sylan ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ ∀ 𝑔 ∀ 𝑓 ( ( 𝑓 : ( 𝑀 ... 𝑘 ) –1-1-onto→ ( 𝑀 ... 𝑘 ) ∧ 𝑔 : ( 𝑀 ... 𝑘 ) ⟶ 𝐶 ) → ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ 𝑘 ) = ( seq 𝑀 ( + , 𝑔 ) ‘ 𝑘 ) ) ) ∧ ( 𝑓 : ( 𝑀 ... ( 𝑘 + 1 ) ) –1-1-onto→ ( 𝑀 ... ( 𝑘 + 1 ) ) ∧ 𝑔 : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐶 ) ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
94 92 2 sylan ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ ∀ 𝑔 ∀ 𝑓 ( ( 𝑓 : ( 𝑀 ... 𝑘 ) –1-1-onto→ ( 𝑀 ... 𝑘 ) ∧ 𝑔 : ( 𝑀 ... 𝑘 ) ⟶ 𝐶 ) → ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ 𝑘 ) = ( seq 𝑀 ( + , 𝑔 ) ‘ 𝑘 ) ) ) ∧ ( 𝑓 : ( 𝑀 ... ( 𝑘 + 1 ) ) –1-1-onto→ ( 𝑀 ... ( 𝑘 + 1 ) ) ∧ 𝑔 : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐶 ) ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) )
95 92 3 sylan ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ ∀ 𝑔 ∀ 𝑓 ( ( 𝑓 : ( 𝑀 ... 𝑘 ) –1-1-onto→ ( 𝑀 ... 𝑘 ) ∧ 𝑔 : ( 𝑀 ... 𝑘 ) ⟶ 𝐶 ) → ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ 𝑘 ) = ( seq 𝑀 ( + , 𝑔 ) ‘ 𝑘 ) ) ) ∧ ( 𝑓 : ( 𝑀 ... ( 𝑘 + 1 ) ) –1-1-onto→ ( 𝑀 ... ( 𝑘 + 1 ) ) ∧ 𝑔 : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐶 ) ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) )
96 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ ∀ 𝑔 ∀ 𝑓 ( ( 𝑓 : ( 𝑀 ... 𝑘 ) –1-1-onto→ ( 𝑀 ... 𝑘 ) ∧ 𝑔 : ( 𝑀 ... 𝑘 ) ⟶ 𝐶 ) → ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ 𝑘 ) = ( seq 𝑀 ( + , 𝑔 ) ‘ 𝑘 ) ) ) ∧ ( 𝑓 : ( 𝑀 ... ( 𝑘 + 1 ) ) –1-1-onto→ ( 𝑀 ... ( 𝑘 + 1 ) ) ∧ 𝑔 : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐶 ) ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) )
97 92 5 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ ∀ 𝑔 ∀ 𝑓 ( ( 𝑓 : ( 𝑀 ... 𝑘 ) –1-1-onto→ ( 𝑀 ... 𝑘 ) ∧ 𝑔 : ( 𝑀 ... 𝑘 ) ⟶ 𝐶 ) → ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ 𝑘 ) = ( seq 𝑀 ( + , 𝑔 ) ‘ 𝑘 ) ) ) ∧ ( 𝑓 : ( 𝑀 ... ( 𝑘 + 1 ) ) –1-1-onto→ ( 𝑀 ... ( 𝑘 + 1 ) ) ∧ 𝑔 : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐶 ) ) → 𝐶 ⊆ 𝑆 )
98 simprl ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ ∀ 𝑔 ∀ 𝑓 ( ( 𝑓 : ( 𝑀 ... 𝑘 ) –1-1-onto→ ( 𝑀 ... 𝑘 ) ∧ 𝑔 : ( 𝑀 ... 𝑘 ) ⟶ 𝐶 ) → ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ 𝑘 ) = ( seq 𝑀 ( + , 𝑔 ) ‘ 𝑘 ) ) ) ∧ ( 𝑓 : ( 𝑀 ... ( 𝑘 + 1 ) ) –1-1-onto→ ( 𝑀 ... ( 𝑘 + 1 ) ) ∧ 𝑔 : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐶 ) ) → 𝑓 : ( 𝑀 ... ( 𝑘 + 1 ) ) –1-1-onto→ ( 𝑀 ... ( 𝑘 + 1 ) ) )
99 simprr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ ∀ 𝑔 ∀ 𝑓 ( ( 𝑓 : ( 𝑀 ... 𝑘 ) –1-1-onto→ ( 𝑀 ... 𝑘 ) ∧ 𝑔 : ( 𝑀 ... 𝑘 ) ⟶ 𝐶 ) → ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ 𝑘 ) = ( seq 𝑀 ( + , 𝑔 ) ‘ 𝑘 ) ) ) ∧ ( 𝑓 : ( 𝑀 ... ( 𝑘 + 1 ) ) –1-1-onto→ ( 𝑀 ... ( 𝑘 + 1 ) ) ∧ 𝑔 : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐶 ) ) → 𝑔 : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐶 )
100 eqid ⊢ ( 𝑤 ∈ ( 𝑀 ... 𝑘 ) ↦ ( 𝑓 ‘ if ( 𝑤 < ( ◡ 𝑓 ‘ ( 𝑘 + 1 ) ) , 𝑤 , ( 𝑤 + 1 ) ) ) ) = ( 𝑤 ∈ ( 𝑀 ... 𝑘 ) ↦ ( 𝑓 ‘ if ( 𝑤 < ( ◡ 𝑓 ‘ ( 𝑘 + 1 ) ) , 𝑤 , ( 𝑤 + 1 ) ) ) )
101 eqid ⊢ ( ◡ 𝑓 ‘ ( 𝑘 + 1 ) ) = ( ◡ 𝑓 ‘ ( 𝑘 + 1 ) )
102 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ ∀ 𝑔 ∀ 𝑓 ( ( 𝑓 : ( 𝑀 ... 𝑘 ) –1-1-onto→ ( 𝑀 ... 𝑘 ) ∧ 𝑔 : ( 𝑀 ... 𝑘 ) ⟶ 𝐶 ) → ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ 𝑘 ) = ( seq 𝑀 ( + , 𝑔 ) ‘ 𝑘 ) ) ) ∧ ( 𝑓 : ( 𝑀 ... ( 𝑘 + 1 ) ) –1-1-onto→ ( 𝑀 ... ( 𝑘 + 1 ) ) ∧ 𝑔 : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐶 ) ) → ∀ 𝑔 ∀ 𝑓 ( ( 𝑓 : ( 𝑀 ... 𝑘 ) –1-1-onto→ ( 𝑀 ... 𝑘 ) ∧ 𝑔 : ( 𝑀 ... 𝑘 ) ⟶ 𝐶 ) → ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ 𝑘 ) = ( seq 𝑀 ( + , 𝑔 ) ‘ 𝑘 ) ) )
103 102 91 sylib ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ ∀ 𝑔 ∀ 𝑓 ( ( 𝑓 : ( 𝑀 ... 𝑘 ) –1-1-onto→ ( 𝑀 ... 𝑘 ) ∧ 𝑔 : ( 𝑀 ... 𝑘 ) ⟶ 𝐶 ) → ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ 𝑘 ) = ( seq 𝑀 ( + , 𝑔 ) ‘ 𝑘 ) ) ) ∧ ( 𝑓 : ( 𝑀 ... ( 𝑘 + 1 ) ) –1-1-onto→ ( 𝑀 ... ( 𝑘 + 1 ) ) ∧ 𝑔 : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐶 ) ) → ∀ 𝑠 ∀ 𝑡 ( ( 𝑡 : ( 𝑀 ... 𝑘 ) –1-1-onto→ ( 𝑀 ... 𝑘 ) ∧ 𝑠 : ( 𝑀 ... 𝑘 ) ⟶ 𝐶 ) → ( seq 𝑀 ( + , ( 𝑠 ∘ 𝑡 ) ) ‘ 𝑘 ) = ( seq 𝑀 ( + , 𝑠 ) ‘ 𝑘 ) ) )
104 93 94 95 96 97 98 99 100 101 103 seqf1olem2 ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ ∀ 𝑔 ∀ 𝑓 ( ( 𝑓 : ( 𝑀 ... 𝑘 ) –1-1-onto→ ( 𝑀 ... 𝑘 ) ∧ 𝑔 : ( 𝑀 ... 𝑘 ) ⟶ 𝐶 ) → ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ 𝑘 ) = ( seq 𝑀 ( + , 𝑔 ) ‘ 𝑘 ) ) ) ∧ ( 𝑓 : ( 𝑀 ... ( 𝑘 + 1 ) ) –1-1-onto→ ( 𝑀 ... ( 𝑘 + 1 ) ) ∧ 𝑔 : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐶 ) ) → ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ ( 𝑘 + 1 ) ) = ( seq 𝑀 ( + , 𝑔 ) ‘ ( 𝑘 + 1 ) ) )
105 104 exp31 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ∀ 𝑔 ∀ 𝑓 ( ( 𝑓 : ( 𝑀 ... 𝑘 ) –1-1-onto→ ( 𝑀 ... 𝑘 ) ∧ 𝑔 : ( 𝑀 ... 𝑘 ) ⟶ 𝐶 ) → ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ 𝑘 ) = ( seq 𝑀 ( + , 𝑔 ) ‘ 𝑘 ) ) → ( ( 𝑓 : ( 𝑀 ... ( 𝑘 + 1 ) ) –1-1-onto→ ( 𝑀 ... ( 𝑘 + 1 ) ) ∧ 𝑔 : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐶 ) → ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ ( 𝑘 + 1 ) ) = ( seq 𝑀 ( + , 𝑔 ) ‘ ( 𝑘 + 1 ) ) ) ) )
106 91 105 biimtrrid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ∀ 𝑠 ∀ 𝑡 ( ( 𝑡 : ( 𝑀 ... 𝑘 ) –1-1-onto→ ( 𝑀 ... 𝑘 ) ∧ 𝑠 : ( 𝑀 ... 𝑘 ) ⟶ 𝐶 ) → ( seq 𝑀 ( + , ( 𝑠 ∘ 𝑡 ) ) ‘ 𝑘 ) = ( seq 𝑀 ( + , 𝑠 ) ‘ 𝑘 ) ) → ( ( 𝑓 : ( 𝑀 ... ( 𝑘 + 1 ) ) –1-1-onto→ ( 𝑀 ... ( 𝑘 + 1 ) ) ∧ 𝑔 : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐶 ) → ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ ( 𝑘 + 1 ) ) = ( seq 𝑀 ( + , 𝑔 ) ‘ ( 𝑘 + 1 ) ) ) ) )
107 106 alrimdv ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ∀ 𝑠 ∀ 𝑡 ( ( 𝑡 : ( 𝑀 ... 𝑘 ) –1-1-onto→ ( 𝑀 ... 𝑘 ) ∧ 𝑠 : ( 𝑀 ... 𝑘 ) ⟶ 𝐶 ) → ( seq 𝑀 ( + , ( 𝑠 ∘ 𝑡 ) ) ‘ 𝑘 ) = ( seq 𝑀 ( + , 𝑠 ) ‘ 𝑘 ) ) → ∀ 𝑓 ( ( 𝑓 : ( 𝑀 ... ( 𝑘 + 1 ) ) –1-1-onto→ ( 𝑀 ... ( 𝑘 + 1 ) ) ∧ 𝑔 : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐶 ) → ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ ( 𝑘 + 1 ) ) = ( seq 𝑀 ( + , 𝑔 ) ‘ ( 𝑘 + 1 ) ) ) ) )
108 107 alrimdv ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ∀ 𝑠 ∀ 𝑡 ( ( 𝑡 : ( 𝑀 ... 𝑘 ) –1-1-onto→ ( 𝑀 ... 𝑘 ) ∧ 𝑠 : ( 𝑀 ... 𝑘 ) ⟶ 𝐶 ) → ( seq 𝑀 ( + , ( 𝑠 ∘ 𝑡 ) ) ‘ 𝑘 ) = ( seq 𝑀 ( + , 𝑠 ) ‘ 𝑘 ) ) → ∀ 𝑔 ∀ 𝑓 ( ( 𝑓 : ( 𝑀 ... ( 𝑘 + 1 ) ) –1-1-onto→ ( 𝑀 ... ( 𝑘 + 1 ) ) ∧ 𝑔 : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐶 ) → ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ ( 𝑘 + 1 ) ) = ( seq 𝑀 ( + , 𝑔 ) ‘ ( 𝑘 + 1 ) ) ) ) )
109 91 108 biimtrid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ∀ 𝑔 ∀ 𝑓 ( ( 𝑓 : ( 𝑀 ... 𝑘 ) –1-1-onto→ ( 𝑀 ... 𝑘 ) ∧ 𝑔 : ( 𝑀 ... 𝑘 ) ⟶ 𝐶 ) → ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ 𝑘 ) = ( seq 𝑀 ( + , 𝑔 ) ‘ 𝑘 ) ) → ∀ 𝑔 ∀ 𝑓 ( ( 𝑓 : ( 𝑀 ... ( 𝑘 + 1 ) ) –1-1-onto→ ( 𝑀 ... ( 𝑘 + 1 ) ) ∧ 𝑔 : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐶 ) → ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ ( 𝑘 + 1 ) ) = ( seq 𝑀 ( + , 𝑔 ) ‘ ( 𝑘 + 1 ) ) ) ) )
110 109 expcom ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝜑 → ( ∀ 𝑔 ∀ 𝑓 ( ( 𝑓 : ( 𝑀 ... 𝑘 ) –1-1-onto→ ( 𝑀 ... 𝑘 ) ∧ 𝑔 : ( 𝑀 ... 𝑘 ) ⟶ 𝐶 ) → ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ 𝑘 ) = ( seq 𝑀 ( + , 𝑔 ) ‘ 𝑘 ) ) → ∀ 𝑔 ∀ 𝑓 ( ( 𝑓 : ( 𝑀 ... ( 𝑘 + 1 ) ) –1-1-onto→ ( 𝑀 ... ( 𝑘 + 1 ) ) ∧ 𝑔 : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐶 ) → ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ ( 𝑘 + 1 ) ) = ( seq 𝑀 ( + , 𝑔 ) ‘ ( 𝑘 + 1 ) ) ) ) ) )
111 110 a2d ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝜑 → ∀ 𝑔 ∀ 𝑓 ( ( 𝑓 : ( 𝑀 ... 𝑘 ) –1-1-onto→ ( 𝑀 ... 𝑘 ) ∧ 𝑔 : ( 𝑀 ... 𝑘 ) ⟶ 𝐶 ) → ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ 𝑘 ) = ( seq 𝑀 ( + , 𝑔 ) ‘ 𝑘 ) ) ) → ( 𝜑 → ∀ 𝑔 ∀ 𝑓 ( ( 𝑓 : ( 𝑀 ... ( 𝑘 + 1 ) ) –1-1-onto→ ( 𝑀 ... ( 𝑘 + 1 ) ) ∧ 𝑔 : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐶 ) → ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ ( 𝑘 + 1 ) ) = ( seq 𝑀 ( + , 𝑔 ) ‘ ( 𝑘 + 1 ) ) ) ) ) )
112 20 31 42 53 77 111 uzind4 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝜑 → ∀ 𝑔 ∀ 𝑓 ( ( 𝑓 : ( 𝑀 ... 𝑁 ) –1-1-onto→ ( 𝑀 ... 𝑁 ) ∧ 𝑔 : ( 𝑀 ... 𝑁 ) ⟶ 𝐶 ) → ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ 𝑁 ) = ( seq 𝑀 ( + , 𝑔 ) ‘ 𝑁 ) ) ) )
113 4 112 mpcom ⊢ ( 𝜑 → ∀ 𝑔 ∀ 𝑓 ( ( 𝑓 : ( 𝑀 ... 𝑁 ) –1-1-onto→ ( 𝑀 ... 𝑁 ) ∧ 𝑔 : ( 𝑀 ... 𝑁 ) ⟶ 𝐶 ) → ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ 𝑁 ) = ( seq 𝑀 ( + , 𝑔 ) ‘ 𝑁 ) ) )
114 fvex ⊢ ( 𝐺 ‘ 𝑥 ) ∈ V
115 eqid ⊢ ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝐺 ‘ 𝑥 ) ) = ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝐺 ‘ 𝑥 ) )
116 114 115 fnmpti ⊢ ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝐺 ‘ 𝑥 ) ) Fn ( 𝑀 ... 𝑁 )
117 fzfi ⊢ ( 𝑀 ... 𝑁 ) ∈ Fin
118 fnfi ⊢ ( ( ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝐺 ‘ 𝑥 ) ) Fn ( 𝑀 ... 𝑁 ) ∧ ( 𝑀 ... 𝑁 ) ∈ Fin ) → ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝐺 ‘ 𝑥 ) ) ∈ Fin )
119 116 117 118 mp2an ⊢ ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝐺 ‘ 𝑥 ) ) ∈ Fin
120 f1of ⊢ ( 𝐹 : ( 𝑀 ... 𝑁 ) –1-1-onto→ ( 𝑀 ... 𝑁 ) → 𝐹 : ( 𝑀 ... 𝑁 ) ⟶ ( 𝑀 ... 𝑁 ) )
121 6 120 syl ⊢ ( 𝜑 → 𝐹 : ( 𝑀 ... 𝑁 ) ⟶ ( 𝑀 ... 𝑁 ) )
122 ovexd ⊢ ( 𝜑 → ( 𝑀 ... 𝑁 ) ∈ V )
123 fex2 ⊢ ( ( 𝐹 : ( 𝑀 ... 𝑁 ) ⟶ ( 𝑀 ... 𝑁 ) ∧ ( 𝑀 ... 𝑁 ) ∈ V ∧ ( 𝑀 ... 𝑁 ) ∈ V ) → 𝐹 ∈ V )
124 121 122 122 123 syl3anc ⊢ ( 𝜑 → 𝐹 ∈ V )
125 f1oeq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 : ( 𝑀 ... 𝑁 ) –1-1-onto→ ( 𝑀 ... 𝑁 ) ↔ 𝐹 : ( 𝑀 ... 𝑁 ) –1-1-onto→ ( 𝑀 ... 𝑁 ) ) )
126 feq1 ⊢ ( 𝑔 = ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝐺 ‘ 𝑥 ) ) → ( 𝑔 : ( 𝑀 ... 𝑁 ) ⟶ 𝐶 ↔ ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝐺 ‘ 𝑥 ) ) : ( 𝑀 ... 𝑁 ) ⟶ 𝐶 ) )
127 125 126 bi2anan9r ⊢ ( ( 𝑔 = ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝐺 ‘ 𝑥 ) ) ∧ 𝑓 = 𝐹 ) → ( ( 𝑓 : ( 𝑀 ... 𝑁 ) –1-1-onto→ ( 𝑀 ... 𝑁 ) ∧ 𝑔 : ( 𝑀 ... 𝑁 ) ⟶ 𝐶 ) ↔ ( 𝐹 : ( 𝑀 ... 𝑁 ) –1-1-onto→ ( 𝑀 ... 𝑁 ) ∧ ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝐺 ‘ 𝑥 ) ) : ( 𝑀 ... 𝑁 ) ⟶ 𝐶 ) ) )
128 coeq1 ⊢ ( 𝑔 = ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝐺 ‘ 𝑥 ) ) → ( 𝑔 ∘ 𝑓 ) = ( ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝐺 ‘ 𝑥 ) ) ∘ 𝑓 ) )
129 coeq2 ⊢ ( 𝑓 = 𝐹 → ( ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝐺 ‘ 𝑥 ) ) ∘ 𝑓 ) = ( ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝐺 ‘ 𝑥 ) ) ∘ 𝐹 ) )
130 128 129 sylan9eq ⊢ ( ( 𝑔 = ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝐺 ‘ 𝑥 ) ) ∧ 𝑓 = 𝐹 ) → ( 𝑔 ∘ 𝑓 ) = ( ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝐺 ‘ 𝑥 ) ) ∘ 𝐹 ) )
131 130 seqeq3d ⊢ ( ( 𝑔 = ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝐺 ‘ 𝑥 ) ) ∧ 𝑓 = 𝐹 ) → seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) = seq 𝑀 ( + , ( ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝐺 ‘ 𝑥 ) ) ∘ 𝐹 ) ) )
132 131 fveq1d ⊢ ( ( 𝑔 = ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝐺 ‘ 𝑥 ) ) ∧ 𝑓 = 𝐹 ) → ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ 𝑁 ) = ( seq 𝑀 ( + , ( ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝐺 ‘ 𝑥 ) ) ∘ 𝐹 ) ) ‘ 𝑁 ) )
133 simpl ⊢ ( ( 𝑔 = ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝐺 ‘ 𝑥 ) ) ∧ 𝑓 = 𝐹 ) → 𝑔 = ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝐺 ‘ 𝑥 ) ) )
134 133 seqeq3d ⊢ ( ( 𝑔 = ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝐺 ‘ 𝑥 ) ) ∧ 𝑓 = 𝐹 ) → seq 𝑀 ( + , 𝑔 ) = seq 𝑀 ( + , ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝐺 ‘ 𝑥 ) ) ) )
135 134 fveq1d ⊢ ( ( 𝑔 = ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝐺 ‘ 𝑥 ) ) ∧ 𝑓 = 𝐹 ) → ( seq 𝑀 ( + , 𝑔 ) ‘ 𝑁 ) = ( seq 𝑀 ( + , ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝐺 ‘ 𝑥 ) ) ) ‘ 𝑁 ) )
136 132 135 eqeq12d ⊢ ( ( 𝑔 = ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝐺 ‘ 𝑥 ) ) ∧ 𝑓 = 𝐹 ) → ( ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ 𝑁 ) = ( seq 𝑀 ( + , 𝑔 ) ‘ 𝑁 ) ↔ ( seq 𝑀 ( + , ( ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝐺 ‘ 𝑥 ) ) ∘ 𝐹 ) ) ‘ 𝑁 ) = ( seq 𝑀 ( + , ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝐺 ‘ 𝑥 ) ) ) ‘ 𝑁 ) ) )
137 127 136 imbi12d ⊢ ( ( 𝑔 = ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝐺 ‘ 𝑥 ) ) ∧ 𝑓 = 𝐹 ) → ( ( ( 𝑓 : ( 𝑀 ... 𝑁 ) –1-1-onto→ ( 𝑀 ... 𝑁 ) ∧ 𝑔 : ( 𝑀 ... 𝑁 ) ⟶ 𝐶 ) → ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ 𝑁 ) = ( seq 𝑀 ( + , 𝑔 ) ‘ 𝑁 ) ) ↔ ( ( 𝐹 : ( 𝑀 ... 𝑁 ) –1-1-onto→ ( 𝑀 ... 𝑁 ) ∧ ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝐺 ‘ 𝑥 ) ) : ( 𝑀 ... 𝑁 ) ⟶ 𝐶 ) → ( seq 𝑀 ( + , ( ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝐺 ‘ 𝑥 ) ) ∘ 𝐹 ) ) ‘ 𝑁 ) = ( seq 𝑀 ( + , ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝐺 ‘ 𝑥 ) ) ) ‘ 𝑁 ) ) ) )
138 137 spc2gv ⊢ ( ( ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝐺 ‘ 𝑥 ) ) ∈ Fin ∧ 𝐹 ∈ V ) → ( ∀ 𝑔 ∀ 𝑓 ( ( 𝑓 : ( 𝑀 ... 𝑁 ) –1-1-onto→ ( 𝑀 ... 𝑁 ) ∧ 𝑔 : ( 𝑀 ... 𝑁 ) ⟶ 𝐶 ) → ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ 𝑁 ) = ( seq 𝑀 ( + , 𝑔 ) ‘ 𝑁 ) ) → ( ( 𝐹 : ( 𝑀 ... 𝑁 ) –1-1-onto→ ( 𝑀 ... 𝑁 ) ∧ ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝐺 ‘ 𝑥 ) ) : ( 𝑀 ... 𝑁 ) ⟶ 𝐶 ) → ( seq 𝑀 ( + , ( ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝐺 ‘ 𝑥 ) ) ∘ 𝐹 ) ) ‘ 𝑁 ) = ( seq 𝑀 ( + , ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝐺 ‘ 𝑥 ) ) ) ‘ 𝑁 ) ) ) )
139 119 124 138 sylancr ⊢ ( 𝜑 → ( ∀ 𝑔 ∀ 𝑓 ( ( 𝑓 : ( 𝑀 ... 𝑁 ) –1-1-onto→ ( 𝑀 ... 𝑁 ) ∧ 𝑔 : ( 𝑀 ... 𝑁 ) ⟶ 𝐶 ) → ( seq 𝑀 ( + , ( 𝑔 ∘ 𝑓 ) ) ‘ 𝑁 ) = ( seq 𝑀 ( + , 𝑔 ) ‘ 𝑁 ) ) → ( ( 𝐹 : ( 𝑀 ... 𝑁 ) –1-1-onto→ ( 𝑀 ... 𝑁 ) ∧ ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝐺 ‘ 𝑥 ) ) : ( 𝑀 ... 𝑁 ) ⟶ 𝐶 ) → ( seq 𝑀 ( + , ( ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝐺 ‘ 𝑥 ) ) ∘ 𝐹 ) ) ‘ 𝑁 ) = ( seq 𝑀 ( + , ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝐺 ‘ 𝑥 ) ) ) ‘ 𝑁 ) ) ) )
140 113 139 mpd ⊢ ( 𝜑 → ( ( 𝐹 : ( 𝑀 ... 𝑁 ) –1-1-onto→ ( 𝑀 ... 𝑁 ) ∧ ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝐺 ‘ 𝑥 ) ) : ( 𝑀 ... 𝑁 ) ⟶ 𝐶 ) → ( seq 𝑀 ( + , ( ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝐺 ‘ 𝑥 ) ) ∘ 𝐹 ) ) ‘ 𝑁 ) = ( seq 𝑀 ( + , ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝐺 ‘ 𝑥 ) ) ) ‘ 𝑁 ) ) )
141 6 9 140 mp2and ⊢ ( 𝜑 → ( seq 𝑀 ( + , ( ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝐺 ‘ 𝑥 ) ) ∘ 𝐹 ) ) ‘ 𝑁 ) = ( seq 𝑀 ( + , ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝐺 ‘ 𝑥 ) ) ) ‘ 𝑁 ) )
142 121 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑀 ... 𝑁 ) )
143 fveq2 ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑘 ) → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) )
144 fvex ⊢ ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ V
145 143 115 144 fvmpt ⊢ ( ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑀 ... 𝑁 ) → ( ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝐺 ‘ 𝑥 ) ) ‘ ( 𝐹 ‘ 𝑘 ) ) = ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) )
146 142 145 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝐺 ‘ 𝑥 ) ) ‘ ( 𝐹 ‘ 𝑘 ) ) = ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) )
147 fvco3 ⊢ ( ( 𝐹 : ( 𝑀 ... 𝑁 ) ⟶ ( 𝑀 ... 𝑁 ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝐺 ‘ 𝑥 ) ) ∘ 𝐹 ) ‘ 𝑘 ) = ( ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝐺 ‘ 𝑥 ) ) ‘ ( 𝐹 ‘ 𝑘 ) ) )
148 121 147 sylan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝐺 ‘ 𝑥 ) ) ∘ 𝐹 ) ‘ 𝑘 ) = ( ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝐺 ‘ 𝑥 ) ) ‘ ( 𝐹 ‘ 𝑘 ) ) )
149 146 148 8 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝐺 ‘ 𝑥 ) ) ∘ 𝐹 ) ‘ 𝑘 ) = ( 𝐻 ‘ 𝑘 ) )
150 4 149 seqfveq ⊢ ( 𝜑 → ( seq 𝑀 ( + , ( ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝐺 ‘ 𝑥 ) ) ∘ 𝐹 ) ) ‘ 𝑁 ) = ( seq 𝑀 ( + , 𝐻 ) ‘ 𝑁 ) )
151 fveq2 ⊢ ( 𝑥 = 𝑘 → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑘 ) )
152 fvex ⊢ ( 𝐺 ‘ 𝑘 ) ∈ V
153 151 115 152 fvmpt ⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) → ( ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝐺 ‘ 𝑥 ) ) ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) )
154 153 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝐺 ‘ 𝑥 ) ) ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) )
155 4 154 seqfveq ⊢ ( 𝜑 → ( seq 𝑀 ( + , ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝐺 ‘ 𝑥 ) ) ) ‘ 𝑁 ) = ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑁 ) )
156 141 150 155 3eqtr3d ⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐻 ) ‘ 𝑁 ) = ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑁 ) )