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 eqtr4di ( 𝐴 ∈ ω → ( ( 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 eqtr4di ( 𝐴 ∈ ω → ( ( 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 eqtr3id ( 𝐴 ∈ ω → ( ( 𝑖 ∈ ω , 𝑣 ∈ 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 𝐴 ) = ( 𝐴 𝐹 ( ( 𝑄 “ ω ) ‘ 𝐴 ) ) )