Step | Hyp | Ref
| Expression |
1 | | fveq2 6103 |
. . 3
⊢ (𝑎 = ∅ → (𝑄‘𝑎) = (𝑄‘∅)) |
2 | | id 22 |
. . . 4
⊢ (𝑎 = ∅ → 𝑎 = ∅) |
3 | 1 | fveq2d 6107 |
. . . 4
⊢ (𝑎 = ∅ →
(2nd ‘(𝑄‘𝑎)) = (2nd ‘(𝑄‘∅))) |
4 | 2, 3 | opeq12d 4348 |
. . 3
⊢ (𝑎 = ∅ → 〈𝑎, (2nd ‘(𝑄‘𝑎))〉 = 〈∅, (2nd
‘(𝑄‘∅))〉) |
5 | 1, 4 | eqeq12d 2625 |
. 2
⊢ (𝑎 = ∅ → ((𝑄‘𝑎) = 〈𝑎, (2nd ‘(𝑄‘𝑎))〉 ↔ (𝑄‘∅) = 〈∅,
(2nd ‘(𝑄‘∅))〉)) |
6 | | fveq2 6103 |
. . 3
⊢ (𝑎 = 𝑏 → (𝑄‘𝑎) = (𝑄‘𝑏)) |
7 | | id 22 |
. . . 4
⊢ (𝑎 = 𝑏 → 𝑎 = 𝑏) |
8 | 6 | fveq2d 6107 |
. . . 4
⊢ (𝑎 = 𝑏 → (2nd ‘(𝑄‘𝑎)) = (2nd ‘(𝑄‘𝑏))) |
9 | 7, 8 | opeq12d 4348 |
. . 3
⊢ (𝑎 = 𝑏 → 〈𝑎, (2nd ‘(𝑄‘𝑎))〉 = 〈𝑏, (2nd ‘(𝑄‘𝑏))〉) |
10 | 6, 9 | eqeq12d 2625 |
. 2
⊢ (𝑎 = 𝑏 → ((𝑄‘𝑎) = 〈𝑎, (2nd ‘(𝑄‘𝑎))〉 ↔ (𝑄‘𝑏) = 〈𝑏, (2nd ‘(𝑄‘𝑏))〉)) |
11 | | fveq2 6103 |
. . 3
⊢ (𝑎 = suc 𝑏 → (𝑄‘𝑎) = (𝑄‘suc 𝑏)) |
12 | | id 22 |
. . . 4
⊢ (𝑎 = suc 𝑏 → 𝑎 = suc 𝑏) |
13 | 11 | fveq2d 6107 |
. . . 4
⊢ (𝑎 = suc 𝑏 → (2nd ‘(𝑄‘𝑎)) = (2nd ‘(𝑄‘suc 𝑏))) |
14 | 12, 13 | opeq12d 4348 |
. . 3
⊢ (𝑎 = suc 𝑏 → 〈𝑎, (2nd ‘(𝑄‘𝑎))〉 = 〈suc 𝑏, (2nd ‘(𝑄‘suc 𝑏))〉) |
15 | 11, 14 | eqeq12d 2625 |
. 2
⊢ (𝑎 = suc 𝑏 → ((𝑄‘𝑎) = 〈𝑎, (2nd ‘(𝑄‘𝑎))〉 ↔ (𝑄‘suc 𝑏) = 〈suc 𝑏, (2nd ‘(𝑄‘suc 𝑏))〉)) |
16 | | fveq2 6103 |
. . 3
⊢ (𝑎 = 𝐴 → (𝑄‘𝑎) = (𝑄‘𝐴)) |
17 | | id 22 |
. . . 4
⊢ (𝑎 = 𝐴 → 𝑎 = 𝐴) |
18 | 16 | fveq2d 6107 |
. . . 4
⊢ (𝑎 = 𝐴 → (2nd ‘(𝑄‘𝑎)) = (2nd ‘(𝑄‘𝐴))) |
19 | 17, 18 | opeq12d 4348 |
. . 3
⊢ (𝑎 = 𝐴 → 〈𝑎, (2nd ‘(𝑄‘𝑎))〉 = 〈𝐴, (2nd ‘(𝑄‘𝐴))〉) |
20 | 16, 19 | eqeq12d 2625 |
. 2
⊢ (𝑎 = 𝐴 → ((𝑄‘𝑎) = 〈𝑎, (2nd ‘(𝑄‘𝑎))〉 ↔ (𝑄‘𝐴) = 〈𝐴, (2nd ‘(𝑄‘𝐴))〉)) |
21 | | seqomlem.a |
. . . . 5
⊢ 𝑄 = rec((𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc 𝑖, (𝑖𝐹𝑣)〉), 〈∅, ( I ‘𝐼)〉) |
22 | 21 | fveq1i 6104 |
. . . 4
⊢ (𝑄‘∅) = (rec((𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc
𝑖, (𝑖𝐹𝑣)〉), 〈∅, ( I ‘𝐼)〉)‘∅) |
23 | | opex 4859 |
. . . . 5
⊢
〈∅, ( I ‘𝐼)〉 ∈ V |
24 | 23 | rdg0 7404 |
. . . 4
⊢
(rec((𝑖 ∈
ω, 𝑣 ∈ V ↦
〈suc 𝑖, (𝑖𝐹𝑣)〉), 〈∅, ( I ‘𝐼)〉)‘∅) =
〈∅, ( I ‘𝐼)〉 |
25 | 22, 24 | eqtri 2632 |
. . 3
⊢ (𝑄‘∅) = 〈∅,
( I ‘𝐼)〉 |
26 | | 0ex 4718 |
. . . . . . 7
⊢ ∅
∈ V |
27 | | fvex 6113 |
. . . . . . 7
⊢ ( I
‘𝐼) ∈
V |
28 | 26, 27 | op2nd 7068 |
. . . . . 6
⊢
(2nd ‘〈∅, ( I ‘𝐼)〉) = ( I ‘𝐼) |
29 | 28 | eqcomi 2619 |
. . . . 5
⊢ ( I
‘𝐼) = (2nd
‘〈∅, ( I ‘𝐼)〉) |
30 | 29 | opeq2i 4344 |
. . . 4
⊢
〈∅, ( I ‘𝐼)〉 = 〈∅, (2nd
‘〈∅, ( I ‘𝐼)〉)〉 |
31 | | id 22 |
. . . 4
⊢ ((𝑄‘∅) = 〈∅,
( I ‘𝐼)〉 →
(𝑄‘∅) =
〈∅, ( I ‘𝐼)〉) |
32 | | fveq2 6103 |
. . . . 5
⊢ ((𝑄‘∅) = 〈∅,
( I ‘𝐼)〉 →
(2nd ‘(𝑄‘∅)) = (2nd
‘〈∅, ( I ‘𝐼)〉)) |
33 | 32 | opeq2d 4347 |
. . . 4
⊢ ((𝑄‘∅) = 〈∅,
( I ‘𝐼)〉 →
〈∅, (2nd ‘(𝑄‘∅))〉 = 〈∅,
(2nd ‘〈∅, ( I ‘𝐼)〉)〉) |
34 | 30, 31, 33 | 3eqtr4a 2670 |
. . 3
⊢ ((𝑄‘∅) = 〈∅,
( I ‘𝐼)〉 →
(𝑄‘∅) =
〈∅, (2nd ‘(𝑄‘∅))〉) |
35 | 25, 34 | ax-mp 5 |
. 2
⊢ (𝑄‘∅) = 〈∅,
(2nd ‘(𝑄‘∅))〉 |
36 | | df-ov 6552 |
. . . . . 6
⊢ (𝑏(𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc 𝑖, (𝑖𝐹𝑣)〉)(2nd ‘(𝑄‘𝑏))) = ((𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc 𝑖, (𝑖𝐹𝑣)〉)‘〈𝑏, (2nd ‘(𝑄‘𝑏))〉) |
37 | | fvex 6113 |
. . . . . . 7
⊢
(2nd ‘(𝑄‘𝑏)) ∈ V |
38 | | suceq 5707 |
. . . . . . . . 9
⊢ (𝑖 = 𝑏 → suc 𝑖 = suc 𝑏) |
39 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑖 = 𝑏 → (𝑖𝐹𝑣) = (𝑏𝐹𝑣)) |
40 | 38, 39 | opeq12d 4348 |
. . . . . . . 8
⊢ (𝑖 = 𝑏 → 〈suc 𝑖, (𝑖𝐹𝑣)〉 = 〈suc 𝑏, (𝑏𝐹𝑣)〉) |
41 | | oveq2 6557 |
. . . . . . . . 9
⊢ (𝑣 = (2nd ‘(𝑄‘𝑏)) → (𝑏𝐹𝑣) = (𝑏𝐹(2nd ‘(𝑄‘𝑏)))) |
42 | 41 | opeq2d 4347 |
. . . . . . . 8
⊢ (𝑣 = (2nd ‘(𝑄‘𝑏)) → 〈suc 𝑏, (𝑏𝐹𝑣)〉 = 〈suc 𝑏, (𝑏𝐹(2nd ‘(𝑄‘𝑏)))〉) |
43 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc
𝑖, (𝑖𝐹𝑣)〉) = (𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc 𝑖, (𝑖𝐹𝑣)〉) |
44 | | opex 4859 |
. . . . . . . 8
⊢ 〈suc
𝑏, (𝑏𝐹(2nd ‘(𝑄‘𝑏)))〉 ∈ V |
45 | 40, 42, 43, 44 | ovmpt2 6694 |
. . . . . . 7
⊢ ((𝑏 ∈ ω ∧
(2nd ‘(𝑄‘𝑏)) ∈ V) → (𝑏(𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc 𝑖, (𝑖𝐹𝑣)〉)(2nd ‘(𝑄‘𝑏))) = 〈suc 𝑏, (𝑏𝐹(2nd ‘(𝑄‘𝑏)))〉) |
46 | 37, 45 | mpan2 703 |
. . . . . 6
⊢ (𝑏 ∈ ω → (𝑏(𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc 𝑖, (𝑖𝐹𝑣)〉)(2nd ‘(𝑄‘𝑏))) = 〈suc 𝑏, (𝑏𝐹(2nd ‘(𝑄‘𝑏)))〉) |
47 | 36, 46 | syl5eqr 2658 |
. . . . 5
⊢ (𝑏 ∈ ω → ((𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc
𝑖, (𝑖𝐹𝑣)〉)‘〈𝑏, (2nd ‘(𝑄‘𝑏))〉) = 〈suc 𝑏, (𝑏𝐹(2nd ‘(𝑄‘𝑏)))〉) |
48 | | fveq2 6103 |
. . . . . 6
⊢ ((𝑄‘𝑏) = 〈𝑏, (2nd ‘(𝑄‘𝑏))〉 → ((𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc 𝑖, (𝑖𝐹𝑣)〉)‘(𝑄‘𝑏)) = ((𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc 𝑖, (𝑖𝐹𝑣)〉)‘〈𝑏, (2nd ‘(𝑄‘𝑏))〉)) |
49 | 48 | eqeq1d 2612 |
. . . . 5
⊢ ((𝑄‘𝑏) = 〈𝑏, (2nd ‘(𝑄‘𝑏))〉 → (((𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc 𝑖, (𝑖𝐹𝑣)〉)‘(𝑄‘𝑏)) = 〈suc 𝑏, (𝑏𝐹(2nd ‘(𝑄‘𝑏)))〉 ↔ ((𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc 𝑖, (𝑖𝐹𝑣)〉)‘〈𝑏, (2nd ‘(𝑄‘𝑏))〉) = 〈suc 𝑏, (𝑏𝐹(2nd ‘(𝑄‘𝑏)))〉)) |
50 | 47, 49 | syl5ibrcom 236 |
. . . 4
⊢ (𝑏 ∈ ω → ((𝑄‘𝑏) = 〈𝑏, (2nd ‘(𝑄‘𝑏))〉 → ((𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc 𝑖, (𝑖𝐹𝑣)〉)‘(𝑄‘𝑏)) = 〈suc 𝑏, (𝑏𝐹(2nd ‘(𝑄‘𝑏)))〉)) |
51 | | vex 3176 |
. . . . . . . . . 10
⊢ 𝑏 ∈ V |
52 | 51 | sucex 6903 |
. . . . . . . . 9
⊢ suc 𝑏 ∈ V |
53 | | ovex 6577 |
. . . . . . . . 9
⊢ (𝑏𝐹(2nd ‘(𝑄‘𝑏))) ∈ V |
54 | 52, 53 | op2nd 7068 |
. . . . . . . 8
⊢
(2nd ‘〈suc 𝑏, (𝑏𝐹(2nd ‘(𝑄‘𝑏)))〉) = (𝑏𝐹(2nd ‘(𝑄‘𝑏))) |
55 | 54 | eqcomi 2619 |
. . . . . . 7
⊢ (𝑏𝐹(2nd ‘(𝑄‘𝑏))) = (2nd ‘〈suc 𝑏, (𝑏𝐹(2nd ‘(𝑄‘𝑏)))〉) |
56 | 55 | a1i 11 |
. . . . . 6
⊢ (𝑏 ∈ ω → (𝑏𝐹(2nd ‘(𝑄‘𝑏))) = (2nd ‘〈suc 𝑏, (𝑏𝐹(2nd ‘(𝑄‘𝑏)))〉)) |
57 | 56 | opeq2d 4347 |
. . . . 5
⊢ (𝑏 ∈ ω → 〈suc
𝑏, (𝑏𝐹(2nd ‘(𝑄‘𝑏)))〉 = 〈suc 𝑏, (2nd ‘〈suc 𝑏, (𝑏𝐹(2nd ‘(𝑄‘𝑏)))〉)〉) |
58 | | id 22 |
. . . . . 6
⊢ (((𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc
𝑖, (𝑖𝐹𝑣)〉)‘(𝑄‘𝑏)) = 〈suc 𝑏, (𝑏𝐹(2nd ‘(𝑄‘𝑏)))〉 → ((𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc 𝑖, (𝑖𝐹𝑣)〉)‘(𝑄‘𝑏)) = 〈suc 𝑏, (𝑏𝐹(2nd ‘(𝑄‘𝑏)))〉) |
59 | | fveq2 6103 |
. . . . . . 7
⊢ (((𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc
𝑖, (𝑖𝐹𝑣)〉)‘(𝑄‘𝑏)) = 〈suc 𝑏, (𝑏𝐹(2nd ‘(𝑄‘𝑏)))〉 → (2nd
‘((𝑖 ∈ ω,
𝑣 ∈ V ↦
〈suc 𝑖, (𝑖𝐹𝑣)〉)‘(𝑄‘𝑏))) = (2nd ‘〈suc 𝑏, (𝑏𝐹(2nd ‘(𝑄‘𝑏)))〉)) |
60 | 59 | opeq2d 4347 |
. . . . . 6
⊢ (((𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc
𝑖, (𝑖𝐹𝑣)〉)‘(𝑄‘𝑏)) = 〈suc 𝑏, (𝑏𝐹(2nd ‘(𝑄‘𝑏)))〉 → 〈suc 𝑏, (2nd ‘((𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc 𝑖, (𝑖𝐹𝑣)〉)‘(𝑄‘𝑏)))〉 = 〈suc 𝑏, (2nd ‘〈suc 𝑏, (𝑏𝐹(2nd ‘(𝑄‘𝑏)))〉)〉) |
61 | 58, 60 | eqeq12d 2625 |
. . . . 5
⊢ (((𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc
𝑖, (𝑖𝐹𝑣)〉)‘(𝑄‘𝑏)) = 〈suc 𝑏, (𝑏𝐹(2nd ‘(𝑄‘𝑏)))〉 → (((𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc 𝑖, (𝑖𝐹𝑣)〉)‘(𝑄‘𝑏)) = 〈suc 𝑏, (2nd ‘((𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc 𝑖, (𝑖𝐹𝑣)〉)‘(𝑄‘𝑏)))〉 ↔ 〈suc 𝑏, (𝑏𝐹(2nd ‘(𝑄‘𝑏)))〉 = 〈suc 𝑏, (2nd ‘〈suc 𝑏, (𝑏𝐹(2nd ‘(𝑄‘𝑏)))〉)〉)) |
62 | 57, 61 | syl5ibrcom 236 |
. . . 4
⊢ (𝑏 ∈ ω → (((𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc
𝑖, (𝑖𝐹𝑣)〉)‘(𝑄‘𝑏)) = 〈suc 𝑏, (𝑏𝐹(2nd ‘(𝑄‘𝑏)))〉 → ((𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc 𝑖, (𝑖𝐹𝑣)〉)‘(𝑄‘𝑏)) = 〈suc 𝑏, (2nd ‘((𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc 𝑖, (𝑖𝐹𝑣)〉)‘(𝑄‘𝑏)))〉)) |
63 | 50, 62 | syld 46 |
. . 3
⊢ (𝑏 ∈ ω → ((𝑄‘𝑏) = 〈𝑏, (2nd ‘(𝑄‘𝑏))〉 → ((𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc 𝑖, (𝑖𝐹𝑣)〉)‘(𝑄‘𝑏)) = 〈suc 𝑏, (2nd ‘((𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc 𝑖, (𝑖𝐹𝑣)〉)‘(𝑄‘𝑏)))〉)) |
64 | | frsuc 7419 |
. . . . 5
⊢ (𝑏 ∈ ω →
((rec((𝑖 ∈ ω,
𝑣 ∈ V ↦
〈suc 𝑖, (𝑖𝐹𝑣)〉), 〈∅, ( I ‘𝐼)〉) ↾
ω)‘suc 𝑏) =
((𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc
𝑖, (𝑖𝐹𝑣)〉)‘((rec((𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc 𝑖, (𝑖𝐹𝑣)〉), 〈∅, ( I ‘𝐼)〉) ↾
ω)‘𝑏))) |
65 | | peano2 6978 |
. . . . . . 7
⊢ (𝑏 ∈ ω → suc 𝑏 ∈
ω) |
66 | | fvres 6117 |
. . . . . . 7
⊢ (suc
𝑏 ∈ ω →
((rec((𝑖 ∈ ω,
𝑣 ∈ V ↦
〈suc 𝑖, (𝑖𝐹𝑣)〉), 〈∅, ( I ‘𝐼)〉) ↾
ω)‘suc 𝑏) =
(rec((𝑖 ∈ ω,
𝑣 ∈ V ↦
〈suc 𝑖, (𝑖𝐹𝑣)〉), 〈∅, ( I ‘𝐼)〉)‘suc 𝑏)) |
67 | 65, 66 | syl 17 |
. . . . . 6
⊢ (𝑏 ∈ ω →
((rec((𝑖 ∈ ω,
𝑣 ∈ V ↦
〈suc 𝑖, (𝑖𝐹𝑣)〉), 〈∅, ( I ‘𝐼)〉) ↾
ω)‘suc 𝑏) =
(rec((𝑖 ∈ ω,
𝑣 ∈ V ↦
〈suc 𝑖, (𝑖𝐹𝑣)〉), 〈∅, ( I ‘𝐼)〉)‘suc 𝑏)) |
68 | 21 | fveq1i 6104 |
. . . . . 6
⊢ (𝑄‘suc 𝑏) = (rec((𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc 𝑖, (𝑖𝐹𝑣)〉), 〈∅, ( I ‘𝐼)〉)‘suc 𝑏) |
69 | 67, 68 | syl6eqr 2662 |
. . . . 5
⊢ (𝑏 ∈ ω →
((rec((𝑖 ∈ ω,
𝑣 ∈ V ↦
〈suc 𝑖, (𝑖𝐹𝑣)〉), 〈∅, ( I ‘𝐼)〉) ↾
ω)‘suc 𝑏) =
(𝑄‘suc 𝑏)) |
70 | | fvres 6117 |
. . . . . . 7
⊢ (𝑏 ∈ ω →
((rec((𝑖 ∈ ω,
𝑣 ∈ V ↦
〈suc 𝑖, (𝑖𝐹𝑣)〉), 〈∅, ( I ‘𝐼)〉) ↾
ω)‘𝑏) =
(rec((𝑖 ∈ ω,
𝑣 ∈ V ↦
〈suc 𝑖, (𝑖𝐹𝑣)〉), 〈∅, ( I ‘𝐼)〉)‘𝑏)) |
71 | 21 | fveq1i 6104 |
. . . . . . 7
⊢ (𝑄‘𝑏) = (rec((𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc 𝑖, (𝑖𝐹𝑣)〉), 〈∅, ( I ‘𝐼)〉)‘𝑏) |
72 | 70, 71 | syl6eqr 2662 |
. . . . . 6
⊢ (𝑏 ∈ ω →
((rec((𝑖 ∈ ω,
𝑣 ∈ V ↦
〈suc 𝑖, (𝑖𝐹𝑣)〉), 〈∅, ( I ‘𝐼)〉) ↾
ω)‘𝑏) = (𝑄‘𝑏)) |
73 | 72 | fveq2d 6107 |
. . . . 5
⊢ (𝑏 ∈ ω → ((𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc
𝑖, (𝑖𝐹𝑣)〉)‘((rec((𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc 𝑖, (𝑖𝐹𝑣)〉), 〈∅, ( I ‘𝐼)〉) ↾
ω)‘𝑏)) =
((𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc
𝑖, (𝑖𝐹𝑣)〉)‘(𝑄‘𝑏))) |
74 | 64, 69, 73 | 3eqtr3d 2652 |
. . . 4
⊢ (𝑏 ∈ ω → (𝑄‘suc 𝑏) = ((𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc 𝑖, (𝑖𝐹𝑣)〉)‘(𝑄‘𝑏))) |
75 | 74 | fveq2d 6107 |
. . . . 5
⊢ (𝑏 ∈ ω →
(2nd ‘(𝑄‘suc 𝑏)) = (2nd ‘((𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc
𝑖, (𝑖𝐹𝑣)〉)‘(𝑄‘𝑏)))) |
76 | 75 | opeq2d 4347 |
. . . 4
⊢ (𝑏 ∈ ω → 〈suc
𝑏, (2nd
‘(𝑄‘suc 𝑏))〉 = 〈suc 𝑏, (2nd ‘((𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc
𝑖, (𝑖𝐹𝑣)〉)‘(𝑄‘𝑏)))〉) |
77 | 74, 76 | eqeq12d 2625 |
. . 3
⊢ (𝑏 ∈ ω → ((𝑄‘suc 𝑏) = 〈suc 𝑏, (2nd ‘(𝑄‘suc 𝑏))〉 ↔ ((𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc 𝑖, (𝑖𝐹𝑣)〉)‘(𝑄‘𝑏)) = 〈suc 𝑏, (2nd ‘((𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc 𝑖, (𝑖𝐹𝑣)〉)‘(𝑄‘𝑏)))〉)) |
78 | 63, 77 | sylibrd 248 |
. 2
⊢ (𝑏 ∈ ω → ((𝑄‘𝑏) = 〈𝑏, (2nd ‘(𝑄‘𝑏))〉 → (𝑄‘suc 𝑏) = 〈suc 𝑏, (2nd ‘(𝑄‘suc 𝑏))〉)) |
79 | 5, 10, 15, 20, 35, 78 | finds 6984 |
1
⊢ (𝐴 ∈ ω → (𝑄‘𝐴) = 〈𝐴, (2nd ‘(𝑄‘𝐴))〉) |