Metamath Proof Explorer

Theorem seqomlem1

Description: Lemma for seqom . The underlying recursion generates a sequence of pairs with the expected first values. (Contributed by Stefan O'Rear, 1-Nov-2014) (Revised by Mario Carneiro, 23-Jun-2015)

Ref Expression
Hypothesis seqomlem.a ⊢ 𝑄 = rec ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) , ⟨ ∅ , ( I ‘ 𝐼 ) ⟩ )
Assertion seqomlem1 ( 𝐴 ∈ ω → ( 𝑄 ‘ 𝐴 ) = ⟨ 𝐴 , ( 2nd ‘ ( 𝑄 ‘ 𝐴 ) ) ⟩ )

Proof

Step Hyp Ref Expression
1 seqomlem.a ⊢ 𝑄 = rec ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) , ⟨ ∅ , ( I ‘ 𝐼 ) ⟩ )
2 fveq2 ⊢ ( 𝑎 = ∅ → ( 𝑄 ‘ 𝑎 ) = ( 𝑄 ‘ ∅ ) )
3 id ⊢ ( 𝑎 = ∅ → 𝑎 = ∅ )
4 2fveq3 ⊢ ( 𝑎 = ∅ → ( 2nd ‘ ( 𝑄 ‘ 𝑎 ) ) = ( 2nd ‘ ( 𝑄 ‘ ∅ ) ) )
5 3 4 opeq12d ⊢ ( 𝑎 = ∅ → ⟨ 𝑎 , ( 2nd ‘ ( 𝑄 ‘ 𝑎 ) ) ⟩ = ⟨ ∅ , ( 2nd ‘ ( 𝑄 ‘ ∅ ) ) ⟩ )
6 2 5 eqeq12d ⊢ ( 𝑎 = ∅ → ( ( 𝑄 ‘ 𝑎 ) = ⟨ 𝑎 , ( 2nd ‘ ( 𝑄 ‘ 𝑎 ) ) ⟩ ↔ ( 𝑄 ‘ ∅ ) = ⟨ ∅ , ( 2nd ‘ ( 𝑄 ‘ ∅ ) ) ⟩ ) )
7 fveq2 ⊢ ( 𝑎 = 𝑏 → ( 𝑄 ‘ 𝑎 ) = ( 𝑄 ‘ 𝑏 ) )
8 id ⊢ ( 𝑎 = 𝑏 → 𝑎 = 𝑏 )
9 2fveq3 ⊢ ( 𝑎 = 𝑏 → ( 2nd ‘ ( 𝑄 ‘ 𝑎 ) ) = ( 2nd ‘ ( 𝑄 ‘ 𝑏 ) ) )
10 8 9 opeq12d ⊢ ( 𝑎 = 𝑏 → ⟨ 𝑎 , ( 2nd ‘ ( 𝑄 ‘ 𝑎 ) ) ⟩ = ⟨ 𝑏 , ( 2nd ‘ ( 𝑄 ‘ 𝑏 ) ) ⟩ )
11 7 10 eqeq12d ⊢ ( 𝑎 = 𝑏 → ( ( 𝑄 ‘ 𝑎 ) = ⟨ 𝑎 , ( 2nd ‘ ( 𝑄 ‘ 𝑎 ) ) ⟩ ↔ ( 𝑄 ‘ 𝑏 ) = ⟨ 𝑏 , ( 2nd ‘ ( 𝑄 ‘ 𝑏 ) ) ⟩ ) )
12 fveq2 ⊢ ( 𝑎 = suc 𝑏 → ( 𝑄 ‘ 𝑎 ) = ( 𝑄 ‘ suc 𝑏 ) )
13 id ⊢ ( 𝑎 = suc 𝑏 → 𝑎 = suc 𝑏 )
14 2fveq3 ⊢ ( 𝑎 = suc 𝑏 → ( 2nd ‘ ( 𝑄 ‘ 𝑎 ) ) = ( 2nd ‘ ( 𝑄 ‘ suc 𝑏 ) ) )
15 13 14 opeq12d ⊢ ( 𝑎 = suc 𝑏 → ⟨ 𝑎 , ( 2nd ‘ ( 𝑄 ‘ 𝑎 ) ) ⟩ = ⟨ suc 𝑏 , ( 2nd ‘ ( 𝑄 ‘ suc 𝑏 ) ) ⟩ )
16 12 15 eqeq12d ⊢ ( 𝑎 = suc 𝑏 → ( ( 𝑄 ‘ 𝑎 ) = ⟨ 𝑎 , ( 2nd ‘ ( 𝑄 ‘ 𝑎 ) ) ⟩ ↔ ( 𝑄 ‘ suc 𝑏 ) = ⟨ suc 𝑏 , ( 2nd ‘ ( 𝑄 ‘ suc 𝑏 ) ) ⟩ ) )
17 fveq2 ⊢ ( 𝑎 = 𝐴 → ( 𝑄 ‘ 𝑎 ) = ( 𝑄 ‘ 𝐴 ) )
18 id ⊢ ( 𝑎 = 𝐴 → 𝑎 = 𝐴 )
19 2fveq3 ⊢ ( 𝑎 = 𝐴 → ( 2nd ‘ ( 𝑄 ‘ 𝑎 ) ) = ( 2nd ‘ ( 𝑄 ‘ 𝐴 ) ) )
20 18 19 opeq12d ⊢ ( 𝑎 = 𝐴 → ⟨ 𝑎 , ( 2nd ‘ ( 𝑄 ‘ 𝑎 ) ) ⟩ = ⟨ 𝐴 , ( 2nd ‘ ( 𝑄 ‘ 𝐴 ) ) ⟩ )
21 17 20 eqeq12d ⊢ ( 𝑎 = 𝐴 → ( ( 𝑄 ‘ 𝑎 ) = ⟨ 𝑎 , ( 2nd ‘ ( 𝑄 ‘ 𝑎 ) ) ⟩ ↔ ( 𝑄 ‘ 𝐴 ) = ⟨ 𝐴 , ( 2nd ‘ ( 𝑄 ‘ 𝐴 ) ) ⟩ ) )
22 1 fveq1i ⊢ ( 𝑄 ‘ ∅ ) = ( rec ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) , ⟨ ∅ , ( I ‘ 𝐼 ) ⟩ ) ‘ ∅ )
23 opex ⊢ ⟨ ∅ , ( I ‘ 𝐼 ) ⟩ ∈ V
24 23 rdg0 ⊢ ( rec ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) , ⟨ ∅ , ( I ‘ 𝐼 ) ⟩ ) ‘ ∅ ) = ⟨ ∅ , ( I ‘ 𝐼 ) ⟩
25 22 24 eqtri ⊢ ( 𝑄 ‘ ∅ ) = ⟨ ∅ , ( I ‘ 𝐼 ) ⟩
26 0ex ⊢ ∅ ∈ V
27 fvex ⊢ ( I ‘ 𝐼 ) ∈ V
28 26 27 op2nd ⊢ ( 2nd ‘ ⟨ ∅ , ( I ‘ 𝐼 ) ⟩ ) = ( I ‘ 𝐼 )
29 28 eqcomi ⊢ ( I ‘ 𝐼 ) = ( 2nd ‘ ⟨ ∅ , ( I ‘ 𝐼 ) ⟩ )
30 29 opeq2i ⊢ ⟨ ∅ , ( I ‘ 𝐼 ) ⟩ = ⟨ ∅ , ( 2nd ‘ ⟨ ∅ , ( I ‘ 𝐼 ) ⟩ ) ⟩
31 id ⊢ ( ( 𝑄 ‘ ∅ ) = ⟨ ∅ , ( I ‘ 𝐼 ) ⟩ → ( 𝑄 ‘ ∅ ) = ⟨ ∅ , ( I ‘ 𝐼 ) ⟩ )
32 fveq2 ⊢ ( ( 𝑄 ‘ ∅ ) = ⟨ ∅ , ( I ‘ 𝐼 ) ⟩ → ( 2nd ‘ ( 𝑄 ‘ ∅ ) ) = ( 2nd ‘ ⟨ ∅ , ( I ‘ 𝐼 ) ⟩ ) )
33 32 opeq2d ⊢ ( ( 𝑄 ‘ ∅ ) = ⟨ ∅ , ( I ‘ 𝐼 ) ⟩ → ⟨ ∅ , ( 2nd ‘ ( 𝑄 ‘ ∅ ) ) ⟩ = ⟨ ∅ , ( 2nd ‘ ⟨ ∅ , ( I ‘ 𝐼 ) ⟩ ) ⟩ )
34 30 31 33 3eqtr4a ⊢ ( ( 𝑄 ‘ ∅ ) = ⟨ ∅ , ( I ‘ 𝐼 ) ⟩ → ( 𝑄 ‘ ∅ ) = ⟨ ∅ , ( 2nd ‘ ( 𝑄 ‘ ∅ ) ) ⟩ )
35 25 34 ax-mp ⊢ ( 𝑄 ‘ ∅ ) = ⟨ ∅ , ( 2nd ‘ ( 𝑄 ‘ ∅ ) ) ⟩
36 df-ov ⊢ ( 𝑏 ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) ( 2nd ‘ ( 𝑄 ‘ 𝑏 ) ) ) = ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) ‘ ⟨ 𝑏 , ( 2nd ‘ ( 𝑄 ‘ 𝑏 ) ) ⟩ )
37 fvex ⊢ ( 2nd ‘ ( 𝑄 ‘ 𝑏 ) ) ∈ V
38 suceq ⊢ ( 𝑖 = 𝑏 → suc 𝑖 = suc 𝑏 )
39 oveq1 ⊢ ( 𝑖 = 𝑏 → ( 𝑖 𝐹 𝑣 ) = ( 𝑏 𝐹 𝑣 ) )
40 38 39 opeq12d ⊢ ( 𝑖 = 𝑏 → ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ = ⟨ suc 𝑏 , ( 𝑏 𝐹 𝑣 ) ⟩ )
41 oveq2 ⊢ ( 𝑣 = ( 2nd ‘ ( 𝑄 ‘ 𝑏 ) ) → ( 𝑏 𝐹 𝑣 ) = ( 𝑏 𝐹 ( 2nd ‘ ( 𝑄 ‘ 𝑏 ) ) ) )
42 41 opeq2d ⊢ ( 𝑣 = ( 2nd ‘ ( 𝑄 ‘ 𝑏 ) ) → ⟨ suc 𝑏 , ( 𝑏 𝐹 𝑣 ) ⟩ = ⟨ suc 𝑏 , ( 𝑏 𝐹 ( 2nd ‘ ( 𝑄 ‘ 𝑏 ) ) ) ⟩ )
43 eqid ⊢ ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) = ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ )
44 opex ⊢ ⟨ suc 𝑏 , ( 𝑏 𝐹 ( 2nd ‘ ( 𝑄 ‘ 𝑏 ) ) ) ⟩ ∈ V
45 40 42 43 44 ovmpo ⊢ ( ( 𝑏 ∈ ω ∧ ( 2nd ‘ ( 𝑄 ‘ 𝑏 ) ) ∈ V ) → ( 𝑏 ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) ( 2nd ‘ ( 𝑄 ‘ 𝑏 ) ) ) = ⟨ suc 𝑏 , ( 𝑏 𝐹 ( 2nd ‘ ( 𝑄 ‘ 𝑏 ) ) ) ⟩ )
46 37 45 mpan2 ⊢ ( 𝑏 ∈ ω → ( 𝑏 ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) ( 2nd ‘ ( 𝑄 ‘ 𝑏 ) ) ) = ⟨ suc 𝑏 , ( 𝑏 𝐹 ( 2nd ‘ ( 𝑄 ‘ 𝑏 ) ) ) ⟩ )
47 36 46 eqtr3id ⊢ ( 𝑏 ∈ ω → ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) ‘ ⟨ 𝑏 , ( 2nd ‘ ( 𝑄 ‘ 𝑏 ) ) ⟩ ) = ⟨ suc 𝑏 , ( 𝑏 𝐹 ( 2nd ‘ ( 𝑄 ‘ 𝑏 ) ) ) ⟩ )
48 fveqeq2 ⊢ ( ( 𝑄 ‘ 𝑏 ) = ⟨ 𝑏 , ( 2nd ‘ ( 𝑄 ‘ 𝑏 ) ) ⟩ → ( ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) ‘ ( 𝑄 ‘ 𝑏 ) ) = ⟨ suc 𝑏 , ( 𝑏 𝐹 ( 2nd ‘ ( 𝑄 ‘ 𝑏 ) ) ) ⟩ ↔ ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) ‘ ⟨ 𝑏 , ( 2nd ‘ ( 𝑄 ‘ 𝑏 ) ) ⟩ ) = ⟨ suc 𝑏 , ( 𝑏 𝐹 ( 2nd ‘ ( 𝑄 ‘ 𝑏 ) ) ) ⟩ ) )
49 47 48 syl5ibrcom ⊢ ( 𝑏 ∈ ω → ( ( 𝑄 ‘ 𝑏 ) = ⟨ 𝑏 , ( 2nd ‘ ( 𝑄 ‘ 𝑏 ) ) ⟩ → ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) ‘ ( 𝑄 ‘ 𝑏 ) ) = ⟨ suc 𝑏 , ( 𝑏 𝐹 ( 2nd ‘ ( 𝑄 ‘ 𝑏 ) ) ) ⟩ ) )
50 vex ⊢ 𝑏 ∈ V
51 50 sucex ⊢ suc 𝑏 ∈ V
52 ovex ⊢ ( 𝑏 𝐹 ( 2nd ‘ ( 𝑄 ‘ 𝑏 ) ) ) ∈ V
53 51 52 op2nd ⊢ ( 2nd ‘ ⟨ suc 𝑏 , ( 𝑏 𝐹 ( 2nd ‘ ( 𝑄 ‘ 𝑏 ) ) ) ⟩ ) = ( 𝑏 𝐹 ( 2nd ‘ ( 𝑄 ‘ 𝑏 ) ) )
54 53 eqcomi ⊢ ( 𝑏 𝐹 ( 2nd ‘ ( 𝑄 ‘ 𝑏 ) ) ) = ( 2nd ‘ ⟨ suc 𝑏 , ( 𝑏 𝐹 ( 2nd ‘ ( 𝑄 ‘ 𝑏 ) ) ) ⟩ )
55 54 a1i ⊢ ( 𝑏 ∈ ω → ( 𝑏 𝐹 ( 2nd ‘ ( 𝑄 ‘ 𝑏 ) ) ) = ( 2nd ‘ ⟨ suc 𝑏 , ( 𝑏 𝐹 ( 2nd ‘ ( 𝑄 ‘ 𝑏 ) ) ) ⟩ ) )
56 55 opeq2d ⊢ ( 𝑏 ∈ ω → ⟨ suc 𝑏 , ( 𝑏 𝐹 ( 2nd ‘ ( 𝑄 ‘ 𝑏 ) ) ) ⟩ = ⟨ suc 𝑏 , ( 2nd ‘ ⟨ suc 𝑏 , ( 𝑏 𝐹 ( 2nd ‘ ( 𝑄 ‘ 𝑏 ) ) ) ⟩ ) ⟩ )
57 id ⊢ ( ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) ‘ ( 𝑄 ‘ 𝑏 ) ) = ⟨ suc 𝑏 , ( 𝑏 𝐹 ( 2nd ‘ ( 𝑄 ‘ 𝑏 ) ) ) ⟩ → ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) ‘ ( 𝑄 ‘ 𝑏 ) ) = ⟨ suc 𝑏 , ( 𝑏 𝐹 ( 2nd ‘ ( 𝑄 ‘ 𝑏 ) ) ) ⟩ )
58 fveq2 ⊢ ( ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) ‘ ( 𝑄 ‘ 𝑏 ) ) = ⟨ suc 𝑏 , ( 𝑏 𝐹 ( 2nd ‘ ( 𝑄 ‘ 𝑏 ) ) ) ⟩ → ( 2nd ‘ ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) ‘ ( 𝑄 ‘ 𝑏 ) ) ) = ( 2nd ‘ ⟨ suc 𝑏 , ( 𝑏 𝐹 ( 2nd ‘ ( 𝑄 ‘ 𝑏 ) ) ) ⟩ ) )
59 58 opeq2d ⊢ ( ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) ‘ ( 𝑄 ‘ 𝑏 ) ) = ⟨ suc 𝑏 , ( 𝑏 𝐹 ( 2nd ‘ ( 𝑄 ‘ 𝑏 ) ) ) ⟩ → ⟨ suc 𝑏 , ( 2nd ‘ ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) ‘ ( 𝑄 ‘ 𝑏 ) ) ) ⟩ = ⟨ suc 𝑏 , ( 2nd ‘ ⟨ suc 𝑏 , ( 𝑏 𝐹 ( 2nd ‘ ( 𝑄 ‘ 𝑏 ) ) ) ⟩ ) ⟩ )
60 57 59 eqeq12d ⊢ ( ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) ‘ ( 𝑄 ‘ 𝑏 ) ) = ⟨ suc 𝑏 , ( 𝑏 𝐹 ( 2nd ‘ ( 𝑄 ‘ 𝑏 ) ) ) ⟩ → ( ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) ‘ ( 𝑄 ‘ 𝑏 ) ) = ⟨ suc 𝑏 , ( 2nd ‘ ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) ‘ ( 𝑄 ‘ 𝑏 ) ) ) ⟩ ↔ ⟨ suc 𝑏 , ( 𝑏 𝐹 ( 2nd ‘ ( 𝑄 ‘ 𝑏 ) ) ) ⟩ = ⟨ suc 𝑏 , ( 2nd ‘ ⟨ suc 𝑏 , ( 𝑏 𝐹 ( 2nd ‘ ( 𝑄 ‘ 𝑏 ) ) ) ⟩ ) ⟩ ) )
61 56 60 syl5ibrcom ⊢ ( 𝑏 ∈ ω → ( ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) ‘ ( 𝑄 ‘ 𝑏 ) ) = ⟨ suc 𝑏 , ( 𝑏 𝐹 ( 2nd ‘ ( 𝑄 ‘ 𝑏 ) ) ) ⟩ → ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) ‘ ( 𝑄 ‘ 𝑏 ) ) = ⟨ suc 𝑏 , ( 2nd ‘ ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) ‘ ( 𝑄 ‘ 𝑏 ) ) ) ⟩ ) )
62 49 61 syld ⊢ ( 𝑏 ∈ ω → ( ( 𝑄 ‘ 𝑏 ) = ⟨ 𝑏 , ( 2nd ‘ ( 𝑄 ‘ 𝑏 ) ) ⟩ → ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) ‘ ( 𝑄 ‘ 𝑏 ) ) = ⟨ suc 𝑏 , ( 2nd ‘ ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) ‘ ( 𝑄 ‘ 𝑏 ) ) ) ⟩ ) )
63 frsuc ⊢ ( 𝑏 ∈ ω → ( ( rec ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) , ⟨ ∅ , ( I ‘ 𝐼 ) ⟩ ) ↾ ω ) ‘ suc 𝑏 ) = ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) ‘ ( ( rec ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) , ⟨ ∅ , ( I ‘ 𝐼 ) ⟩ ) ↾ ω ) ‘ 𝑏 ) ) )
64 peano2 ⊢ ( 𝑏 ∈ ω → suc 𝑏 ∈ ω )
65 64 fvresd ⊢ ( 𝑏 ∈ ω → ( ( rec ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) , ⟨ ∅ , ( I ‘ 𝐼 ) ⟩ ) ↾ ω ) ‘ suc 𝑏 ) = ( rec ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) , ⟨ ∅ , ( I ‘ 𝐼 ) ⟩ ) ‘ suc 𝑏 ) )
66 1 fveq1i ⊢ ( 𝑄 ‘ suc 𝑏 ) = ( rec ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) , ⟨ ∅ , ( I ‘ 𝐼 ) ⟩ ) ‘ suc 𝑏 )
67 65 66 eqtr4di ⊢ ( 𝑏 ∈ ω → ( ( rec ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) , ⟨ ∅ , ( I ‘ 𝐼 ) ⟩ ) ↾ ω ) ‘ suc 𝑏 ) = ( 𝑄 ‘ suc 𝑏 ) )
68 fvres ⊢ ( 𝑏 ∈ ω → ( ( rec ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) , ⟨ ∅ , ( I ‘ 𝐼 ) ⟩ ) ↾ ω ) ‘ 𝑏 ) = ( rec ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) , ⟨ ∅ , ( I ‘ 𝐼 ) ⟩ ) ‘ 𝑏 ) )
69 1 fveq1i ⊢ ( 𝑄 ‘ 𝑏 ) = ( rec ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) , ⟨ ∅ , ( I ‘ 𝐼 ) ⟩ ) ‘ 𝑏 )
70 68 69 eqtr4di ⊢ ( 𝑏 ∈ ω → ( ( rec ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) , ⟨ ∅ , ( I ‘ 𝐼 ) ⟩ ) ↾ ω ) ‘ 𝑏 ) = ( 𝑄 ‘ 𝑏 ) )
71 70 fveq2d ⊢ ( 𝑏 ∈ ω → ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) ‘ ( ( rec ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) , ⟨ ∅ , ( I ‘ 𝐼 ) ⟩ ) ↾ ω ) ‘ 𝑏 ) ) = ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) ‘ ( 𝑄 ‘ 𝑏 ) ) )
72 63 67 71 3eqtr3d ⊢ ( 𝑏 ∈ ω → ( 𝑄 ‘ suc 𝑏 ) = ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) ‘ ( 𝑄 ‘ 𝑏 ) ) )
73 72 fveq2d ⊢ ( 𝑏 ∈ ω → ( 2nd ‘ ( 𝑄 ‘ suc 𝑏 ) ) = ( 2nd ‘ ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) ‘ ( 𝑄 ‘ 𝑏 ) ) ) )
74 73 opeq2d ⊢ ( 𝑏 ∈ ω → ⟨ suc 𝑏 , ( 2nd ‘ ( 𝑄 ‘ suc 𝑏 ) ) ⟩ = ⟨ suc 𝑏 , ( 2nd ‘ ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) ‘ ( 𝑄 ‘ 𝑏 ) ) ) ⟩ )
75 72 74 eqeq12d ⊢ ( 𝑏 ∈ ω → ( ( 𝑄 ‘ suc 𝑏 ) = ⟨ suc 𝑏 , ( 2nd ‘ ( 𝑄 ‘ suc 𝑏 ) ) ⟩ ↔ ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) ‘ ( 𝑄 ‘ 𝑏 ) ) = ⟨ suc 𝑏 , ( 2nd ‘ ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) ‘ ( 𝑄 ‘ 𝑏 ) ) ) ⟩ ) )
76 62 75 sylibrd ⊢ ( 𝑏 ∈ ω → ( ( 𝑄 ‘ 𝑏 ) = ⟨ 𝑏 , ( 2nd ‘ ( 𝑄 ‘ 𝑏 ) ) ⟩ → ( 𝑄 ‘ suc 𝑏 ) = ⟨ suc 𝑏 , ( 2nd ‘ ( 𝑄 ‘ suc 𝑏 ) ) ⟩ ) )
77 6 11 16 21 35 76 finds ⊢ ( 𝐴 ∈ ω → ( 𝑄 ‘ 𝐴 ) = ⟨ 𝐴 , ( 2nd ‘ ( 𝑄 ‘ 𝐴 ) ) ⟩ )