Proof of Theorem seqomlem4
Step | Hyp | Ref
| Expression |
1 | | peano2 7086 |
. . . . . . 7
⊢ (𝐴 ∈ ω → suc 𝐴 ∈
ω) |
2 | | fvres 6207 |
. . . . . . 7
⊢ (suc
𝐴 ∈ ω →
((𝑄 ↾
ω)‘suc 𝐴) =
(𝑄‘suc 𝐴)) |
3 | 1, 2 | syl 17 |
. . . . . 6
⊢ (𝐴 ∈ ω → ((𝑄 ↾ ω)‘suc
𝐴) = (𝑄‘suc 𝐴)) |
4 | | frsuc 7532 |
. . . . . . . 8
⊢ (𝐴 ∈ ω →
((rec((𝑖 ∈ ω,
𝑣 ∈ V ↦
〈suc 𝑖, (𝑖𝐹𝑣)〉), 〈∅, ( I ‘𝐼)〉) ↾
ω)‘suc 𝐴) =
((𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc
𝑖, (𝑖𝐹𝑣)〉)‘((rec((𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc 𝑖, (𝑖𝐹𝑣)〉), 〈∅, ( I ‘𝐼)〉) ↾
ω)‘𝐴))) |
5 | | fvres 6207 |
. . . . . . . . . 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 6192 |
. . . . . . . . 9
⊢ (𝑄‘suc 𝐴) = (rec((𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc 𝑖, (𝑖𝐹𝑣)〉), 〈∅, ( I ‘𝐼)〉)‘suc 𝐴) |
9 | 6, 8 | syl6eqr 2674 |
. . . . . . . 8
⊢ (𝐴 ∈ ω →
((rec((𝑖 ∈ ω,
𝑣 ∈ V ↦
〈suc 𝑖, (𝑖𝐹𝑣)〉), 〈∅, ( I ‘𝐼)〉) ↾
ω)‘suc 𝐴) =
(𝑄‘suc 𝐴)) |
10 | | fvres 6207 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ω →
((rec((𝑖 ∈ ω,
𝑣 ∈ V ↦
〈suc 𝑖, (𝑖𝐹𝑣)〉), 〈∅, ( I ‘𝐼)〉) ↾
ω)‘𝐴) =
(rec((𝑖 ∈ ω,
𝑣 ∈ V ↦
〈suc 𝑖, (𝑖𝐹𝑣)〉), 〈∅, ( I ‘𝐼)〉)‘𝐴)) |
11 | 7 | fveq1i 6192 |
. . . . . . . . . 10
⊢ (𝑄‘𝐴) = (rec((𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc 𝑖, (𝑖𝐹𝑣)〉), 〈∅, ( I ‘𝐼)〉)‘𝐴) |
12 | 10, 11 | syl6eqr 2674 |
. . . . . . . . 9
⊢ (𝐴 ∈ ω →
((rec((𝑖 ∈ ω,
𝑣 ∈ V ↦
〈suc 𝑖, (𝑖𝐹𝑣)〉), 〈∅, ( I ‘𝐼)〉) ↾
ω)‘𝐴) = (𝑄‘𝐴)) |
13 | 12 | fveq2d 6195 |
. . . . . . . 8
⊢ (𝐴 ∈ ω → ((𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc
𝑖, (𝑖𝐹𝑣)〉)‘((rec((𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc 𝑖, (𝑖𝐹𝑣)〉), 〈∅, ( I ‘𝐼)〉) ↾
ω)‘𝐴)) =
((𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc
𝑖, (𝑖𝐹𝑣)〉)‘(𝑄‘𝐴))) |
14 | 4, 9, 13 | 3eqtr3d 2664 |
. . . . . . 7
⊢ (𝐴 ∈ ω → (𝑄‘suc 𝐴) = ((𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc 𝑖, (𝑖𝐹𝑣)〉)‘(𝑄‘𝐴))) |
15 | 7 | seqomlem1 7545 |
. . . . . . . 8
⊢ (𝐴 ∈ ω → (𝑄‘𝐴) = 〈𝐴, (2nd ‘(𝑄‘𝐴))〉) |
16 | 15 | fveq2d 6195 |
. . . . . . 7
⊢ (𝐴 ∈ ω → ((𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc
𝑖, (𝑖𝐹𝑣)〉)‘(𝑄‘𝐴)) = ((𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc 𝑖, (𝑖𝐹𝑣)〉)‘〈𝐴, (2nd ‘(𝑄‘𝐴))〉)) |
17 | | df-ov 6653 |
. . . . . . . 8
⊢ (𝐴(𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc 𝑖, (𝑖𝐹𝑣)〉)(2nd ‘(𝑄‘𝐴))) = ((𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc 𝑖, (𝑖𝐹𝑣)〉)‘〈𝐴, (2nd ‘(𝑄‘𝐴))〉) |
18 | | fvex 6201 |
. . . . . . . . . 10
⊢
(2nd ‘(𝑄‘𝐴)) ∈ V |
19 | | suceq 5790 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝐴 → suc 𝑖 = suc 𝐴) |
20 | | oveq1 6657 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝐴 → (𝑖𝐹𝑣) = (𝐴𝐹𝑣)) |
21 | 19, 20 | opeq12d 4410 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝐴 → 〈suc 𝑖, (𝑖𝐹𝑣)〉 = 〈suc 𝐴, (𝐴𝐹𝑣)〉) |
22 | | oveq2 6658 |
. . . . . . . . . . . 12
⊢ (𝑣 = (2nd ‘(𝑄‘𝐴)) → (𝐴𝐹𝑣) = (𝐴𝐹(2nd ‘(𝑄‘𝐴)))) |
23 | 22 | opeq2d 4409 |
. . . . . . . . . . 11
⊢ (𝑣 = (2nd ‘(𝑄‘𝐴)) → 〈suc 𝐴, (𝐴𝐹𝑣)〉 = 〈suc 𝐴, (𝐴𝐹(2nd ‘(𝑄‘𝐴)))〉) |
24 | | eqid 2622 |
. . . . . . . . . . 11
⊢ (𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc
𝑖, (𝑖𝐹𝑣)〉) = (𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc 𝑖, (𝑖𝐹𝑣)〉) |
25 | | opex 4932 |
. . . . . . . . . . 11
⊢ 〈suc
𝐴, (𝐴𝐹(2nd ‘(𝑄‘𝐴)))〉 ∈ V |
26 | 21, 23, 24, 25 | ovmpt2 6796 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ω ∧
(2nd ‘(𝑄‘𝐴)) ∈ V) → (𝐴(𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc 𝑖, (𝑖𝐹𝑣)〉)(2nd ‘(𝑄‘𝐴))) = 〈suc 𝐴, (𝐴𝐹(2nd ‘(𝑄‘𝐴)))〉) |
27 | 18, 26 | mpan2 707 |
. . . . . . . . 9
⊢ (𝐴 ∈ ω → (𝐴(𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc 𝑖, (𝑖𝐹𝑣)〉)(2nd ‘(𝑄‘𝐴))) = 〈suc 𝐴, (𝐴𝐹(2nd ‘(𝑄‘𝐴)))〉) |
28 | | fvres 6207 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ ω → ((𝑄 ↾ ω)‘𝐴) = (𝑄‘𝐴)) |
29 | 28, 15 | eqtrd 2656 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ ω → ((𝑄 ↾ ω)‘𝐴) = 〈𝐴, (2nd ‘(𝑄‘𝐴))〉) |
30 | | frfnom 7530 |
. . . . . . . . . . . . . . . . . 18
⊢
(rec((𝑖 ∈
ω, 𝑣 ∈ V ↦
〈suc 𝑖, (𝑖𝐹𝑣)〉), 〈∅, ( I ‘𝐼)〉) ↾ ω) Fn
ω |
31 | 7 | reseq1i 5392 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑄 ↾ ω) = (rec((𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc
𝑖, (𝑖𝐹𝑣)〉), 〈∅, ( I ‘𝐼)〉) ↾
ω) |
32 | 31 | fneq1i 5985 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑄 ↾ ω) Fn ω
↔ (rec((𝑖 ∈
ω, 𝑣 ∈ V ↦
〈suc 𝑖, (𝑖𝐹𝑣)〉), 〈∅, ( I ‘𝐼)〉) ↾ ω) Fn
ω) |
33 | 30, 32 | mpbir 221 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑄 ↾ ω) Fn
ω |
34 | | fnfvelrn 6356 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑄 ↾ ω) Fn ω
∧ 𝐴 ∈ ω)
→ ((𝑄 ↾
ω)‘𝐴) ∈
ran (𝑄 ↾
ω)) |
35 | 33, 34 | mpan 706 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ ω → ((𝑄 ↾ ω)‘𝐴) ∈ ran (𝑄 ↾ ω)) |
36 | 29, 35 | eqeltrrd 2702 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ω →
〈𝐴, (2nd
‘(𝑄‘𝐴))〉 ∈ ran (𝑄 ↾
ω)) |
37 | | df-ima 5127 |
. . . . . . . . . . . . . . 15
⊢ (𝑄 “ ω) = ran (𝑄 ↾
ω) |
38 | 36, 37 | syl6eleqr 2712 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ω →
〈𝐴, (2nd
‘(𝑄‘𝐴))〉 ∈ (𝑄 “
ω)) |
39 | | df-br 4654 |
. . . . . . . . . . . . . 14
⊢ (𝐴(𝑄 “ ω)(2nd
‘(𝑄‘𝐴)) ↔ 〈𝐴, (2nd ‘(𝑄‘𝐴))〉 ∈ (𝑄 “ ω)) |
40 | 38, 39 | sylibr 224 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ω → 𝐴(𝑄 “ ω)(2nd
‘(𝑄‘𝐴))) |
41 | 7 | seqomlem2 7546 |
. . . . . . . . . . . . . 14
⊢ (𝑄 “ ω) Fn
ω |
42 | | fnbrfvb 6236 |
. . . . . . . . . . . . . 14
⊢ (((𝑄 “ ω) Fn ω
∧ 𝐴 ∈ ω)
→ (((𝑄 “
ω)‘𝐴) =
(2nd ‘(𝑄‘𝐴)) ↔ 𝐴(𝑄 “ ω)(2nd
‘(𝑄‘𝐴)))) |
43 | 41, 42 | mpan 706 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ω → (((𝑄 “ ω)‘𝐴) = (2nd
‘(𝑄‘𝐴)) ↔ 𝐴(𝑄 “ ω)(2nd
‘(𝑄‘𝐴)))) |
44 | 40, 43 | mpbird 247 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ω → ((𝑄 “ ω)‘𝐴) = (2nd
‘(𝑄‘𝐴))) |
45 | 44 | eqcomd 2628 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ω →
(2nd ‘(𝑄‘𝐴)) = ((𝑄 “ ω)‘𝐴)) |
46 | 45 | oveq2d 6666 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ω → (𝐴𝐹(2nd ‘(𝑄‘𝐴))) = (𝐴𝐹((𝑄 “ ω)‘𝐴))) |
47 | 46 | opeq2d 4409 |
. . . . . . . . 9
⊢ (𝐴 ∈ ω → 〈suc
𝐴, (𝐴𝐹(2nd ‘(𝑄‘𝐴)))〉 = 〈suc 𝐴, (𝐴𝐹((𝑄 “ ω)‘𝐴))〉) |
48 | 27, 47 | eqtrd 2656 |
. . . . . . . 8
⊢ (𝐴 ∈ ω → (𝐴(𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc 𝑖, (𝑖𝐹𝑣)〉)(2nd ‘(𝑄‘𝐴))) = 〈suc 𝐴, (𝐴𝐹((𝑄 “ ω)‘𝐴))〉) |
49 | 17, 48 | syl5eqr 2670 |
. . . . . . 7
⊢ (𝐴 ∈ ω → ((𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc
𝑖, (𝑖𝐹𝑣)〉)‘〈𝐴, (2nd ‘(𝑄‘𝐴))〉) = 〈suc 𝐴, (𝐴𝐹((𝑄 “ ω)‘𝐴))〉) |
50 | 14, 16, 49 | 3eqtrd 2660 |
. . . . . 6
⊢ (𝐴 ∈ ω → (𝑄‘suc 𝐴) = 〈suc 𝐴, (𝐴𝐹((𝑄 “ ω)‘𝐴))〉) |
51 | 3, 50 | eqtrd 2656 |
. . . . 5
⊢ (𝐴 ∈ ω → ((𝑄 ↾ ω)‘suc
𝐴) = 〈suc 𝐴, (𝐴𝐹((𝑄 “ ω)‘𝐴))〉) |
52 | | fnfvelrn 6356 |
. . . . . 6
⊢ (((𝑄 ↾ ω) Fn ω
∧ suc 𝐴 ∈ ω)
→ ((𝑄 ↾
ω)‘suc 𝐴)
∈ ran (𝑄 ↾
ω)) |
53 | 33, 1, 52 | sylancr 695 |
. . . . 5
⊢ (𝐴 ∈ ω → ((𝑄 ↾ ω)‘suc
𝐴) ∈ ran (𝑄 ↾
ω)) |
54 | 51, 53 | eqeltrrd 2702 |
. . . 4
⊢ (𝐴 ∈ ω → 〈suc
𝐴, (𝐴𝐹((𝑄 “ ω)‘𝐴))〉 ∈ ran (𝑄 ↾ ω)) |
55 | 54, 37 | syl6eleqr 2712 |
. . 3
⊢ (𝐴 ∈ ω → 〈suc
𝐴, (𝐴𝐹((𝑄 “ ω)‘𝐴))〉 ∈ (𝑄 “ ω)) |
56 | | df-br 4654 |
. . 3
⊢ (suc
𝐴(𝑄 “ ω)(𝐴𝐹((𝑄 “ ω)‘𝐴)) ↔ 〈suc 𝐴, (𝐴𝐹((𝑄 “ ω)‘𝐴))〉 ∈ (𝑄 “ ω)) |
57 | 55, 56 | sylibr 224 |
. 2
⊢ (𝐴 ∈ ω → suc 𝐴(𝑄 “ ω)(𝐴𝐹((𝑄 “ ω)‘𝐴))) |
58 | | fnbrfvb 6236 |
. . 3
⊢ (((𝑄 “ ω) Fn ω
∧ suc 𝐴 ∈ ω)
→ (((𝑄 “
ω)‘suc 𝐴) =
(𝐴𝐹((𝑄 “ ω)‘𝐴)) ↔ suc 𝐴(𝑄 “ ω)(𝐴𝐹((𝑄 “ ω)‘𝐴)))) |
59 | 41, 1, 58 | sylancr 695 |
. 2
⊢ (𝐴 ∈ ω → (((𝑄 “ ω)‘suc
𝐴) = (𝐴𝐹((𝑄 “ ω)‘𝐴)) ↔ suc 𝐴(𝑄 “ ω)(𝐴𝐹((𝑄 “ ω)‘𝐴)))) |
60 | 57, 59 | mpbird 247 |
1
⊢ (𝐴 ∈ ω → ((𝑄 “ ω)‘suc
𝐴) = (𝐴𝐹((𝑄 “ ω)‘𝐴))) |