Metamath Proof Explorer

Theorem seqomlem4

Description: Lemma for seqom . (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 seqomlem4 ( 𝐴 ∈ ω → ( ( 𝑄 “ ω ) ‘ suc 𝐴 ) = ( 𝐴 𝐹 ( ( 𝑄 “ ω ) ‘ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 seqomlem.a ⊢ 𝑄 = rec ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) , ⟨ ∅ , ( I ‘ 𝐼 ) ⟩ )
2 peano2 ⊢ ( 𝐴 ∈ ω → suc 𝐴 ∈ ω )
3 2 fvresd ⊢ ( 𝐴 ∈ ω → ( ( 𝑄 ↾ ω ) ‘ suc 𝐴 ) = ( 𝑄 ‘ suc 𝐴 ) )
4 frsuc ⊢ ( 𝐴 ∈ ω → ( ( rec ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) , ⟨ ∅ , ( I ‘ 𝐼 ) ⟩ ) ↾ ω ) ‘ suc 𝐴 ) = ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) ‘ ( ( rec ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) , ⟨ ∅ , ( I ‘ 𝐼 ) ⟩ ) ↾ ω ) ‘ 𝐴 ) ) )
5 2 fvresd ⊢ ( 𝐴 ∈ ω → ( ( rec ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) , ⟨ ∅ , ( I ‘ 𝐼 ) ⟩ ) ↾ ω ) ‘ suc 𝐴 ) = ( rec ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) , ⟨ ∅ , ( I ‘ 𝐼 ) ⟩ ) ‘ suc 𝐴 ) )
6 1 fveq1i ⊢ ( 𝑄 ‘ suc 𝐴 ) = ( rec ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) , ⟨ ∅ , ( I ‘ 𝐼 ) ⟩ ) ‘ suc 𝐴 )
7 5 6 syl6eqr ⊢ ( 𝐴 ∈ ω → ( ( rec ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) , ⟨ ∅ , ( I ‘ 𝐼 ) ⟩ ) ↾ ω ) ‘ suc 𝐴 ) = ( 𝑄 ‘ suc 𝐴 ) )
8 fvres ⊢ ( 𝐴 ∈ ω → ( ( rec ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) , ⟨ ∅ , ( I ‘ 𝐼 ) ⟩ ) ↾ ω ) ‘ 𝐴 ) = ( rec ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) , ⟨ ∅ , ( I ‘ 𝐼 ) ⟩ ) ‘ 𝐴 ) )
9 1 fveq1i ⊢ ( 𝑄 ‘ 𝐴 ) = ( rec ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) , ⟨ ∅ , ( I ‘ 𝐼 ) ⟩ ) ‘ 𝐴 )
10 8 9 syl6eqr ⊢ ( 𝐴 ∈ ω → ( ( rec ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) , ⟨ ∅ , ( I ‘ 𝐼 ) ⟩ ) ↾ ω ) ‘ 𝐴 ) = ( 𝑄 ‘ 𝐴 ) )
11 10 fveq2d ⊢ ( 𝐴 ∈ ω → ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) ‘ ( ( rec ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) , ⟨ ∅ , ( I ‘ 𝐼 ) ⟩ ) ↾ ω ) ‘ 𝐴 ) ) = ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) ‘ ( 𝑄 ‘ 𝐴 ) ) )
12 4 7 11 3eqtr3d ⊢ ( 𝐴 ∈ ω → ( 𝑄 ‘ suc 𝐴 ) = ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) ‘ ( 𝑄 ‘ 𝐴 ) ) )
13 1 seqomlem1 ⊢ ( 𝐴 ∈ ω → ( 𝑄 ‘ 𝐴 ) = ⟨ 𝐴 , ( 2nd ‘ ( 𝑄 ‘ 𝐴 ) ) ⟩ )
14 13 fveq2d ⊢ ( 𝐴 ∈ ω → ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) ‘ ( 𝑄 ‘ 𝐴 ) ) = ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) ‘ ⟨ 𝐴 , ( 2nd ‘ ( 𝑄 ‘ 𝐴 ) ) ⟩ ) )
15 df-ov ⊢ ( 𝐴 ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) ( 2nd ‘ ( 𝑄 ‘ 𝐴 ) ) ) = ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) ‘ ⟨ 𝐴 , ( 2nd ‘ ( 𝑄 ‘ 𝐴 ) ) ⟩ )
16 fvex ⊢ ( 2nd ‘ ( 𝑄 ‘ 𝐴 ) ) ∈ V
17 suceq ⊢ ( 𝑖 = 𝐴 → suc 𝑖 = suc 𝐴 )
18 oveq1 ⊢ ( 𝑖 = 𝐴 → ( 𝑖 𝐹 𝑣 ) = ( 𝐴 𝐹 𝑣 ) )
19 17 18 opeq12d ⊢ ( 𝑖 = 𝐴 → ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ = ⟨ suc 𝐴 , ( 𝐴 𝐹 𝑣 ) ⟩ )
20 oveq2 ⊢ ( 𝑣 = ( 2nd ‘ ( 𝑄 ‘ 𝐴 ) ) → ( 𝐴 𝐹 𝑣 ) = ( 𝐴 𝐹 ( 2nd ‘ ( 𝑄 ‘ 𝐴 ) ) ) )
21 20 opeq2d ⊢ ( 𝑣 = ( 2nd ‘ ( 𝑄 ‘ 𝐴 ) ) → ⟨ suc 𝐴 , ( 𝐴 𝐹 𝑣 ) ⟩ = ⟨ suc 𝐴 , ( 𝐴 𝐹 ( 2nd ‘ ( 𝑄 ‘ 𝐴 ) ) ) ⟩ )
22 eqid ⊢ ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) = ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ )
23 opex ⊢ ⟨ suc 𝐴 , ( 𝐴 𝐹 ( 2nd ‘ ( 𝑄 ‘ 𝐴 ) ) ) ⟩ ∈ V
24 19 21 22 23 ovmpo ⊢ ( ( 𝐴 ∈ ω ∧ ( 2nd ‘ ( 𝑄 ‘ 𝐴 ) ) ∈ V ) → ( 𝐴 ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) ( 2nd ‘ ( 𝑄 ‘ 𝐴 ) ) ) = ⟨ suc 𝐴 , ( 𝐴 𝐹 ( 2nd ‘ ( 𝑄 ‘ 𝐴 ) ) ) ⟩ )
25 16 24 mpan2 ⊢ ( 𝐴 ∈ ω → ( 𝐴 ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) ( 2nd ‘ ( 𝑄 ‘ 𝐴 ) ) ) = ⟨ suc 𝐴 , ( 𝐴 𝐹 ( 2nd ‘ ( 𝑄 ‘ 𝐴 ) ) ) ⟩ )
26 fvres ⊢ ( 𝐴 ∈ ω → ( ( 𝑄 ↾ ω ) ‘ 𝐴 ) = ( 𝑄 ‘ 𝐴 ) )
27 26 13 eqtrd ⊢ ( 𝐴 ∈ ω → ( ( 𝑄 ↾ ω ) ‘ 𝐴 ) = ⟨ 𝐴 , ( 2nd ‘ ( 𝑄 ‘ 𝐴 ) ) ⟩ )
28 frfnom ⊢ ( rec ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) , ⟨ ∅ , ( I ‘ 𝐼 ) ⟩ ) ↾ ω ) Fn ω
29 1 reseq1i ⊢ ( 𝑄 ↾ ω ) = ( rec ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) , ⟨ ∅ , ( I ‘ 𝐼 ) ⟩ ) ↾ ω )
30 29 fneq1i ⊢ ( ( 𝑄 ↾ ω ) Fn ω ↔ ( rec ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) , ⟨ ∅ , ( I ‘ 𝐼 ) ⟩ ) ↾ ω ) Fn ω )
31 28 30 mpbir ⊢ ( 𝑄 ↾ ω ) Fn ω
32 fnfvelrn ⊢ ( ( ( 𝑄 ↾ ω ) Fn ω ∧ 𝐴 ∈ ω ) → ( ( 𝑄 ↾ ω ) ‘ 𝐴 ) ∈ ran ( 𝑄 ↾ ω ) )
33 31 32 mpan ⊢ ( 𝐴 ∈ ω → ( ( 𝑄 ↾ ω ) ‘ 𝐴 ) ∈ ran ( 𝑄 ↾ ω ) )
34 27 33 eqeltrrd ⊢ ( 𝐴 ∈ ω → ⟨ 𝐴 , ( 2nd ‘ ( 𝑄 ‘ 𝐴 ) ) ⟩ ∈ ran ( 𝑄 ↾ ω ) )
35 df-ima ⊢ ( 𝑄 “ ω ) = ran ( 𝑄 ↾ ω )
36 34 35 eleqtrrdi ⊢ ( 𝐴 ∈ ω → ⟨ 𝐴 , ( 2nd ‘ ( 𝑄 ‘ 𝐴 ) ) ⟩ ∈ ( 𝑄 “ ω ) )
37 df-br ⊢ ( 𝐴 ( 𝑄 “ ω ) ( 2nd ‘ ( 𝑄 ‘ 𝐴 ) ) ↔ ⟨ 𝐴 , ( 2nd ‘ ( 𝑄 ‘ 𝐴 ) ) ⟩ ∈ ( 𝑄 “ ω ) )
38 36 37 sylibr ⊢ ( 𝐴 ∈ ω → 𝐴 ( 𝑄 “ ω ) ( 2nd ‘ ( 𝑄 ‘ 𝐴 ) ) )
39 1 seqomlem2 ⊢ ( 𝑄 “ ω ) Fn ω
40 fnbrfvb ⊢ ( ( ( 𝑄 “ ω ) Fn ω ∧ 𝐴 ∈ ω ) → ( ( ( 𝑄 “ ω ) ‘ 𝐴 ) = ( 2nd ‘ ( 𝑄 ‘ 𝐴 ) ) ↔ 𝐴 ( 𝑄 “ ω ) ( 2nd ‘ ( 𝑄 ‘ 𝐴 ) ) ) )
41 39 40 mpan ⊢ ( 𝐴 ∈ ω → ( ( ( 𝑄 “ ω ) ‘ 𝐴 ) = ( 2nd ‘ ( 𝑄 ‘ 𝐴 ) ) ↔ 𝐴 ( 𝑄 “ ω ) ( 2nd ‘ ( 𝑄 ‘ 𝐴 ) ) ) )
42 38 41 mpbird ⊢ ( 𝐴 ∈ ω → ( ( 𝑄 “ ω ) ‘ 𝐴 ) = ( 2nd ‘ ( 𝑄 ‘ 𝐴 ) ) )
43 42 eqcomd ⊢ ( 𝐴 ∈ ω → ( 2nd ‘ ( 𝑄 ‘ 𝐴 ) ) = ( ( 𝑄 “ ω ) ‘ 𝐴 ) )
44 43 oveq2d ⊢ ( 𝐴 ∈ ω → ( 𝐴 𝐹 ( 2nd ‘ ( 𝑄 ‘ 𝐴 ) ) ) = ( 𝐴 𝐹 ( ( 𝑄 “ ω ) ‘ 𝐴 ) ) )
45 44 opeq2d ⊢ ( 𝐴 ∈ ω → ⟨ suc 𝐴 , ( 𝐴 𝐹 ( 2nd ‘ ( 𝑄 ‘ 𝐴 ) ) ) ⟩ = ⟨ suc 𝐴 , ( 𝐴 𝐹 ( ( 𝑄 “ ω ) ‘ 𝐴 ) ) ⟩ )
46 25 45 eqtrd ⊢ ( 𝐴 ∈ ω → ( 𝐴 ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) ( 2nd ‘ ( 𝑄 ‘ 𝐴 ) ) ) = ⟨ suc 𝐴 , ( 𝐴 𝐹 ( ( 𝑄 “ ω ) ‘ 𝐴 ) ) ⟩ )
47 15 46 syl5eqr ⊢ ( 𝐴 ∈ ω → ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) ‘ ⟨ 𝐴 , ( 2nd ‘ ( 𝑄 ‘ 𝐴 ) ) ⟩ ) = ⟨ suc 𝐴 , ( 𝐴 𝐹 ( ( 𝑄 “ ω ) ‘ 𝐴 ) ) ⟩ )
48 12 14 47 3eqtrd ⊢ ( 𝐴 ∈ ω → ( 𝑄 ‘ suc 𝐴 ) = ⟨ suc 𝐴 , ( 𝐴 𝐹 ( ( 𝑄 “ ω ) ‘ 𝐴 ) ) ⟩ )
49 3 48 eqtrd ⊢ ( 𝐴 ∈ ω → ( ( 𝑄 ↾ ω ) ‘ suc 𝐴 ) = ⟨ suc 𝐴 , ( 𝐴 𝐹 ( ( 𝑄 “ ω ) ‘ 𝐴 ) ) ⟩ )
50 fnfvelrn ⊢ ( ( ( 𝑄 ↾ ω ) Fn ω ∧ suc 𝐴 ∈ ω ) → ( ( 𝑄 ↾ ω ) ‘ suc 𝐴 ) ∈ ran ( 𝑄 ↾ ω ) )
51 31 2 50 sylancr ⊢ ( 𝐴 ∈ ω → ( ( 𝑄 ↾ ω ) ‘ suc 𝐴 ) ∈ ran ( 𝑄 ↾ ω ) )
52 49 51 eqeltrrd ⊢ ( 𝐴 ∈ ω → ⟨ suc 𝐴 , ( 𝐴 𝐹 ( ( 𝑄 “ ω ) ‘ 𝐴 ) ) ⟩ ∈ ran ( 𝑄 ↾ ω ) )
53 52 35 eleqtrrdi ⊢ ( 𝐴 ∈ ω → ⟨ suc 𝐴 , ( 𝐴 𝐹 ( ( 𝑄 “ ω ) ‘ 𝐴 ) ) ⟩ ∈ ( 𝑄 “ ω ) )
54 df-br ⊢ ( suc 𝐴 ( 𝑄 “ ω ) ( 𝐴 𝐹 ( ( 𝑄 “ ω ) ‘ 𝐴 ) ) ↔ ⟨ suc 𝐴 , ( 𝐴 𝐹 ( ( 𝑄 “ ω ) ‘ 𝐴 ) ) ⟩ ∈ ( 𝑄 “ ω ) )
55 53 54 sylibr ⊢ ( 𝐴 ∈ ω → suc 𝐴 ( 𝑄 “ ω ) ( 𝐴 𝐹 ( ( 𝑄 “ ω ) ‘ 𝐴 ) ) )
56 fnbrfvb ⊢ ( ( ( 𝑄 “ ω ) Fn ω ∧ suc 𝐴 ∈ ω ) → ( ( ( 𝑄 “ ω ) ‘ suc 𝐴 ) = ( 𝐴 𝐹 ( ( 𝑄 “ ω ) ‘ 𝐴 ) ) ↔ suc 𝐴 ( 𝑄 “ ω ) ( 𝐴 𝐹 ( ( 𝑄 “ ω ) ‘ 𝐴 ) ) ) )
57 39 2 56 sylancr ⊢ ( 𝐴 ∈ ω → ( ( ( 𝑄 “ ω ) ‘ suc 𝐴 ) = ( 𝐴 𝐹 ( ( 𝑄 “ ω ) ‘ 𝐴 ) ) ↔ suc 𝐴 ( 𝑄 “ ω ) ( 𝐴 𝐹 ( ( 𝑄 “ ω ) ‘ 𝐴 ) ) ) )
58 55 57 mpbird ⊢ ( 𝐴 ∈ ω → ( ( 𝑄 “ ω ) ‘ suc 𝐴 ) = ( 𝐴 𝐹 ( ( 𝑄 “ ω ) ‘ 𝐴 ) ) )