Step | Hyp | Ref
| Expression |
1 | | fveq2 6891 |
. . 3
⊢ (𝑧 = ∅ → (𝑅‘𝑧) = (𝑅‘∅)) |
2 | | fveq2 6891 |
. . . 4
⊢ (𝑧 = ∅ → (𝐺‘𝑧) = (𝐺‘∅)) |
3 | | 2fveq3 6896 |
. . . 4
⊢ (𝑧 = ∅ →
(2nd ‘(𝑅‘𝑧)) = (2nd ‘(𝑅‘∅))) |
4 | 2, 3 | opeq12d 4881 |
. . 3
⊢ (𝑧 = ∅ → ⟨(𝐺‘𝑧), (2nd ‘(𝑅‘𝑧))⟩ = ⟨(𝐺‘∅), (2nd
‘(𝑅‘∅))⟩) |
5 | 1, 4 | eqeq12d 2748 |
. 2
⊢ (𝑧 = ∅ → ((𝑅‘𝑧) = ⟨(𝐺‘𝑧), (2nd ‘(𝑅‘𝑧))⟩ ↔ (𝑅‘∅) = ⟨(𝐺‘∅), (2nd
‘(𝑅‘∅))⟩)) |
6 | | fveq2 6891 |
. . 3
⊢ (𝑧 = 𝑣 → (𝑅‘𝑧) = (𝑅‘𝑣)) |
7 | | fveq2 6891 |
. . . 4
⊢ (𝑧 = 𝑣 → (𝐺‘𝑧) = (𝐺‘𝑣)) |
8 | | 2fveq3 6896 |
. . . 4
⊢ (𝑧 = 𝑣 → (2nd ‘(𝑅‘𝑧)) = (2nd ‘(𝑅‘𝑣))) |
9 | 7, 8 | opeq12d 4881 |
. . 3
⊢ (𝑧 = 𝑣 → ⟨(𝐺‘𝑧), (2nd ‘(𝑅‘𝑧))⟩ = ⟨(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))⟩) |
10 | 6, 9 | eqeq12d 2748 |
. 2
⊢ (𝑧 = 𝑣 → ((𝑅‘𝑧) = ⟨(𝐺‘𝑧), (2nd ‘(𝑅‘𝑧))⟩ ↔ (𝑅‘𝑣) = ⟨(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))⟩)) |
11 | | fveq2 6891 |
. . 3
⊢ (𝑧 = suc 𝑣 → (𝑅‘𝑧) = (𝑅‘suc 𝑣)) |
12 | | fveq2 6891 |
. . . 4
⊢ (𝑧 = suc 𝑣 → (𝐺‘𝑧) = (𝐺‘suc 𝑣)) |
13 | | 2fveq3 6896 |
. . . 4
⊢ (𝑧 = suc 𝑣 → (2nd ‘(𝑅‘𝑧)) = (2nd ‘(𝑅‘suc 𝑣))) |
14 | 12, 13 | opeq12d 4881 |
. . 3
⊢ (𝑧 = suc 𝑣 → ⟨(𝐺‘𝑧), (2nd ‘(𝑅‘𝑧))⟩ = ⟨(𝐺‘suc 𝑣), (2nd ‘(𝑅‘suc 𝑣))⟩) |
15 | 11, 14 | eqeq12d 2748 |
. 2
⊢ (𝑧 = suc 𝑣 → ((𝑅‘𝑧) = ⟨(𝐺‘𝑧), (2nd ‘(𝑅‘𝑧))⟩ ↔ (𝑅‘suc 𝑣) = ⟨(𝐺‘suc 𝑣), (2nd ‘(𝑅‘suc 𝑣))⟩)) |
16 | | fveq2 6891 |
. . 3
⊢ (𝑧 = 𝐵 → (𝑅‘𝑧) = (𝑅‘𝐵)) |
17 | | fveq2 6891 |
. . . 4
⊢ (𝑧 = 𝐵 → (𝐺‘𝑧) = (𝐺‘𝐵)) |
18 | | 2fveq3 6896 |
. . . 4
⊢ (𝑧 = 𝐵 → (2nd ‘(𝑅‘𝑧)) = (2nd ‘(𝑅‘𝐵))) |
19 | 17, 18 | opeq12d 4881 |
. . 3
⊢ (𝑧 = 𝐵 → ⟨(𝐺‘𝑧), (2nd ‘(𝑅‘𝑧))⟩ = ⟨(𝐺‘𝐵), (2nd ‘(𝑅‘𝐵))⟩) |
20 | 16, 19 | eqeq12d 2748 |
. 2
⊢ (𝑧 = 𝐵 → ((𝑅‘𝑧) = ⟨(𝐺‘𝑧), (2nd ‘(𝑅‘𝑧))⟩ ↔ (𝑅‘𝐵) = ⟨(𝐺‘𝐵), (2nd ‘(𝑅‘𝐵))⟩)) |
21 | | uzrdg.2 |
. . . . 5
⊢ 𝑅 = (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩), ⟨𝐶, 𝐴⟩) ↾ ω) |
22 | 21 | fveq1i 6892 |
. . . 4
⊢ (𝑅‘∅) = ((rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩), ⟨𝐶, 𝐴⟩) ↾
ω)‘∅) |
23 | | opex 5464 |
. . . . 5
⊢
⟨𝐶, 𝐴⟩ ∈ V |
24 | | fr0g 8438 |
. . . . 5
⊢
(⟨𝐶, 𝐴⟩ ∈ V →
((rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩), ⟨𝐶, 𝐴⟩) ↾ ω)‘∅) =
⟨𝐶, 𝐴⟩) |
25 | 23, 24 | ax-mp 5 |
. . . 4
⊢
((rec((𝑥 ∈ V,
𝑦 ∈ V ↦
⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩), ⟨𝐶, 𝐴⟩) ↾ ω)‘∅) =
⟨𝐶, 𝐴⟩ |
26 | 22, 25 | eqtri 2760 |
. . 3
⊢ (𝑅‘∅) = ⟨𝐶, 𝐴⟩ |
27 | | om2uz.1 |
. . . . 5
⊢ 𝐶 ∈ ℤ |
28 | | om2uz.2 |
. . . . 5
⊢ 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 𝐶) ↾ ω) |
29 | 27, 28 | om2uz0i 13914 |
. . . 4
⊢ (𝐺‘∅) = 𝐶 |
30 | 26 | fveq2i 6894 |
. . . . 5
⊢
(2nd ‘(𝑅‘∅)) = (2nd
‘⟨𝐶, 𝐴⟩) |
31 | 27 | elexi 3493 |
. . . . . 6
⊢ 𝐶 ∈ V |
32 | | uzrdg.1 |
. . . . . 6
⊢ 𝐴 ∈ V |
33 | 31, 32 | op2nd 7986 |
. . . . 5
⊢
(2nd ‘⟨𝐶, 𝐴⟩) = 𝐴 |
34 | 30, 33 | eqtri 2760 |
. . . 4
⊢
(2nd ‘(𝑅‘∅)) = 𝐴 |
35 | 29, 34 | opeq12i 4878 |
. . 3
⊢
⟨(𝐺‘∅), (2nd
‘(𝑅‘∅))⟩ = ⟨𝐶, 𝐴⟩ |
36 | 26, 35 | eqtr4i 2763 |
. 2
⊢ (𝑅‘∅) = ⟨(𝐺‘∅), (2nd
‘(𝑅‘∅))⟩ |
37 | | frsuc 8439 |
. . . . . 6
⊢ (𝑣 ∈ ω →
((rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩), ⟨𝐶, 𝐴⟩) ↾ ω)‘suc 𝑣) = ((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩)‘((rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩), ⟨𝐶, 𝐴⟩) ↾ ω)‘𝑣))) |
38 | 21 | fveq1i 6892 |
. . . . . 6
⊢ (𝑅‘suc 𝑣) = ((rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩), ⟨𝐶, 𝐴⟩) ↾ ω)‘suc 𝑣) |
39 | 21 | fveq1i 6892 |
. . . . . . 7
⊢ (𝑅‘𝑣) = ((rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩), ⟨𝐶, 𝐴⟩) ↾ ω)‘𝑣) |
40 | 39 | fveq2i 6894 |
. . . . . 6
⊢ ((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩)‘(𝑅‘𝑣)) = ((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩)‘((rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩), ⟨𝐶, 𝐴⟩) ↾ ω)‘𝑣)) |
41 | 37, 38, 40 | 3eqtr4g 2797 |
. . . . 5
⊢ (𝑣 ∈ ω → (𝑅‘suc 𝑣) = ((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩)‘(𝑅‘𝑣))) |
42 | | fveq2 6891 |
. . . . . 6
⊢ ((𝑅‘𝑣) = ⟨(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))⟩ → ((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩)‘(𝑅‘𝑣)) = ((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩)‘⟨(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))⟩)) |
43 | | df-ov 7414 |
. . . . . . 7
⊢ ((𝐺‘𝑣)(𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩)(2nd ‘(𝑅‘𝑣))) = ((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩)‘⟨(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))⟩) |
44 | | fvex 6904 |
. . . . . . . 8
⊢ (𝐺‘𝑣) ∈ V |
45 | | fvex 6904 |
. . . . . . . 8
⊢
(2nd ‘(𝑅‘𝑣)) ∈ V |
46 | | oveq1 7418 |
. . . . . . . . . 10
⊢ (𝑤 = (𝐺‘𝑣) → (𝑤 + 1) = ((𝐺‘𝑣) + 1)) |
47 | | oveq1 7418 |
. . . . . . . . . 10
⊢ (𝑤 = (𝐺‘𝑣) → (𝑤𝐹𝑧) = ((𝐺‘𝑣)𝐹𝑧)) |
48 | 46, 47 | opeq12d 4881 |
. . . . . . . . 9
⊢ (𝑤 = (𝐺‘𝑣) → ⟨(𝑤 + 1), (𝑤𝐹𝑧)⟩ = ⟨((𝐺‘𝑣) + 1), ((𝐺‘𝑣)𝐹𝑧)⟩) |
49 | | oveq2 7419 |
. . . . . . . . . 10
⊢ (𝑧 = (2nd ‘(𝑅‘𝑣)) → ((𝐺‘𝑣)𝐹𝑧) = ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣)))) |
50 | 49 | opeq2d 4880 |
. . . . . . . . 9
⊢ (𝑧 = (2nd ‘(𝑅‘𝑣)) → ⟨((𝐺‘𝑣) + 1), ((𝐺‘𝑣)𝐹𝑧)⟩ = ⟨((𝐺‘𝑣) + 1), ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣)))⟩) |
51 | | oveq1 7418 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑤 → (𝑥 + 1) = (𝑤 + 1)) |
52 | | oveq1 7418 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑤 → (𝑥𝐹𝑦) = (𝑤𝐹𝑦)) |
53 | 51, 52 | opeq12d 4881 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑤 → ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩ = ⟨(𝑤 + 1), (𝑤𝐹𝑦)⟩) |
54 | | oveq2 7419 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑧 → (𝑤𝐹𝑦) = (𝑤𝐹𝑧)) |
55 | 54 | opeq2d 4880 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑧 → ⟨(𝑤 + 1), (𝑤𝐹𝑦)⟩ = ⟨(𝑤 + 1), (𝑤𝐹𝑧)⟩) |
56 | 53, 55 | cbvmpov 7506 |
. . . . . . . . 9
⊢ (𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩) = (𝑤 ∈ V, 𝑧 ∈ V ↦ ⟨(𝑤 + 1), (𝑤𝐹𝑧)⟩) |
57 | | opex 5464 |
. . . . . . . . 9
⊢
⟨((𝐺‘𝑣) + 1), ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣)))⟩ ∈ V |
58 | 48, 50, 56, 57 | ovmpo 7570 |
. . . . . . . 8
⊢ (((𝐺‘𝑣) ∈ V ∧ (2nd
‘(𝑅‘𝑣)) ∈ V) → ((𝐺‘𝑣)(𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩)(2nd ‘(𝑅‘𝑣))) = ⟨((𝐺‘𝑣) + 1), ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣)))⟩) |
59 | 44, 45, 58 | mp2an 690 |
. . . . . . 7
⊢ ((𝐺‘𝑣)(𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩)(2nd ‘(𝑅‘𝑣))) = ⟨((𝐺‘𝑣) + 1), ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣)))⟩ |
60 | 43, 59 | eqtr3i 2762 |
. . . . . 6
⊢ ((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩)‘⟨(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))⟩) = ⟨((𝐺‘𝑣) + 1), ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣)))⟩ |
61 | 42, 60 | eqtrdi 2788 |
. . . . 5
⊢ ((𝑅‘𝑣) = ⟨(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))⟩ → ((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩)‘(𝑅‘𝑣)) = ⟨((𝐺‘𝑣) + 1), ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣)))⟩) |
62 | 41, 61 | sylan9eq 2792 |
. . . 4
⊢ ((𝑣 ∈ ω ∧ (𝑅‘𝑣) = ⟨(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))⟩) → (𝑅‘suc 𝑣) = ⟨((𝐺‘𝑣) + 1), ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣)))⟩) |
63 | 27, 28 | om2uzsuci 13915 |
. . . . . 6
⊢ (𝑣 ∈ ω → (𝐺‘suc 𝑣) = ((𝐺‘𝑣) + 1)) |
64 | 63 | adantr 481 |
. . . . 5
⊢ ((𝑣 ∈ ω ∧ (𝑅‘𝑣) = ⟨(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))⟩) → (𝐺‘suc 𝑣) = ((𝐺‘𝑣) + 1)) |
65 | 62 | fveq2d 6895 |
. . . . . 6
⊢ ((𝑣 ∈ ω ∧ (𝑅‘𝑣) = ⟨(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))⟩) → (2nd
‘(𝑅‘suc 𝑣)) = (2nd
‘⟨((𝐺‘𝑣) + 1), ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣)))⟩)) |
66 | | ovex 7444 |
. . . . . . 7
⊢ ((𝐺‘𝑣) + 1) ∈ V |
67 | | ovex 7444 |
. . . . . . 7
⊢ ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣))) ∈ V |
68 | 66, 67 | op2nd 7986 |
. . . . . 6
⊢
(2nd ‘⟨((𝐺‘𝑣) + 1), ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣)))⟩) = ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣))) |
69 | 65, 68 | eqtrdi 2788 |
. . . . 5
⊢ ((𝑣 ∈ ω ∧ (𝑅‘𝑣) = ⟨(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))⟩) → (2nd
‘(𝑅‘suc 𝑣)) = ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣)))) |
70 | 64, 69 | opeq12d 4881 |
. . . 4
⊢ ((𝑣 ∈ ω ∧ (𝑅‘𝑣) = ⟨(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))⟩) → ⟨(𝐺‘suc 𝑣), (2nd ‘(𝑅‘suc 𝑣))⟩ = ⟨((𝐺‘𝑣) + 1), ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣)))⟩) |
71 | 62, 70 | eqtr4d 2775 |
. . 3
⊢ ((𝑣 ∈ ω ∧ (𝑅‘𝑣) = ⟨(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))⟩) → (𝑅‘suc 𝑣) = ⟨(𝐺‘suc 𝑣), (2nd ‘(𝑅‘suc 𝑣))⟩) |
72 | 71 | ex 413 |
. 2
⊢ (𝑣 ∈ ω → ((𝑅‘𝑣) = ⟨(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))⟩ → (𝑅‘suc 𝑣) = ⟨(𝐺‘suc 𝑣), (2nd ‘(𝑅‘suc 𝑣))⟩)) |
73 | 5, 10, 15, 20, 36, 72 | finds 7891 |
1
⊢ (𝐵 ∈ ω → (𝑅‘𝐵) = ⟨(𝐺‘𝐵), (2nd ‘(𝑅‘𝐵))⟩) |