Proof of Theorem seqomlem4
Step | Hyp | Ref
| Expression |
1 | | peano2 6978 |
. . . . . . 7
⊢ (𝐴 ∈ ω → suc 𝐴 ∈
ω) |
2 | | fvres 6117 |
. . . . . . 7
⊢ (suc
𝐴 ∈ ω →
((𝑄 ↾
ω)‘suc 𝐴) =
(𝑄‘suc 𝐴)) |
3 | 1, 2 | syl 17 |
. . . . . 6
⊢ (𝐴 ∈ ω → ((𝑄 ↾ ω)‘suc
𝐴) = (𝑄‘suc 𝐴)) |
4 | | frsuc 7419 |
. . . . . . . 8
⊢ (𝐴 ∈ ω →
((rec((𝑖 ∈ ω,
𝑣 ∈ V ↦
〈suc 𝑖, (𝑖𝐹𝑣)〉), 〈∅, ( I ‘𝐼)〉) ↾
ω)‘suc 𝐴) =
((𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc
𝑖, (𝑖𝐹𝑣)〉)‘((rec((𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc 𝑖, (𝑖𝐹𝑣)〉), 〈∅, ( I ‘𝐼)〉) ↾
ω)‘𝐴))) |
5 | | fvres 6117 |
. . . . . . . . . 10
⊢ (suc
𝐴 ∈ ω →
((rec((𝑖 ∈ ω,
𝑣 ∈ V ↦
〈suc 𝑖, (𝑖𝐹𝑣)〉), 〈∅, ( I ‘𝐼)〉) ↾
ω)‘suc 𝐴) =
(rec((𝑖 ∈ ω,
𝑣 ∈ V ↦
〈suc 𝑖, (𝑖𝐹𝑣)〉), 〈∅, ( I ‘𝐼)〉)‘suc 𝐴)) |
6 | 1, 5 | syl 17 |
. . . . . . . . 9
⊢ (𝐴 ∈ ω →
((rec((𝑖 ∈ ω,
𝑣 ∈ V ↦
〈suc 𝑖, (𝑖𝐹𝑣)〉), 〈∅, ( I ‘𝐼)〉) ↾
ω)‘suc 𝐴) =
(rec((𝑖 ∈ ω,
𝑣 ∈ V ↦
〈suc 𝑖, (𝑖𝐹𝑣)〉), 〈∅, ( I ‘𝐼)〉)‘suc 𝐴)) |
7 | | seqomlem.a |
. . . . . . . . . 10
⊢ 𝑄 = rec((𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc 𝑖, (𝑖𝐹𝑣)〉), 〈∅, ( I ‘𝐼)〉) |
8 | 7 | fveq1i 6104 |
. . . . . . . . 9
⊢ (𝑄‘suc 𝐴) = (rec((𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc 𝑖, (𝑖𝐹𝑣)〉), 〈∅, ( I ‘𝐼)〉)‘suc 𝐴) |
9 | 6, 8 | syl6eqr 2662 |
. . . . . . . 8
⊢ (𝐴 ∈ ω →
((rec((𝑖 ∈ ω,
𝑣 ∈ V ↦
〈suc 𝑖, (𝑖𝐹𝑣)〉), 〈∅, ( I ‘𝐼)〉) ↾
ω)‘suc 𝐴) =
(𝑄‘suc 𝐴)) |
10 | | fvres 6117 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ω →
((rec((𝑖 ∈ ω,
𝑣 ∈ V ↦
〈suc 𝑖, (𝑖𝐹𝑣)〉), 〈∅, ( I ‘𝐼)〉) ↾
ω)‘𝐴) =
(rec((𝑖 ∈ ω,
𝑣 ∈ V ↦
〈suc 𝑖, (𝑖𝐹𝑣)〉), 〈∅, ( I ‘𝐼)〉)‘𝐴)) |
11 | 7 | fveq1i 6104 |
. . . . . . . . . 10
⊢ (𝑄‘𝐴) = (rec((𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc 𝑖, (𝑖𝐹𝑣)〉), 〈∅, ( I ‘𝐼)〉)‘𝐴) |
12 | 10, 11 | syl6eqr 2662 |
. . . . . . . . 9
⊢ (𝐴 ∈ ω →
((rec((𝑖 ∈ ω,
𝑣 ∈ V ↦
〈suc 𝑖, (𝑖𝐹𝑣)〉), 〈∅, ( I ‘𝐼)〉) ↾
ω)‘𝐴) = (𝑄‘𝐴)) |
13 | 12 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝐴 ∈ ω → ((𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc
𝑖, (𝑖𝐹𝑣)〉)‘((rec((𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc 𝑖, (𝑖𝐹𝑣)〉), 〈∅, ( I ‘𝐼)〉) ↾
ω)‘𝐴)) =
((𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc
𝑖, (𝑖𝐹𝑣)〉)‘(𝑄‘𝐴))) |
14 | 4, 9, 13 | 3eqtr3d 2652 |
. . . . . . 7
⊢ (𝐴 ∈ ω → (𝑄‘suc 𝐴) = ((𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc 𝑖, (𝑖𝐹𝑣)〉)‘(𝑄‘𝐴))) |
15 | 7 | seqomlem1 7432 |
. . . . . . . 8
⊢ (𝐴 ∈ ω → (𝑄‘𝐴) = 〈𝐴, (2nd ‘(𝑄‘𝐴))〉) |
16 | 15 | fveq2d 6107 |
. . . . . . 7
⊢ (𝐴 ∈ ω → ((𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc
𝑖, (𝑖𝐹𝑣)〉)‘(𝑄‘𝐴)) = ((𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc 𝑖, (𝑖𝐹𝑣)〉)‘〈𝐴, (2nd ‘(𝑄‘𝐴))〉)) |
17 | | df-ov 6552 |
. . . . . . . 8
⊢ (𝐴(𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc 𝑖, (𝑖𝐹𝑣)〉)(2nd ‘(𝑄‘𝐴))) = ((𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc 𝑖, (𝑖𝐹𝑣)〉)‘〈𝐴, (2nd ‘(𝑄‘𝐴))〉) |
18 | | fvex 6113 |
. . . . . . . . . 10
⊢
(2nd ‘(𝑄‘𝐴)) ∈ V |
19 | | suceq 5707 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝐴 → suc 𝑖 = suc 𝐴) |
20 | | oveq1 6556 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝐴 → (𝑖𝐹𝑣) = (𝐴𝐹𝑣)) |
21 | 19, 20 | opeq12d 4348 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝐴 → 〈suc 𝑖, (𝑖𝐹𝑣)〉 = 〈suc 𝐴, (𝐴𝐹𝑣)〉) |
22 | | oveq2 6557 |
. . . . . . . . . . . 12
⊢ (𝑣 = (2nd ‘(𝑄‘𝐴)) → (𝐴𝐹𝑣) = (𝐴𝐹(2nd ‘(𝑄‘𝐴)))) |
23 | 22 | opeq2d 4347 |
. . . . . . . . . . 11
⊢ (𝑣 = (2nd ‘(𝑄‘𝐴)) → 〈suc 𝐴, (𝐴𝐹𝑣)〉 = 〈suc 𝐴, (𝐴𝐹(2nd ‘(𝑄‘𝐴)))〉) |
24 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc
𝑖, (𝑖𝐹𝑣)〉) = (𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc 𝑖, (𝑖𝐹𝑣)〉) |
25 | | opex 4859 |
. . . . . . . . . . 11
⊢ 〈suc
𝐴, (𝐴𝐹(2nd ‘(𝑄‘𝐴)))〉 ∈ V |
26 | 21, 23, 24, 25 | ovmpt2 6694 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ω ∧
(2nd ‘(𝑄‘𝐴)) ∈ V) → (𝐴(𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc 𝑖, (𝑖𝐹𝑣)〉)(2nd ‘(𝑄‘𝐴))) = 〈suc 𝐴, (𝐴𝐹(2nd ‘(𝑄‘𝐴)))〉) |
27 | 18, 26 | mpan2 703 |
. . . . . . . . 9
⊢ (𝐴 ∈ ω → (𝐴(𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc 𝑖, (𝑖𝐹𝑣)〉)(2nd ‘(𝑄‘𝐴))) = 〈suc 𝐴, (𝐴𝐹(2nd ‘(𝑄‘𝐴)))〉) |
28 | | fvres 6117 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ ω → ((𝑄 ↾ ω)‘𝐴) = (𝑄‘𝐴)) |
29 | 28, 15 | eqtrd 2644 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ ω → ((𝑄 ↾ ω)‘𝐴) = 〈𝐴, (2nd ‘(𝑄‘𝐴))〉) |
30 | | frfnom 7417 |
. . . . . . . . . . . . . . . . . 18
⊢
(rec((𝑖 ∈
ω, 𝑣 ∈ V ↦
〈suc 𝑖, (𝑖𝐹𝑣)〉), 〈∅, ( I ‘𝐼)〉) ↾ ω) Fn
ω |
31 | 7 | reseq1i 5313 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑄 ↾ ω) = (rec((𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc
𝑖, (𝑖𝐹𝑣)〉), 〈∅, ( I ‘𝐼)〉) ↾
ω) |
32 | 31 | fneq1i 5899 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑄 ↾ ω) Fn ω
↔ (rec((𝑖 ∈
ω, 𝑣 ∈ V ↦
〈suc 𝑖, (𝑖𝐹𝑣)〉), 〈∅, ( I ‘𝐼)〉) ↾ ω) Fn
ω) |
33 | 30, 32 | mpbir 220 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑄 ↾ ω) Fn
ω |
34 | | fnfvelrn 6264 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑄 ↾ ω) Fn ω
∧ 𝐴 ∈ ω)
→ ((𝑄 ↾
ω)‘𝐴) ∈
ran (𝑄 ↾
ω)) |
35 | 33, 34 | mpan 702 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ ω → ((𝑄 ↾ ω)‘𝐴) ∈ ran (𝑄 ↾ ω)) |
36 | 29, 35 | eqeltrrd 2689 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ω →
〈𝐴, (2nd
‘(𝑄‘𝐴))〉 ∈ ran (𝑄 ↾
ω)) |
37 | | df-ima 5051 |
. . . . . . . . . . . . . . 15
⊢ (𝑄 “ ω) = ran (𝑄 ↾
ω) |
38 | 36, 37 | syl6eleqr 2699 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ω →
〈𝐴, (2nd
‘(𝑄‘𝐴))〉 ∈ (𝑄 “
ω)) |
39 | | df-br 4584 |
. . . . . . . . . . . . . 14
⊢ (𝐴(𝑄 “ ω)(2nd
‘(𝑄‘𝐴)) ↔ 〈𝐴, (2nd ‘(𝑄‘𝐴))〉 ∈ (𝑄 “ ω)) |
40 | 38, 39 | sylibr 223 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ω → 𝐴(𝑄 “ ω)(2nd
‘(𝑄‘𝐴))) |
41 | 7 | seqomlem2 7433 |
. . . . . . . . . . . . . 14
⊢ (𝑄 “ ω) Fn
ω |
42 | | fnbrfvb 6146 |
. . . . . . . . . . . . . 14
⊢ (((𝑄 “ ω) Fn ω
∧ 𝐴 ∈ ω)
→ (((𝑄 “
ω)‘𝐴) =
(2nd ‘(𝑄‘𝐴)) ↔ 𝐴(𝑄 “ ω)(2nd
‘(𝑄‘𝐴)))) |
43 | 41, 42 | mpan 702 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ω → (((𝑄 “ ω)‘𝐴) = (2nd
‘(𝑄‘𝐴)) ↔ 𝐴(𝑄 “ ω)(2nd
‘(𝑄‘𝐴)))) |
44 | 40, 43 | mpbird 246 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ω → ((𝑄 “ ω)‘𝐴) = (2nd
‘(𝑄‘𝐴))) |
45 | 44 | eqcomd 2616 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ω →
(2nd ‘(𝑄‘𝐴)) = ((𝑄 “ ω)‘𝐴)) |
46 | 45 | oveq2d 6565 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ω → (𝐴𝐹(2nd ‘(𝑄‘𝐴))) = (𝐴𝐹((𝑄 “ ω)‘𝐴))) |
47 | 46 | opeq2d 4347 |
. . . . . . . . 9
⊢ (𝐴 ∈ ω → 〈suc
𝐴, (𝐴𝐹(2nd ‘(𝑄‘𝐴)))〉 = 〈suc 𝐴, (𝐴𝐹((𝑄 “ ω)‘𝐴))〉) |
48 | 27, 47 | eqtrd 2644 |
. . . . . . . 8
⊢ (𝐴 ∈ ω → (𝐴(𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc 𝑖, (𝑖𝐹𝑣)〉)(2nd ‘(𝑄‘𝐴))) = 〈suc 𝐴, (𝐴𝐹((𝑄 “ ω)‘𝐴))〉) |
49 | 17, 48 | syl5eqr 2658 |
. . . . . . 7
⊢ (𝐴 ∈ ω → ((𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc
𝑖, (𝑖𝐹𝑣)〉)‘〈𝐴, (2nd ‘(𝑄‘𝐴))〉) = 〈suc 𝐴, (𝐴𝐹((𝑄 “ ω)‘𝐴))〉) |
50 | 14, 16, 49 | 3eqtrd 2648 |
. . . . . 6
⊢ (𝐴 ∈ ω → (𝑄‘suc 𝐴) = 〈suc 𝐴, (𝐴𝐹((𝑄 “ ω)‘𝐴))〉) |
51 | 3, 50 | eqtrd 2644 |
. . . . 5
⊢ (𝐴 ∈ ω → ((𝑄 ↾ ω)‘suc
𝐴) = 〈suc 𝐴, (𝐴𝐹((𝑄 “ ω)‘𝐴))〉) |
52 | | fnfvelrn 6264 |
. . . . . 6
⊢ (((𝑄 ↾ ω) Fn ω
∧ suc 𝐴 ∈ ω)
→ ((𝑄 ↾
ω)‘suc 𝐴)
∈ ran (𝑄 ↾
ω)) |
53 | 33, 1, 52 | sylancr 694 |
. . . . 5
⊢ (𝐴 ∈ ω → ((𝑄 ↾ ω)‘suc
𝐴) ∈ ran (𝑄 ↾
ω)) |
54 | 51, 53 | eqeltrrd 2689 |
. . . 4
⊢ (𝐴 ∈ ω → 〈suc
𝐴, (𝐴𝐹((𝑄 “ ω)‘𝐴))〉 ∈ ran (𝑄 ↾ ω)) |
55 | 54, 37 | syl6eleqr 2699 |
. . 3
⊢ (𝐴 ∈ ω → 〈suc
𝐴, (𝐴𝐹((𝑄 “ ω)‘𝐴))〉 ∈ (𝑄 “ ω)) |
56 | | df-br 4584 |
. . 3
⊢ (suc
𝐴(𝑄 “ ω)(𝐴𝐹((𝑄 “ ω)‘𝐴)) ↔ 〈suc 𝐴, (𝐴𝐹((𝑄 “ ω)‘𝐴))〉 ∈ (𝑄 “ ω)) |
57 | 55, 56 | sylibr 223 |
. 2
⊢ (𝐴 ∈ ω → suc 𝐴(𝑄 “ ω)(𝐴𝐹((𝑄 “ ω)‘𝐴))) |
58 | | fnbrfvb 6146 |
. . 3
⊢ (((𝑄 “ ω) Fn ω
∧ suc 𝐴 ∈ ω)
→ (((𝑄 “
ω)‘suc 𝐴) =
(𝐴𝐹((𝑄 “ ω)‘𝐴)) ↔ suc 𝐴(𝑄 “ ω)(𝐴𝐹((𝑄 “ ω)‘𝐴)))) |
59 | 41, 1, 58 | sylancr 694 |
. 2
⊢ (𝐴 ∈ ω → (((𝑄 “ ω)‘suc
𝐴) = (𝐴𝐹((𝑄 “ ω)‘𝐴)) ↔ suc 𝐴(𝑄 “ ω)(𝐴𝐹((𝑄 “ ω)‘𝐴)))) |
60 | 57, 59 | mpbird 246 |
1
⊢ (𝐴 ∈ ω → ((𝑄 “ ω)‘suc
𝐴) = (𝐴𝐹((𝑄 “ ω)‘𝐴))) |