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

Metamath Proof Explorer

Theorem seq1st

Description: A sequence whose iteration function ignores the second argument is only affected by the first point of the initial value function. (Contributed by Mario Carneiro, 11-Feb-2015)

Ref Expression
Hypotheses algrf.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
algrf.2 ⊢ 𝑅 = seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) )
Assertion seq1st ( ( 𝑀 ∈ ℤ ∧ 𝐴 ∈ 𝑉 ) → 𝑅 = seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) )

Proof

Step Hyp Ref Expression
1 algrf.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 algrf.2 ⊢ 𝑅 = seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) )
3 seqfn ⊢ ( 𝑀 ∈ ℤ → seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) Fn ( ℤ≥ ‘ 𝑀 ) )
4 3 adantr ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐴 ∈ 𝑉 ) → seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) Fn ( ℤ≥ ‘ 𝑀 ) )
5 seqfn ⊢ ( 𝑀 ∈ ℤ → seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) Fn ( ℤ≥ ‘ 𝑀 ) )
6 5 adantr ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐴 ∈ 𝑉 ) → seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) Fn ( ℤ≥ ‘ 𝑀 ) )
7 fveq2 ⊢ ( 𝑦 = 𝑀 → ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ 𝑦 ) = ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ 𝑀 ) )
8 fveq2 ⊢ ( 𝑦 = 𝑀 → ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ 𝑦 ) = ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ 𝑀 ) )
9 7 8 eqeq12d ⊢ ( 𝑦 = 𝑀 → ( ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ 𝑦 ) = ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ 𝑦 ) ↔ ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ 𝑀 ) = ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ 𝑀 ) ) )
10 9 imbi2d ⊢ ( 𝑦 = 𝑀 → ( ( 𝐴 ∈ 𝑉 → ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ 𝑦 ) = ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ 𝑦 ) ) ↔ ( 𝐴 ∈ 𝑉 → ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ 𝑀 ) = ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ 𝑀 ) ) ) )
11 fveq2 ⊢ ( 𝑦 = 𝑥 → ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ 𝑦 ) = ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ 𝑥 ) )
12 fveq2 ⊢ ( 𝑦 = 𝑥 → ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ 𝑦 ) = ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ 𝑥 ) )
13 11 12 eqeq12d ⊢ ( 𝑦 = 𝑥 → ( ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ 𝑦 ) = ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ 𝑦 ) ↔ ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ 𝑥 ) = ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ 𝑥 ) ) )
14 13 imbi2d ⊢ ( 𝑦 = 𝑥 → ( ( 𝐴 ∈ 𝑉 → ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ 𝑦 ) = ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ 𝑦 ) ) ↔ ( 𝐴 ∈ 𝑉 → ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ 𝑥 ) = ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ 𝑥 ) ) ) )
15 fveq2 ⊢ ( 𝑦 = ( 𝑥 + 1 ) → ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ 𝑦 ) = ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ ( 𝑥 + 1 ) ) )
16 fveq2 ⊢ ( 𝑦 = ( 𝑥 + 1 ) → ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ 𝑦 ) = ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ ( 𝑥 + 1 ) ) )
17 15 16 eqeq12d ⊢ ( 𝑦 = ( 𝑥 + 1 ) → ( ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ 𝑦 ) = ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ 𝑦 ) ↔ ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ ( 𝑥 + 1 ) ) = ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ ( 𝑥 + 1 ) ) ) )
18 17 imbi2d ⊢ ( 𝑦 = ( 𝑥 + 1 ) → ( ( 𝐴 ∈ 𝑉 → ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ 𝑦 ) = ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ 𝑦 ) ) ↔ ( 𝐴 ∈ 𝑉 → ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ ( 𝑥 + 1 ) ) = ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ ( 𝑥 + 1 ) ) ) ) )
19 seq1 ⊢ ( 𝑀 ∈ ℤ → ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ 𝑀 ) = ( ( 𝑍 × { 𝐴 } ) ‘ 𝑀 ) )
20 19 adantr ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐴 ∈ 𝑉 ) → ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ 𝑀 ) = ( ( 𝑍 × { 𝐴 } ) ‘ 𝑀 ) )
21 seq1 ⊢ ( 𝑀 ∈ ℤ → ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ 𝑀 ) = ( { ⟨ 𝑀 , 𝐴 ⟩ } ‘ 𝑀 ) )
22 21 adantr ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐴 ∈ 𝑉 ) → ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ 𝑀 ) = ( { ⟨ 𝑀 , 𝐴 ⟩ } ‘ 𝑀 ) )
23 id ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ 𝑉 )
24 uzid ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) )
25 24 1 eleqtrrdi ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ 𝑍 )
26 fvconst2g ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑀 ∈ 𝑍 ) → ( ( 𝑍 × { 𝐴 } ) ‘ 𝑀 ) = 𝐴 )
27 23 25 26 syl2anr ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐴 ∈ 𝑉 ) → ( ( 𝑍 × { 𝐴 } ) ‘ 𝑀 ) = 𝐴 )
28 fvsng ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐴 ∈ 𝑉 ) → ( { ⟨ 𝑀 , 𝐴 ⟩ } ‘ 𝑀 ) = 𝐴 )
29 27 28 eqtr4d ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐴 ∈ 𝑉 ) → ( ( 𝑍 × { 𝐴 } ) ‘ 𝑀 ) = ( { ⟨ 𝑀 , 𝐴 ⟩ } ‘ 𝑀 ) )
30 22 29 eqtr4d ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐴 ∈ 𝑉 ) → ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ 𝑀 ) = ( ( 𝑍 × { 𝐴 } ) ‘ 𝑀 ) )
31 20 30 eqtr4d ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐴 ∈ 𝑉 ) → ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ 𝑀 ) = ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ 𝑀 ) )
32 31 ex ⊢ ( 𝑀 ∈ ℤ → ( 𝐴 ∈ 𝑉 → ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ 𝑀 ) = ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ 𝑀 ) ) )
33 fveq2 ⊢ ( ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ 𝑥 ) = ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ 𝑥 ) → ( 𝐹 ‘ ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ 𝑥 ) ) = ( 𝐹 ‘ ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ 𝑥 ) ) )
34 seqp1 ⊢ ( 𝑥 ∈ ( ℤ≥ ‘ 𝑀 ) → ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ ( 𝑥 + 1 ) ) = ( ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ 𝑥 ) ( 𝐹 ∘ 1st ) ( ( 𝑍 × { 𝐴 } ) ‘ ( 𝑥 + 1 ) ) ) )
35 fvex ⊢ ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ 𝑥 ) ∈ V
36 fvex ⊢ ( ( 𝑍 × { 𝐴 } ) ‘ ( 𝑥 + 1 ) ) ∈ V
37 35 36 opco1i ⊢ ( ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ 𝑥 ) ( 𝐹 ∘ 1st ) ( ( 𝑍 × { 𝐴 } ) ‘ ( 𝑥 + 1 ) ) ) = ( 𝐹 ‘ ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ 𝑥 ) )
38 34 37 eqtrdi ⊢ ( 𝑥 ∈ ( ℤ≥ ‘ 𝑀 ) → ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ ( 𝑥 + 1 ) ) = ( 𝐹 ‘ ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ 𝑥 ) ) )
39 seqp1 ⊢ ( 𝑥 ∈ ( ℤ≥ ‘ 𝑀 ) → ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ ( 𝑥 + 1 ) ) = ( ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ 𝑥 ) ( 𝐹 ∘ 1st ) ( { ⟨ 𝑀 , 𝐴 ⟩ } ‘ ( 𝑥 + 1 ) ) ) )
40 fvex ⊢ ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ 𝑥 ) ∈ V
41 fvex ⊢ ( { ⟨ 𝑀 , 𝐴 ⟩ } ‘ ( 𝑥 + 1 ) ) ∈ V
42 40 41 opco1i ⊢ ( ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ 𝑥 ) ( 𝐹 ∘ 1st ) ( { ⟨ 𝑀 , 𝐴 ⟩ } ‘ ( 𝑥 + 1 ) ) ) = ( 𝐹 ‘ ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ 𝑥 ) )
43 39 42 eqtrdi ⊢ ( 𝑥 ∈ ( ℤ≥ ‘ 𝑀 ) → ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ ( 𝑥 + 1 ) ) = ( 𝐹 ‘ ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ 𝑥 ) ) )
44 38 43 eqeq12d ⊢ ( 𝑥 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ ( 𝑥 + 1 ) ) = ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ ( 𝑥 + 1 ) ) ↔ ( 𝐹 ‘ ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ 𝑥 ) ) = ( 𝐹 ‘ ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ 𝑥 ) ) ) )
45 44 adantl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ ( 𝑥 + 1 ) ) = ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ ( 𝑥 + 1 ) ) ↔ ( 𝐹 ‘ ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ 𝑥 ) ) = ( 𝐹 ‘ ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ 𝑥 ) ) ) )
46 33 45 imbitrrid ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ 𝑥 ) = ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ 𝑥 ) → ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ ( 𝑥 + 1 ) ) = ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ ( 𝑥 + 1 ) ) ) )
47 46 expcom ⊢ ( 𝑥 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝐴 ∈ 𝑉 → ( ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ 𝑥 ) = ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ 𝑥 ) → ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ ( 𝑥 + 1 ) ) = ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ ( 𝑥 + 1 ) ) ) ) )
48 47 a2d ⊢ ( 𝑥 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝐴 ∈ 𝑉 → ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ 𝑥 ) = ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ 𝑥 ) ) → ( 𝐴 ∈ 𝑉 → ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ ( 𝑥 + 1 ) ) = ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ ( 𝑥 + 1 ) ) ) ) )
49 10 14 18 14 32 48 uzind4 ⊢ ( 𝑥 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝐴 ∈ 𝑉 → ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ 𝑥 ) = ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ 𝑥 ) ) )
50 49 impcom ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ 𝑥 ) = ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ 𝑥 ) )
51 50 adantll ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) ‘ 𝑥 ) = ( seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) ‘ 𝑥 ) )
52 4 6 51 eqfnfvd ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐴 ∈ 𝑉 ) → seq 𝑀 ( ( 𝐹 ∘ 1st ) , ( 𝑍 × { 𝐴 } ) ) = seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) )
53 2 52 eqtrid ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐴 ∈ 𝑉 ) → 𝑅 = seq 𝑀 ( ( 𝐹 ∘ 1st ) , { ⟨ 𝑀 , 𝐴 ⟩ } ) )