Step | Hyp | Ref
| Expression |
1 | | peano2 7828 |
. . . . . . 7
⊢ (𝐴 ∈ ω → suc 𝐴 ∈
ω) |
2 | 1 | fvresd 6863 |
. . . . . 6
⊢ (𝐴 ∈ ω → ((𝑄 ↾ ω)‘suc
𝐴) = (𝑄‘suc 𝐴)) |
3 | | frsuc 8384 |
. . . . . . . 8
⊢ (𝐴 ∈ ω →
((rec((𝑖 ∈ ω,
𝑣 ∈ V ↦
⟨suc 𝑖, (𝑖𝐹𝑣)⟩), ⟨∅, ( I ‘𝐼)⟩) ↾
ω)‘suc 𝐴) =
((𝑖 ∈ ω, 𝑣 ∈ V ↦ ⟨suc
𝑖, (𝑖𝐹𝑣)⟩)‘((rec((𝑖 ∈ ω, 𝑣 ∈ V ↦ ⟨suc 𝑖, (𝑖𝐹𝑣)⟩), ⟨∅, ( I ‘𝐼)⟩) ↾
ω)‘𝐴))) |
4 | 1 | fvresd 6863 |
. . . . . . . . 9
⊢ (𝐴 ∈ ω →
((rec((𝑖 ∈ ω,
𝑣 ∈ V ↦
⟨suc 𝑖, (𝑖𝐹𝑣)⟩), ⟨∅, ( I ‘𝐼)⟩) ↾
ω)‘suc 𝐴) =
(rec((𝑖 ∈ ω,
𝑣 ∈ V ↦
⟨suc 𝑖, (𝑖𝐹𝑣)⟩), ⟨∅, ( I ‘𝐼)⟩)‘suc 𝐴)) |
5 | | seqomlem.a |
. . . . . . . . . 10
⊢ 𝑄 = rec((𝑖 ∈ ω, 𝑣 ∈ V ↦ ⟨suc 𝑖, (𝑖𝐹𝑣)⟩), ⟨∅, ( I ‘𝐼)⟩) |
6 | 5 | fveq1i 6844 |
. . . . . . . . 9
⊢ (𝑄‘suc 𝐴) = (rec((𝑖 ∈ ω, 𝑣 ∈ V ↦ ⟨suc 𝑖, (𝑖𝐹𝑣)⟩), ⟨∅, ( I ‘𝐼)⟩)‘suc 𝐴) |
7 | 4, 6 | eqtr4di 2795 |
. . . . . . . 8
⊢ (𝐴 ∈ ω →
((rec((𝑖 ∈ ω,
𝑣 ∈ V ↦
⟨suc 𝑖, (𝑖𝐹𝑣)⟩), ⟨∅, ( I ‘𝐼)⟩) ↾
ω)‘suc 𝐴) =
(𝑄‘suc 𝐴)) |
8 | | fvres 6862 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ω →
((rec((𝑖 ∈ ω,
𝑣 ∈ V ↦
⟨suc 𝑖, (𝑖𝐹𝑣)⟩), ⟨∅, ( I ‘𝐼)⟩) ↾
ω)‘𝐴) =
(rec((𝑖 ∈ ω,
𝑣 ∈ V ↦
⟨suc 𝑖, (𝑖𝐹𝑣)⟩), ⟨∅, ( I ‘𝐼)⟩)‘𝐴)) |
9 | 5 | fveq1i 6844 |
. . . . . . . . . 10
⊢ (𝑄‘𝐴) = (rec((𝑖 ∈ ω, 𝑣 ∈ V ↦ ⟨suc 𝑖, (𝑖𝐹𝑣)⟩), ⟨∅, ( I ‘𝐼)⟩)‘𝐴) |
10 | 8, 9 | eqtr4di 2795 |
. . . . . . . . 9
⊢ (𝐴 ∈ ω →
((rec((𝑖 ∈ ω,
𝑣 ∈ V ↦
⟨suc 𝑖, (𝑖𝐹𝑣)⟩), ⟨∅, ( I ‘𝐼)⟩) ↾
ω)‘𝐴) = (𝑄‘𝐴)) |
11 | 10 | fveq2d 6847 |
. . . . . . . 8
⊢ (𝐴 ∈ ω → ((𝑖 ∈ ω, 𝑣 ∈ V ↦ ⟨suc
𝑖, (𝑖𝐹𝑣)⟩)‘((rec((𝑖 ∈ ω, 𝑣 ∈ V ↦ ⟨suc 𝑖, (𝑖𝐹𝑣)⟩), ⟨∅, ( I ‘𝐼)⟩) ↾
ω)‘𝐴)) =
((𝑖 ∈ ω, 𝑣 ∈ V ↦ ⟨suc
𝑖, (𝑖𝐹𝑣)⟩)‘(𝑄‘𝐴))) |
12 | 3, 7, 11 | 3eqtr3d 2785 |
. . . . . . 7
⊢ (𝐴 ∈ ω → (𝑄‘suc 𝐴) = ((𝑖 ∈ ω, 𝑣 ∈ V ↦ ⟨suc 𝑖, (𝑖𝐹𝑣)⟩)‘(𝑄‘𝐴))) |
13 | 5 | seqomlem1 8397 |
. . . . . . . 8
⊢ (𝐴 ∈ ω → (𝑄‘𝐴) = ⟨𝐴, (2nd ‘(𝑄‘𝐴))⟩) |
14 | 13 | fveq2d 6847 |
. . . . . . 7
⊢ (𝐴 ∈ ω → ((𝑖 ∈ ω, 𝑣 ∈ V ↦ ⟨suc
𝑖, (𝑖𝐹𝑣)⟩)‘(𝑄‘𝐴)) = ((𝑖 ∈ ω, 𝑣 ∈ V ↦ ⟨suc 𝑖, (𝑖𝐹𝑣)⟩)‘⟨𝐴, (2nd ‘(𝑄‘𝐴))⟩)) |
15 | | df-ov 7361 |
. . . . . . . 8
⊢ (𝐴(𝑖 ∈ ω, 𝑣 ∈ V ↦ ⟨suc 𝑖, (𝑖𝐹𝑣)⟩)(2nd ‘(𝑄‘𝐴))) = ((𝑖 ∈ ω, 𝑣 ∈ V ↦ ⟨suc 𝑖, (𝑖𝐹𝑣)⟩)‘⟨𝐴, (2nd ‘(𝑄‘𝐴))⟩) |
16 | | fvex 6856 |
. . . . . . . . . 10
⊢
(2nd ‘(𝑄‘𝐴)) ∈ V |
17 | | suceq 6384 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝐴 → suc 𝑖 = suc 𝐴) |
18 | | oveq1 7365 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝐴 → (𝑖𝐹𝑣) = (𝐴𝐹𝑣)) |
19 | 17, 18 | opeq12d 4839 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝐴 → ⟨suc 𝑖, (𝑖𝐹𝑣)⟩ = ⟨suc 𝐴, (𝐴𝐹𝑣)⟩) |
20 | | oveq2 7366 |
. . . . . . . . . . . 12
⊢ (𝑣 = (2nd ‘(𝑄‘𝐴)) → (𝐴𝐹𝑣) = (𝐴𝐹(2nd ‘(𝑄‘𝐴)))) |
21 | 20 | opeq2d 4838 |
. . . . . . . . . . 11
⊢ (𝑣 = (2nd ‘(𝑄‘𝐴)) → ⟨suc 𝐴, (𝐴𝐹𝑣)⟩ = ⟨suc 𝐴, (𝐴𝐹(2nd ‘(𝑄‘𝐴)))⟩) |
22 | | eqid 2737 |
. . . . . . . . . . 11
⊢ (𝑖 ∈ ω, 𝑣 ∈ V ↦ ⟨suc
𝑖, (𝑖𝐹𝑣)⟩) = (𝑖 ∈ ω, 𝑣 ∈ V ↦ ⟨suc 𝑖, (𝑖𝐹𝑣)⟩) |
23 | | opex 5422 |
. . . . . . . . . . 11
⊢ ⟨suc
𝐴, (𝐴𝐹(2nd ‘(𝑄‘𝐴)))⟩ ∈ V |
24 | 19, 21, 22, 23 | ovmpo 7516 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ω ∧
(2nd ‘(𝑄‘𝐴)) ∈ V) → (𝐴(𝑖 ∈ ω, 𝑣 ∈ V ↦ ⟨suc 𝑖, (𝑖𝐹𝑣)⟩)(2nd ‘(𝑄‘𝐴))) = ⟨suc 𝐴, (𝐴𝐹(2nd ‘(𝑄‘𝐴)))⟩) |
25 | 16, 24 | mpan2 690 |
. . . . . . . . 9
⊢ (𝐴 ∈ ω → (𝐴(𝑖 ∈ ω, 𝑣 ∈ V ↦ ⟨suc 𝑖, (𝑖𝐹𝑣)⟩)(2nd ‘(𝑄‘𝐴))) = ⟨suc 𝐴, (𝐴𝐹(2nd ‘(𝑄‘𝐴)))⟩) |
26 | | fvres 6862 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ ω → ((𝑄 ↾ ω)‘𝐴) = (𝑄‘𝐴)) |
27 | 26, 13 | eqtrd 2777 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ ω → ((𝑄 ↾ ω)‘𝐴) = ⟨𝐴, (2nd ‘(𝑄‘𝐴))⟩) |
28 | | frfnom 8382 |
. . . . . . . . . . . . . . . . . 18
⊢
(rec((𝑖 ∈
ω, 𝑣 ∈ V ↦
⟨suc 𝑖, (𝑖𝐹𝑣)⟩), ⟨∅, ( I ‘𝐼)⟩) ↾ ω) Fn
ω |
29 | 5 | reseq1i 5934 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑄 ↾ ω) = (rec((𝑖 ∈ ω, 𝑣 ∈ V ↦ ⟨suc
𝑖, (𝑖𝐹𝑣)⟩), ⟨∅, ( I ‘𝐼)⟩) ↾
ω) |
30 | 29 | fneq1i 6600 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑄 ↾ ω) Fn ω
↔ (rec((𝑖 ∈
ω, 𝑣 ∈ V ↦
⟨suc 𝑖, (𝑖𝐹𝑣)⟩), ⟨∅, ( I ‘𝐼)⟩) ↾ ω) Fn
ω) |
31 | 28, 30 | mpbir 230 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑄 ↾ ω) Fn
ω |
32 | | fnfvelrn 7032 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑄 ↾ ω) Fn ω
∧ 𝐴 ∈ ω)
→ ((𝑄 ↾
ω)‘𝐴) ∈
ran (𝑄 ↾
ω)) |
33 | 31, 32 | mpan 689 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ ω → ((𝑄 ↾ ω)‘𝐴) ∈ ran (𝑄 ↾ ω)) |
34 | 27, 33 | eqeltrrd 2839 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ω →
⟨𝐴, (2nd
‘(𝑄‘𝐴))⟩ ∈ ran (𝑄 ↾
ω)) |
35 | | df-ima 5647 |
. . . . . . . . . . . . . . 15
⊢ (𝑄 “ ω) = ran (𝑄 ↾
ω) |
36 | 34, 35 | eleqtrrdi 2849 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ω →
⟨𝐴, (2nd
‘(𝑄‘𝐴))⟩ ∈ (𝑄 “
ω)) |
37 | | df-br 5107 |
. . . . . . . . . . . . . 14
⊢ (𝐴(𝑄 “ ω)(2nd
‘(𝑄‘𝐴)) ↔ ⟨𝐴, (2nd ‘(𝑄‘𝐴))⟩ ∈ (𝑄 “ ω)) |
38 | 36, 37 | sylibr 233 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ω → 𝐴(𝑄 “ ω)(2nd
‘(𝑄‘𝐴))) |
39 | 5 | seqomlem2 8398 |
. . . . . . . . . . . . . 14
⊢ (𝑄 “ ω) Fn
ω |
40 | | fnbrfvb 6896 |
. . . . . . . . . . . . . 14
⊢ (((𝑄 “ ω) Fn ω
∧ 𝐴 ∈ ω)
→ (((𝑄 “
ω)‘𝐴) =
(2nd ‘(𝑄‘𝐴)) ↔ 𝐴(𝑄 “ ω)(2nd
‘(𝑄‘𝐴)))) |
41 | 39, 40 | mpan 689 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ω → (((𝑄 “ ω)‘𝐴) = (2nd
‘(𝑄‘𝐴)) ↔ 𝐴(𝑄 “ ω)(2nd
‘(𝑄‘𝐴)))) |
42 | 38, 41 | mpbird 257 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ω → ((𝑄 “ ω)‘𝐴) = (2nd
‘(𝑄‘𝐴))) |
43 | 42 | eqcomd 2743 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ω →
(2nd ‘(𝑄‘𝐴)) = ((𝑄 “ ω)‘𝐴)) |
44 | 43 | oveq2d 7374 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ω → (𝐴𝐹(2nd ‘(𝑄‘𝐴))) = (𝐴𝐹((𝑄 “ ω)‘𝐴))) |
45 | 44 | opeq2d 4838 |
. . . . . . . . 9
⊢ (𝐴 ∈ ω → ⟨suc
𝐴, (𝐴𝐹(2nd ‘(𝑄‘𝐴)))⟩ = ⟨suc 𝐴, (𝐴𝐹((𝑄 “ ω)‘𝐴))⟩) |
46 | 25, 45 | eqtrd 2777 |
. . . . . . . 8
⊢ (𝐴 ∈ ω → (𝐴(𝑖 ∈ ω, 𝑣 ∈ V ↦ ⟨suc 𝑖, (𝑖𝐹𝑣)⟩)(2nd ‘(𝑄‘𝐴))) = ⟨suc 𝐴, (𝐴𝐹((𝑄 “ ω)‘𝐴))⟩) |
47 | 15, 46 | eqtr3id 2791 |
. . . . . . 7
⊢ (𝐴 ∈ ω → ((𝑖 ∈ ω, 𝑣 ∈ V ↦ ⟨suc
𝑖, (𝑖𝐹𝑣)⟩)‘⟨𝐴, (2nd ‘(𝑄‘𝐴))⟩) = ⟨suc 𝐴, (𝐴𝐹((𝑄 “ ω)‘𝐴))⟩) |
48 | 12, 14, 47 | 3eqtrd 2781 |
. . . . . 6
⊢ (𝐴 ∈ ω → (𝑄‘suc 𝐴) = ⟨suc 𝐴, (𝐴𝐹((𝑄 “ ω)‘𝐴))⟩) |
49 | 2, 48 | eqtrd 2777 |
. . . . 5
⊢ (𝐴 ∈ ω → ((𝑄 ↾ ω)‘suc
𝐴) = ⟨suc 𝐴, (𝐴𝐹((𝑄 “ ω)‘𝐴))⟩) |
50 | | fnfvelrn 7032 |
. . . . . 6
⊢ (((𝑄 ↾ ω) Fn ω
∧ suc 𝐴 ∈ ω)
→ ((𝑄 ↾
ω)‘suc 𝐴)
∈ ran (𝑄 ↾
ω)) |
51 | 31, 1, 50 | sylancr 588 |
. . . . 5
⊢ (𝐴 ∈ ω → ((𝑄 ↾ ω)‘suc
𝐴) ∈ ran (𝑄 ↾
ω)) |
52 | 49, 51 | eqeltrrd 2839 |
. . . 4
⊢ (𝐴 ∈ ω → ⟨suc
𝐴, (𝐴𝐹((𝑄 “ ω)‘𝐴))⟩ ∈ ran (𝑄 ↾ ω)) |
53 | 52, 35 | eleqtrrdi 2849 |
. . 3
⊢ (𝐴 ∈ ω → ⟨suc
𝐴, (𝐴𝐹((𝑄 “ ω)‘𝐴))⟩ ∈ (𝑄 “ ω)) |
54 | | df-br 5107 |
. . 3
⊢ (suc
𝐴(𝑄 “ ω)(𝐴𝐹((𝑄 “ ω)‘𝐴)) ↔ ⟨suc 𝐴, (𝐴𝐹((𝑄 “ ω)‘𝐴))⟩ ∈ (𝑄 “ ω)) |
55 | 53, 54 | sylibr 233 |
. 2
⊢ (𝐴 ∈ ω → suc 𝐴(𝑄 “ ω)(𝐴𝐹((𝑄 “ ω)‘𝐴))) |
56 | | fnbrfvb 6896 |
. . 3
⊢ (((𝑄 “ ω) Fn ω
∧ suc 𝐴 ∈ ω)
→ (((𝑄 “
ω)‘suc 𝐴) =
(𝐴𝐹((𝑄 “ ω)‘𝐴)) ↔ suc 𝐴(𝑄 “ ω)(𝐴𝐹((𝑄 “ ω)‘𝐴)))) |
57 | 39, 1, 56 | sylancr 588 |
. 2
⊢ (𝐴 ∈ ω → (((𝑄 “ ω)‘suc
𝐴) = (𝐴𝐹((𝑄 “ ω)‘𝐴)) ↔ suc 𝐴(𝑄 “ ω)(𝐴𝐹((𝑄 “ ω)‘𝐴)))) |
58 | 55, 57 | mpbird 257 |
1
⊢ (𝐴 ∈ ω → ((𝑄 “ ω)‘suc
𝐴) = (𝐴𝐹((𝑄 “ ω)‘𝐴))) |