Step | Hyp | Ref
| Expression |
1 | | fveq2 6843 |
. . 3
⊢ (𝑎 = ∅ → (𝑄‘𝑎) = (𝑄‘∅)) |
2 | | id 22 |
. . . 4
⊢ (𝑎 = ∅ → 𝑎 = ∅) |
3 | | 2fveq3 6848 |
. . . 4
⊢ (𝑎 = ∅ →
(2nd ‘(𝑄‘𝑎)) = (2nd ‘(𝑄‘∅))) |
4 | 2, 3 | opeq12d 4839 |
. . 3
⊢ (𝑎 = ∅ → ⟨𝑎, (2nd ‘(𝑄‘𝑎))⟩ = ⟨∅, (2nd
‘(𝑄‘∅))⟩) |
5 | 1, 4 | eqeq12d 2753 |
. 2
⊢ (𝑎 = ∅ → ((𝑄‘𝑎) = ⟨𝑎, (2nd ‘(𝑄‘𝑎))⟩ ↔ (𝑄‘∅) = ⟨∅,
(2nd ‘(𝑄‘∅))⟩)) |
6 | | fveq2 6843 |
. . 3
⊢ (𝑎 = 𝑏 → (𝑄‘𝑎) = (𝑄‘𝑏)) |
7 | | id 22 |
. . . 4
⊢ (𝑎 = 𝑏 → 𝑎 = 𝑏) |
8 | | 2fveq3 6848 |
. . . 4
⊢ (𝑎 = 𝑏 → (2nd ‘(𝑄‘𝑎)) = (2nd ‘(𝑄‘𝑏))) |
9 | 7, 8 | opeq12d 4839 |
. . 3
⊢ (𝑎 = 𝑏 → ⟨𝑎, (2nd ‘(𝑄‘𝑎))⟩ = ⟨𝑏, (2nd ‘(𝑄‘𝑏))⟩) |
10 | 6, 9 | eqeq12d 2753 |
. 2
⊢ (𝑎 = 𝑏 → ((𝑄‘𝑎) = ⟨𝑎, (2nd ‘(𝑄‘𝑎))⟩ ↔ (𝑄‘𝑏) = ⟨𝑏, (2nd ‘(𝑄‘𝑏))⟩)) |
11 | | fveq2 6843 |
. . 3
⊢ (𝑎 = suc 𝑏 → (𝑄‘𝑎) = (𝑄‘suc 𝑏)) |
12 | | id 22 |
. . . 4
⊢ (𝑎 = suc 𝑏 → 𝑎 = suc 𝑏) |
13 | | 2fveq3 6848 |
. . . 4
⊢ (𝑎 = suc 𝑏 → (2nd ‘(𝑄‘𝑎)) = (2nd ‘(𝑄‘suc 𝑏))) |
14 | 12, 13 | opeq12d 4839 |
. . 3
⊢ (𝑎 = suc 𝑏 → ⟨𝑎, (2nd ‘(𝑄‘𝑎))⟩ = ⟨suc 𝑏, (2nd ‘(𝑄‘suc 𝑏))⟩) |
15 | 11, 14 | eqeq12d 2753 |
. 2
⊢ (𝑎 = suc 𝑏 → ((𝑄‘𝑎) = ⟨𝑎, (2nd ‘(𝑄‘𝑎))⟩ ↔ (𝑄‘suc 𝑏) = ⟨suc 𝑏, (2nd ‘(𝑄‘suc 𝑏))⟩)) |
16 | | fveq2 6843 |
. . 3
⊢ (𝑎 = 𝐴 → (𝑄‘𝑎) = (𝑄‘𝐴)) |
17 | | id 22 |
. . . 4
⊢ (𝑎 = 𝐴 → 𝑎 = 𝐴) |
18 | | 2fveq3 6848 |
. . . 4
⊢ (𝑎 = 𝐴 → (2nd ‘(𝑄‘𝑎)) = (2nd ‘(𝑄‘𝐴))) |
19 | 17, 18 | opeq12d 4839 |
. . 3
⊢ (𝑎 = 𝐴 → ⟨𝑎, (2nd ‘(𝑄‘𝑎))⟩ = ⟨𝐴, (2nd ‘(𝑄‘𝐴))⟩) |
20 | 16, 19 | eqeq12d 2753 |
. 2
⊢ (𝑎 = 𝐴 → ((𝑄‘𝑎) = ⟨𝑎, (2nd ‘(𝑄‘𝑎))⟩ ↔ (𝑄‘𝐴) = ⟨𝐴, (2nd ‘(𝑄‘𝐴))⟩)) |
21 | | seqomlem.a |
. . . . 5
⊢ 𝑄 = rec((𝑖 ∈ ω, 𝑣 ∈ V ↦ ⟨suc 𝑖, (𝑖𝐹𝑣)⟩), ⟨∅, ( I ‘𝐼)⟩) |
22 | 21 | fveq1i 6844 |
. . . 4
⊢ (𝑄‘∅) = (rec((𝑖 ∈ ω, 𝑣 ∈ V ↦ ⟨suc
𝑖, (𝑖𝐹𝑣)⟩), ⟨∅, ( I ‘𝐼)⟩)‘∅) |
23 | | opex 5422 |
. . . . 5
⊢
⟨∅, ( I ‘𝐼)⟩ ∈ V |
24 | 23 | rdg0 8368 |
. . . 4
⊢
(rec((𝑖 ∈
ω, 𝑣 ∈ V ↦
⟨suc 𝑖, (𝑖𝐹𝑣)⟩), ⟨∅, ( I ‘𝐼)⟩)‘∅) =
⟨∅, ( I ‘𝐼)⟩ |
25 | 22, 24 | eqtri 2765 |
. . 3
⊢ (𝑄‘∅) = ⟨∅,
( I ‘𝐼)⟩ |
26 | | 0ex 5265 |
. . . . . . 7
⊢ ∅
∈ V |
27 | | fvex 6856 |
. . . . . . 7
⊢ ( I
‘𝐼) ∈
V |
28 | 26, 27 | op2nd 7931 |
. . . . . 6
⊢
(2nd ‘⟨∅, ( I ‘𝐼)⟩) = ( I ‘𝐼) |
29 | 28 | eqcomi 2746 |
. . . . 5
⊢ ( I
‘𝐼) = (2nd
‘⟨∅, ( I ‘𝐼)⟩) |
30 | 29 | opeq2i 4835 |
. . . 4
⊢
⟨∅, ( I ‘𝐼)⟩ = ⟨∅, (2nd
‘⟨∅, ( I ‘𝐼)⟩)⟩ |
31 | | id 22 |
. . . 4
⊢ ((𝑄‘∅) = ⟨∅,
( I ‘𝐼)⟩ →
(𝑄‘∅) =
⟨∅, ( I ‘𝐼)⟩) |
32 | | fveq2 6843 |
. . . . 5
⊢ ((𝑄‘∅) = ⟨∅,
( I ‘𝐼)⟩ →
(2nd ‘(𝑄‘∅)) = (2nd
‘⟨∅, ( I ‘𝐼)⟩)) |
33 | 32 | opeq2d 4838 |
. . . 4
⊢ ((𝑄‘∅) = ⟨∅,
( I ‘𝐼)⟩ →
⟨∅, (2nd ‘(𝑄‘∅))⟩ = ⟨∅,
(2nd ‘⟨∅, ( I ‘𝐼)⟩)⟩) |
34 | 30, 31, 33 | 3eqtr4a 2803 |
. . 3
⊢ ((𝑄‘∅) = ⟨∅,
( I ‘𝐼)⟩ →
(𝑄‘∅) =
⟨∅, (2nd ‘(𝑄‘∅))⟩) |
35 | 25, 34 | ax-mp 5 |
. 2
⊢ (𝑄‘∅) = ⟨∅,
(2nd ‘(𝑄‘∅))⟩ |
36 | | df-ov 7361 |
. . . . . 6
⊢ (𝑏(𝑖 ∈ ω, 𝑣 ∈ V ↦ ⟨suc 𝑖, (𝑖𝐹𝑣)⟩)(2nd ‘(𝑄‘𝑏))) = ((𝑖 ∈ ω, 𝑣 ∈ V ↦ ⟨suc 𝑖, (𝑖𝐹𝑣)⟩)‘⟨𝑏, (2nd ‘(𝑄‘𝑏))⟩) |
37 | | fvex 6856 |
. . . . . . 7
⊢
(2nd ‘(𝑄‘𝑏)) ∈ V |
38 | | suceq 6384 |
. . . . . . . . 9
⊢ (𝑖 = 𝑏 → suc 𝑖 = suc 𝑏) |
39 | | oveq1 7365 |
. . . . . . . . 9
⊢ (𝑖 = 𝑏 → (𝑖𝐹𝑣) = (𝑏𝐹𝑣)) |
40 | 38, 39 | opeq12d 4839 |
. . . . . . . 8
⊢ (𝑖 = 𝑏 → ⟨suc 𝑖, (𝑖𝐹𝑣)⟩ = ⟨suc 𝑏, (𝑏𝐹𝑣)⟩) |
41 | | oveq2 7366 |
. . . . . . . . 9
⊢ (𝑣 = (2nd ‘(𝑄‘𝑏)) → (𝑏𝐹𝑣) = (𝑏𝐹(2nd ‘(𝑄‘𝑏)))) |
42 | 41 | opeq2d 4838 |
. . . . . . . 8
⊢ (𝑣 = (2nd ‘(𝑄‘𝑏)) → ⟨suc 𝑏, (𝑏𝐹𝑣)⟩ = ⟨suc 𝑏, (𝑏𝐹(2nd ‘(𝑄‘𝑏)))⟩) |
43 | | eqid 2737 |
. . . . . . . 8
⊢ (𝑖 ∈ ω, 𝑣 ∈ V ↦ ⟨suc
𝑖, (𝑖𝐹𝑣)⟩) = (𝑖 ∈ ω, 𝑣 ∈ V ↦ ⟨suc 𝑖, (𝑖𝐹𝑣)⟩) |
44 | | opex 5422 |
. . . . . . . 8
⊢ ⟨suc
𝑏, (𝑏𝐹(2nd ‘(𝑄‘𝑏)))⟩ ∈ V |
45 | 40, 42, 43, 44 | ovmpo 7516 |
. . . . . . 7
⊢ ((𝑏 ∈ ω ∧
(2nd ‘(𝑄‘𝑏)) ∈ V) → (𝑏(𝑖 ∈ ω, 𝑣 ∈ V ↦ ⟨suc 𝑖, (𝑖𝐹𝑣)⟩)(2nd ‘(𝑄‘𝑏))) = ⟨suc 𝑏, (𝑏𝐹(2nd ‘(𝑄‘𝑏)))⟩) |
46 | 37, 45 | mpan2 690 |
. . . . . 6
⊢ (𝑏 ∈ ω → (𝑏(𝑖 ∈ ω, 𝑣 ∈ V ↦ ⟨suc 𝑖, (𝑖𝐹𝑣)⟩)(2nd ‘(𝑄‘𝑏))) = ⟨suc 𝑏, (𝑏𝐹(2nd ‘(𝑄‘𝑏)))⟩) |
47 | 36, 46 | eqtr3id 2791 |
. . . . 5
⊢ (𝑏 ∈ ω → ((𝑖 ∈ ω, 𝑣 ∈ V ↦ ⟨suc
𝑖, (𝑖𝐹𝑣)⟩)‘⟨𝑏, (2nd ‘(𝑄‘𝑏))⟩) = ⟨suc 𝑏, (𝑏𝐹(2nd ‘(𝑄‘𝑏)))⟩) |
48 | | fveqeq2 6852 |
. . . . 5
⊢ ((𝑄‘𝑏) = ⟨𝑏, (2nd ‘(𝑄‘𝑏))⟩ → (((𝑖 ∈ ω, 𝑣 ∈ V ↦ ⟨suc 𝑖, (𝑖𝐹𝑣)⟩)‘(𝑄‘𝑏)) = ⟨suc 𝑏, (𝑏𝐹(2nd ‘(𝑄‘𝑏)))⟩ ↔ ((𝑖 ∈ ω, 𝑣 ∈ V ↦ ⟨suc 𝑖, (𝑖𝐹𝑣)⟩)‘⟨𝑏, (2nd ‘(𝑄‘𝑏))⟩) = ⟨suc 𝑏, (𝑏𝐹(2nd ‘(𝑄‘𝑏)))⟩)) |
49 | 47, 48 | syl5ibrcom 247 |
. . . 4
⊢ (𝑏 ∈ ω → ((𝑄‘𝑏) = ⟨𝑏, (2nd ‘(𝑄‘𝑏))⟩ → ((𝑖 ∈ ω, 𝑣 ∈ V ↦ ⟨suc 𝑖, (𝑖𝐹𝑣)⟩)‘(𝑄‘𝑏)) = ⟨suc 𝑏, (𝑏𝐹(2nd ‘(𝑄‘𝑏)))⟩)) |
50 | | vex 3450 |
. . . . . . . . . 10
⊢ 𝑏 ∈ V |
51 | 50 | sucex 7742 |
. . . . . . . . 9
⊢ suc 𝑏 ∈ V |
52 | | ovex 7391 |
. . . . . . . . 9
⊢ (𝑏𝐹(2nd ‘(𝑄‘𝑏))) ∈ V |
53 | 51, 52 | op2nd 7931 |
. . . . . . . 8
⊢
(2nd ‘⟨suc 𝑏, (𝑏𝐹(2nd ‘(𝑄‘𝑏)))⟩) = (𝑏𝐹(2nd ‘(𝑄‘𝑏))) |
54 | 53 | eqcomi 2746 |
. . . . . . 7
⊢ (𝑏𝐹(2nd ‘(𝑄‘𝑏))) = (2nd ‘⟨suc 𝑏, (𝑏𝐹(2nd ‘(𝑄‘𝑏)))⟩) |
55 | 54 | a1i 11 |
. . . . . 6
⊢ (𝑏 ∈ ω → (𝑏𝐹(2nd ‘(𝑄‘𝑏))) = (2nd ‘⟨suc 𝑏, (𝑏𝐹(2nd ‘(𝑄‘𝑏)))⟩)) |
56 | 55 | opeq2d 4838 |
. . . . 5
⊢ (𝑏 ∈ ω → ⟨suc
𝑏, (𝑏𝐹(2nd ‘(𝑄‘𝑏)))⟩ = ⟨suc 𝑏, (2nd ‘⟨suc 𝑏, (𝑏𝐹(2nd ‘(𝑄‘𝑏)))⟩)⟩) |
57 | | id 22 |
. . . . . 6
⊢ (((𝑖 ∈ ω, 𝑣 ∈ V ↦ ⟨suc
𝑖, (𝑖𝐹𝑣)⟩)‘(𝑄‘𝑏)) = ⟨suc 𝑏, (𝑏𝐹(2nd ‘(𝑄‘𝑏)))⟩ → ((𝑖 ∈ ω, 𝑣 ∈ V ↦ ⟨suc 𝑖, (𝑖𝐹𝑣)⟩)‘(𝑄‘𝑏)) = ⟨suc 𝑏, (𝑏𝐹(2nd ‘(𝑄‘𝑏)))⟩) |
58 | | fveq2 6843 |
. . . . . . 7
⊢ (((𝑖 ∈ ω, 𝑣 ∈ V ↦ ⟨suc
𝑖, (𝑖𝐹𝑣)⟩)‘(𝑄‘𝑏)) = ⟨suc 𝑏, (𝑏𝐹(2nd ‘(𝑄‘𝑏)))⟩ → (2nd
‘((𝑖 ∈ ω,
𝑣 ∈ V ↦
⟨suc 𝑖, (𝑖𝐹𝑣)⟩)‘(𝑄‘𝑏))) = (2nd ‘⟨suc 𝑏, (𝑏𝐹(2nd ‘(𝑄‘𝑏)))⟩)) |
59 | 58 | opeq2d 4838 |
. . . . . 6
⊢ (((𝑖 ∈ ω, 𝑣 ∈ V ↦ ⟨suc
𝑖, (𝑖𝐹𝑣)⟩)‘(𝑄‘𝑏)) = ⟨suc 𝑏, (𝑏𝐹(2nd ‘(𝑄‘𝑏)))⟩ → ⟨suc 𝑏, (2nd ‘((𝑖 ∈ ω, 𝑣 ∈ V ↦ ⟨suc 𝑖, (𝑖𝐹𝑣)⟩)‘(𝑄‘𝑏)))⟩ = ⟨suc 𝑏, (2nd ‘⟨suc 𝑏, (𝑏𝐹(2nd ‘(𝑄‘𝑏)))⟩)⟩) |
60 | 57, 59 | eqeq12d 2753 |
. . . . 5
⊢ (((𝑖 ∈ ω, 𝑣 ∈ V ↦ ⟨suc
𝑖, (𝑖𝐹𝑣)⟩)‘(𝑄‘𝑏)) = ⟨suc 𝑏, (𝑏𝐹(2nd ‘(𝑄‘𝑏)))⟩ → (((𝑖 ∈ ω, 𝑣 ∈ V ↦ ⟨suc 𝑖, (𝑖𝐹𝑣)⟩)‘(𝑄‘𝑏)) = ⟨suc 𝑏, (2nd ‘((𝑖 ∈ ω, 𝑣 ∈ V ↦ ⟨suc 𝑖, (𝑖𝐹𝑣)⟩)‘(𝑄‘𝑏)))⟩ ↔ ⟨suc 𝑏, (𝑏𝐹(2nd ‘(𝑄‘𝑏)))⟩ = ⟨suc 𝑏, (2nd ‘⟨suc 𝑏, (𝑏𝐹(2nd ‘(𝑄‘𝑏)))⟩)⟩)) |
61 | 56, 60 | syl5ibrcom 247 |
. . . 4
⊢ (𝑏 ∈ ω → (((𝑖 ∈ ω, 𝑣 ∈ V ↦ ⟨suc
𝑖, (𝑖𝐹𝑣)⟩)‘(𝑄‘𝑏)) = ⟨suc 𝑏, (𝑏𝐹(2nd ‘(𝑄‘𝑏)))⟩ → ((𝑖 ∈ ω, 𝑣 ∈ V ↦ ⟨suc 𝑖, (𝑖𝐹𝑣)⟩)‘(𝑄‘𝑏)) = ⟨suc 𝑏, (2nd ‘((𝑖 ∈ ω, 𝑣 ∈ V ↦ ⟨suc 𝑖, (𝑖𝐹𝑣)⟩)‘(𝑄‘𝑏)))⟩)) |
62 | 49, 61 | syld 47 |
. . 3
⊢ (𝑏 ∈ ω → ((𝑄‘𝑏) = ⟨𝑏, (2nd ‘(𝑄‘𝑏))⟩ → ((𝑖 ∈ ω, 𝑣 ∈ V ↦ ⟨suc 𝑖, (𝑖𝐹𝑣)⟩)‘(𝑄‘𝑏)) = ⟨suc 𝑏, (2nd ‘((𝑖 ∈ ω, 𝑣 ∈ V ↦ ⟨suc 𝑖, (𝑖𝐹𝑣)⟩)‘(𝑄‘𝑏)))⟩)) |
63 | | frsuc 8384 |
. . . . 5
⊢ (𝑏 ∈ ω →
((rec((𝑖 ∈ ω,
𝑣 ∈ V ↦
⟨suc 𝑖, (𝑖𝐹𝑣)⟩), ⟨∅, ( I ‘𝐼)⟩) ↾
ω)‘suc 𝑏) =
((𝑖 ∈ ω, 𝑣 ∈ V ↦ ⟨suc
𝑖, (𝑖𝐹𝑣)⟩)‘((rec((𝑖 ∈ ω, 𝑣 ∈ V ↦ ⟨suc 𝑖, (𝑖𝐹𝑣)⟩), ⟨∅, ( I ‘𝐼)⟩) ↾
ω)‘𝑏))) |
64 | | peano2 7828 |
. . . . . . 7
⊢ (𝑏 ∈ ω → suc 𝑏 ∈
ω) |
65 | 64 | fvresd 6863 |
. . . . . 6
⊢ (𝑏 ∈ ω →
((rec((𝑖 ∈ ω,
𝑣 ∈ V ↦
⟨suc 𝑖, (𝑖𝐹𝑣)⟩), ⟨∅, ( I ‘𝐼)⟩) ↾
ω)‘suc 𝑏) =
(rec((𝑖 ∈ ω,
𝑣 ∈ V ↦
⟨suc 𝑖, (𝑖𝐹𝑣)⟩), ⟨∅, ( I ‘𝐼)⟩)‘suc 𝑏)) |
66 | 21 | fveq1i 6844 |
. . . . . 6
⊢ (𝑄‘suc 𝑏) = (rec((𝑖 ∈ ω, 𝑣 ∈ V ↦ ⟨suc 𝑖, (𝑖𝐹𝑣)⟩), ⟨∅, ( I ‘𝐼)⟩)‘suc 𝑏) |
67 | 65, 66 | eqtr4di 2795 |
. . . . 5
⊢ (𝑏 ∈ ω →
((rec((𝑖 ∈ ω,
𝑣 ∈ V ↦
⟨suc 𝑖, (𝑖𝐹𝑣)⟩), ⟨∅, ( I ‘𝐼)⟩) ↾
ω)‘suc 𝑏) =
(𝑄‘suc 𝑏)) |
68 | | fvres 6862 |
. . . . . . 7
⊢ (𝑏 ∈ ω →
((rec((𝑖 ∈ ω,
𝑣 ∈ V ↦
⟨suc 𝑖, (𝑖𝐹𝑣)⟩), ⟨∅, ( I ‘𝐼)⟩) ↾
ω)‘𝑏) =
(rec((𝑖 ∈ ω,
𝑣 ∈ V ↦
⟨suc 𝑖, (𝑖𝐹𝑣)⟩), ⟨∅, ( I ‘𝐼)⟩)‘𝑏)) |
69 | 21 | fveq1i 6844 |
. . . . . . 7
⊢ (𝑄‘𝑏) = (rec((𝑖 ∈ ω, 𝑣 ∈ V ↦ ⟨suc 𝑖, (𝑖𝐹𝑣)⟩), ⟨∅, ( I ‘𝐼)⟩)‘𝑏) |
70 | 68, 69 | eqtr4di 2795 |
. . . . . 6
⊢ (𝑏 ∈ ω →
((rec((𝑖 ∈ ω,
𝑣 ∈ V ↦
⟨suc 𝑖, (𝑖𝐹𝑣)⟩), ⟨∅, ( I ‘𝐼)⟩) ↾
ω)‘𝑏) = (𝑄‘𝑏)) |
71 | 70 | fveq2d 6847 |
. . . . 5
⊢ (𝑏 ∈ ω → ((𝑖 ∈ ω, 𝑣 ∈ V ↦ ⟨suc
𝑖, (𝑖𝐹𝑣)⟩)‘((rec((𝑖 ∈ ω, 𝑣 ∈ V ↦ ⟨suc 𝑖, (𝑖𝐹𝑣)⟩), ⟨∅, ( I ‘𝐼)⟩) ↾
ω)‘𝑏)) =
((𝑖 ∈ ω, 𝑣 ∈ V ↦ ⟨suc
𝑖, (𝑖𝐹𝑣)⟩)‘(𝑄‘𝑏))) |
72 | 63, 67, 71 | 3eqtr3d 2785 |
. . . 4
⊢ (𝑏 ∈ ω → (𝑄‘suc 𝑏) = ((𝑖 ∈ ω, 𝑣 ∈ V ↦ ⟨suc 𝑖, (𝑖𝐹𝑣)⟩)‘(𝑄‘𝑏))) |
73 | 72 | fveq2d 6847 |
. . . . 5
⊢ (𝑏 ∈ ω →
(2nd ‘(𝑄‘suc 𝑏)) = (2nd ‘((𝑖 ∈ ω, 𝑣 ∈ V ↦ ⟨suc
𝑖, (𝑖𝐹𝑣)⟩)‘(𝑄‘𝑏)))) |
74 | 73 | opeq2d 4838 |
. . . 4
⊢ (𝑏 ∈ ω → ⟨suc
𝑏, (2nd
‘(𝑄‘suc 𝑏))⟩ = ⟨suc 𝑏, (2nd ‘((𝑖 ∈ ω, 𝑣 ∈ V ↦ ⟨suc
𝑖, (𝑖𝐹𝑣)⟩)‘(𝑄‘𝑏)))⟩) |
75 | 72, 74 | eqeq12d 2753 |
. . 3
⊢ (𝑏 ∈ ω → ((𝑄‘suc 𝑏) = ⟨suc 𝑏, (2nd ‘(𝑄‘suc 𝑏))⟩ ↔ ((𝑖 ∈ ω, 𝑣 ∈ V ↦ ⟨suc 𝑖, (𝑖𝐹𝑣)⟩)‘(𝑄‘𝑏)) = ⟨suc 𝑏, (2nd ‘((𝑖 ∈ ω, 𝑣 ∈ V ↦ ⟨suc 𝑖, (𝑖𝐹𝑣)⟩)‘(𝑄‘𝑏)))⟩)) |
76 | 62, 75 | sylibrd 259 |
. 2
⊢ (𝑏 ∈ ω → ((𝑄‘𝑏) = ⟨𝑏, (2nd ‘(𝑄‘𝑏))⟩ → (𝑄‘suc 𝑏) = ⟨suc 𝑏, (2nd ‘(𝑄‘suc 𝑏))⟩)) |
77 | 5, 10, 15, 20, 35, 76 | finds 7836 |
1
⊢ (𝐴 ∈ ω → (𝑄‘𝐴) = ⟨𝐴, (2nd ‘(𝑄‘𝐴))⟩) |