| Step | Hyp | Ref
| Expression |
| 1 | | fveq2 6906 |
. . 3
⊢ (𝑧 = ∅ → (𝑅‘𝑧) = (𝑅‘∅)) |
| 2 | | fveq2 6906 |
. . . 4
⊢ (𝑧 = ∅ → (𝐺‘𝑧) = (𝐺‘∅)) |
| 3 | | 2fveq3 6911 |
. . . 4
⊢ (𝑧 = ∅ →
(2nd ‘(𝑅‘𝑧)) = (2nd ‘(𝑅‘∅))) |
| 4 | 2, 3 | opeq12d 4881 |
. . 3
⊢ (𝑧 = ∅ → 〈(𝐺‘𝑧), (2nd ‘(𝑅‘𝑧))〉 = 〈(𝐺‘∅), (2nd
‘(𝑅‘∅))〉) |
| 5 | 1, 4 | eqeq12d 2753 |
. 2
⊢ (𝑧 = ∅ → ((𝑅‘𝑧) = 〈(𝐺‘𝑧), (2nd ‘(𝑅‘𝑧))〉 ↔ (𝑅‘∅) = 〈(𝐺‘∅), (2nd
‘(𝑅‘∅))〉)) |
| 6 | | fveq2 6906 |
. . 3
⊢ (𝑧 = 𝑣 → (𝑅‘𝑧) = (𝑅‘𝑣)) |
| 7 | | fveq2 6906 |
. . . 4
⊢ (𝑧 = 𝑣 → (𝐺‘𝑧) = (𝐺‘𝑣)) |
| 8 | | 2fveq3 6911 |
. . . 4
⊢ (𝑧 = 𝑣 → (2nd ‘(𝑅‘𝑧)) = (2nd ‘(𝑅‘𝑣))) |
| 9 | 7, 8 | opeq12d 4881 |
. . 3
⊢ (𝑧 = 𝑣 → 〈(𝐺‘𝑧), (2nd ‘(𝑅‘𝑧))〉 = 〈(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))〉) |
| 10 | 6, 9 | eqeq12d 2753 |
. 2
⊢ (𝑧 = 𝑣 → ((𝑅‘𝑧) = 〈(𝐺‘𝑧), (2nd ‘(𝑅‘𝑧))〉 ↔ (𝑅‘𝑣) = 〈(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))〉)) |
| 11 | | fveq2 6906 |
. . 3
⊢ (𝑧 = suc 𝑣 → (𝑅‘𝑧) = (𝑅‘suc 𝑣)) |
| 12 | | fveq2 6906 |
. . . 4
⊢ (𝑧 = suc 𝑣 → (𝐺‘𝑧) = (𝐺‘suc 𝑣)) |
| 13 | | 2fveq3 6911 |
. . . 4
⊢ (𝑧 = suc 𝑣 → (2nd ‘(𝑅‘𝑧)) = (2nd ‘(𝑅‘suc 𝑣))) |
| 14 | 12, 13 | opeq12d 4881 |
. . 3
⊢ (𝑧 = suc 𝑣 → 〈(𝐺‘𝑧), (2nd ‘(𝑅‘𝑧))〉 = 〈(𝐺‘suc 𝑣), (2nd ‘(𝑅‘suc 𝑣))〉) |
| 15 | 11, 14 | eqeq12d 2753 |
. 2
⊢ (𝑧 = suc 𝑣 → ((𝑅‘𝑧) = 〈(𝐺‘𝑧), (2nd ‘(𝑅‘𝑧))〉 ↔ (𝑅‘suc 𝑣) = 〈(𝐺‘suc 𝑣), (2nd ‘(𝑅‘suc 𝑣))〉)) |
| 16 | | fveq2 6906 |
. . 3
⊢ (𝑧 = 𝐵 → (𝑅‘𝑧) = (𝑅‘𝐵)) |
| 17 | | fveq2 6906 |
. . . 4
⊢ (𝑧 = 𝐵 → (𝐺‘𝑧) = (𝐺‘𝐵)) |
| 18 | | 2fveq3 6911 |
. . . 4
⊢ (𝑧 = 𝐵 → (2nd ‘(𝑅‘𝑧)) = (2nd ‘(𝑅‘𝐵))) |
| 19 | 17, 18 | opeq12d 4881 |
. . 3
⊢ (𝑧 = 𝐵 → 〈(𝐺‘𝑧), (2nd ‘(𝑅‘𝑧))〉 = 〈(𝐺‘𝐵), (2nd ‘(𝑅‘𝐵))〉) |
| 20 | 16, 19 | eqeq12d 2753 |
. 2
⊢ (𝑧 = 𝐵 → ((𝑅‘𝑧) = 〈(𝐺‘𝑧), (2nd ‘(𝑅‘𝑧))〉 ↔ (𝑅‘𝐵) = 〈(𝐺‘𝐵), (2nd ‘(𝑅‘𝐵))〉)) |
| 21 | | uzrdg.2 |
. . . . 5
⊢ 𝑅 = (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉) ↾ ω) |
| 22 | 21 | fveq1i 6907 |
. . . 4
⊢ (𝑅‘∅) = ((rec((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉) ↾
ω)‘∅) |
| 23 | | opex 5469 |
. . . . 5
⊢
〈𝐶, 𝐴〉 ∈ V |
| 24 | | fr0g 8476 |
. . . . 5
⊢
(〈𝐶, 𝐴〉 ∈ V →
((rec((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉) ↾ ω)‘∅) =
〈𝐶, 𝐴〉) |
| 25 | 23, 24 | ax-mp 5 |
. . . 4
⊢
((rec((𝑥 ∈ V,
𝑦 ∈ V ↦
〈(𝑥 + 1), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉) ↾ ω)‘∅) =
〈𝐶, 𝐴〉 |
| 26 | 22, 25 | eqtri 2765 |
. . 3
⊢ (𝑅‘∅) = 〈𝐶, 𝐴〉 |
| 27 | | om2uz.1 |
. . . . 5
⊢ 𝐶 ∈ ℤ |
| 28 | | om2uz.2 |
. . . . 5
⊢ 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 𝐶) ↾ ω) |
| 29 | 27, 28 | om2uz0i 13988 |
. . . 4
⊢ (𝐺‘∅) = 𝐶 |
| 30 | 26 | fveq2i 6909 |
. . . . 5
⊢
(2nd ‘(𝑅‘∅)) = (2nd
‘〈𝐶, 𝐴〉) |
| 31 | 27 | elexi 3503 |
. . . . . 6
⊢ 𝐶 ∈ V |
| 32 | | uzrdg.1 |
. . . . . 6
⊢ 𝐴 ∈ V |
| 33 | 31, 32 | op2nd 8023 |
. . . . 5
⊢
(2nd ‘〈𝐶, 𝐴〉) = 𝐴 |
| 34 | 30, 33 | eqtri 2765 |
. . . 4
⊢
(2nd ‘(𝑅‘∅)) = 𝐴 |
| 35 | 29, 34 | opeq12i 4878 |
. . 3
⊢
〈(𝐺‘∅), (2nd
‘(𝑅‘∅))〉 = 〈𝐶, 𝐴〉 |
| 36 | 26, 35 | eqtr4i 2768 |
. 2
⊢ (𝑅‘∅) = 〈(𝐺‘∅), (2nd
‘(𝑅‘∅))〉 |
| 37 | | frsuc 8477 |
. . . . . 6
⊢ (𝑣 ∈ ω →
((rec((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉) ↾ ω)‘suc 𝑣) = ((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘((rec((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉) ↾ ω)‘𝑣))) |
| 38 | 21 | fveq1i 6907 |
. . . . . 6
⊢ (𝑅‘suc 𝑣) = ((rec((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉) ↾ ω)‘suc 𝑣) |
| 39 | 21 | fveq1i 6907 |
. . . . . . 7
⊢ (𝑅‘𝑣) = ((rec((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉) ↾ ω)‘𝑣) |
| 40 | 39 | fveq2i 6909 |
. . . . . 6
⊢ ((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘(𝑅‘𝑣)) = ((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘((rec((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉) ↾ ω)‘𝑣)) |
| 41 | 37, 38, 40 | 3eqtr4g 2802 |
. . . . 5
⊢ (𝑣 ∈ ω → (𝑅‘suc 𝑣) = ((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘(𝑅‘𝑣))) |
| 42 | | fveq2 6906 |
. . . . . 6
⊢ ((𝑅‘𝑣) = 〈(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))〉 → ((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘(𝑅‘𝑣)) = ((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘〈(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))〉)) |
| 43 | | df-ov 7434 |
. . . . . . 7
⊢ ((𝐺‘𝑣)(𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)(2nd ‘(𝑅‘𝑣))) = ((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘〈(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))〉) |
| 44 | | fvex 6919 |
. . . . . . . 8
⊢ (𝐺‘𝑣) ∈ V |
| 45 | | fvex 6919 |
. . . . . . . 8
⊢
(2nd ‘(𝑅‘𝑣)) ∈ V |
| 46 | | oveq1 7438 |
. . . . . . . . . 10
⊢ (𝑤 = (𝐺‘𝑣) → (𝑤 + 1) = ((𝐺‘𝑣) + 1)) |
| 47 | | oveq1 7438 |
. . . . . . . . . 10
⊢ (𝑤 = (𝐺‘𝑣) → (𝑤𝐹𝑧) = ((𝐺‘𝑣)𝐹𝑧)) |
| 48 | 46, 47 | opeq12d 4881 |
. . . . . . . . 9
⊢ (𝑤 = (𝐺‘𝑣) → 〈(𝑤 + 1), (𝑤𝐹𝑧)〉 = 〈((𝐺‘𝑣) + 1), ((𝐺‘𝑣)𝐹𝑧)〉) |
| 49 | | oveq2 7439 |
. . . . . . . . . 10
⊢ (𝑧 = (2nd ‘(𝑅‘𝑣)) → ((𝐺‘𝑣)𝐹𝑧) = ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣)))) |
| 50 | 49 | opeq2d 4880 |
. . . . . . . . 9
⊢ (𝑧 = (2nd ‘(𝑅‘𝑣)) → 〈((𝐺‘𝑣) + 1), ((𝐺‘𝑣)𝐹𝑧)〉 = 〈((𝐺‘𝑣) + 1), ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣)))〉) |
| 51 | | oveq1 7438 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑤 → (𝑥 + 1) = (𝑤 + 1)) |
| 52 | | oveq1 7438 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑤 → (𝑥𝐹𝑦) = (𝑤𝐹𝑦)) |
| 53 | 51, 52 | opeq12d 4881 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑤 → 〈(𝑥 + 1), (𝑥𝐹𝑦)〉 = 〈(𝑤 + 1), (𝑤𝐹𝑦)〉) |
| 54 | | oveq2 7439 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑧 → (𝑤𝐹𝑦) = (𝑤𝐹𝑧)) |
| 55 | 54 | opeq2d 4880 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑧 → 〈(𝑤 + 1), (𝑤𝐹𝑦)〉 = 〈(𝑤 + 1), (𝑤𝐹𝑧)〉) |
| 56 | 53, 55 | cbvmpov 7528 |
. . . . . . . . 9
⊢ (𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉) = (𝑤 ∈ V, 𝑧 ∈ V ↦ 〈(𝑤 + 1), (𝑤𝐹𝑧)〉) |
| 57 | | opex 5469 |
. . . . . . . . 9
⊢
〈((𝐺‘𝑣) + 1), ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣)))〉 ∈ V |
| 58 | 48, 50, 56, 57 | ovmpo 7593 |
. . . . . . . 8
⊢ (((𝐺‘𝑣) ∈ V ∧ (2nd
‘(𝑅‘𝑣)) ∈ V) → ((𝐺‘𝑣)(𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)(2nd ‘(𝑅‘𝑣))) = 〈((𝐺‘𝑣) + 1), ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣)))〉) |
| 59 | 44, 45, 58 | mp2an 692 |
. . . . . . 7
⊢ ((𝐺‘𝑣)(𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)(2nd ‘(𝑅‘𝑣))) = 〈((𝐺‘𝑣) + 1), ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣)))〉 |
| 60 | 43, 59 | eqtr3i 2767 |
. . . . . 6
⊢ ((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘〈(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))〉) = 〈((𝐺‘𝑣) + 1), ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣)))〉 |
| 61 | 42, 60 | eqtrdi 2793 |
. . . . 5
⊢ ((𝑅‘𝑣) = 〈(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))〉 → ((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘(𝑅‘𝑣)) = 〈((𝐺‘𝑣) + 1), ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣)))〉) |
| 62 | 41, 61 | sylan9eq 2797 |
. . . 4
⊢ ((𝑣 ∈ ω ∧ (𝑅‘𝑣) = 〈(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))〉) → (𝑅‘suc 𝑣) = 〈((𝐺‘𝑣) + 1), ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣)))〉) |
| 63 | 27, 28 | om2uzsuci 13989 |
. . . . . 6
⊢ (𝑣 ∈ ω → (𝐺‘suc 𝑣) = ((𝐺‘𝑣) + 1)) |
| 64 | 63 | adantr 480 |
. . . . 5
⊢ ((𝑣 ∈ ω ∧ (𝑅‘𝑣) = 〈(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))〉) → (𝐺‘suc 𝑣) = ((𝐺‘𝑣) + 1)) |
| 65 | 62 | fveq2d 6910 |
. . . . . 6
⊢ ((𝑣 ∈ ω ∧ (𝑅‘𝑣) = 〈(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))〉) → (2nd
‘(𝑅‘suc 𝑣)) = (2nd
‘〈((𝐺‘𝑣) + 1), ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣)))〉)) |
| 66 | | ovex 7464 |
. . . . . . 7
⊢ ((𝐺‘𝑣) + 1) ∈ V |
| 67 | | ovex 7464 |
. . . . . . 7
⊢ ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣))) ∈ V |
| 68 | 66, 67 | op2nd 8023 |
. . . . . 6
⊢
(2nd ‘〈((𝐺‘𝑣) + 1), ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣)))〉) = ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣))) |
| 69 | 65, 68 | eqtrdi 2793 |
. . . . 5
⊢ ((𝑣 ∈ ω ∧ (𝑅‘𝑣) = 〈(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))〉) → (2nd
‘(𝑅‘suc 𝑣)) = ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣)))) |
| 70 | 64, 69 | opeq12d 4881 |
. . . 4
⊢ ((𝑣 ∈ ω ∧ (𝑅‘𝑣) = 〈(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))〉) → 〈(𝐺‘suc 𝑣), (2nd ‘(𝑅‘suc 𝑣))〉 = 〈((𝐺‘𝑣) + 1), ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣)))〉) |
| 71 | 62, 70 | eqtr4d 2780 |
. . 3
⊢ ((𝑣 ∈ ω ∧ (𝑅‘𝑣) = 〈(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))〉) → (𝑅‘suc 𝑣) = 〈(𝐺‘suc 𝑣), (2nd ‘(𝑅‘suc 𝑣))〉) |
| 72 | 71 | ex 412 |
. 2
⊢ (𝑣 ∈ ω → ((𝑅‘𝑣) = 〈(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))〉 → (𝑅‘suc 𝑣) = 〈(𝐺‘suc 𝑣), (2nd ‘(𝑅‘suc 𝑣))〉)) |
| 73 | 5, 10, 15, 20, 36, 72 | finds 7918 |
1
⊢ (𝐵 ∈ ω → (𝑅‘𝐵) = 〈(𝐺‘𝐵), (2nd ‘(𝑅‘𝐵))〉) |