| Step | Hyp | Ref
| Expression |
| 1 | | fveq2 6906 |
. . . . 5
⊢ (𝑧 = ∅ → (𝑅‘𝑧) = (𝑅‘∅)) |
| 2 | | fveq2 6906 |
. . . . . 6
⊢ (𝑧 = ∅ → (𝐺‘𝑧) = (𝐺‘∅)) |
| 3 | | 2fveq3 6911 |
. . . . . 6
⊢ (𝑧 = ∅ →
(2nd ‘(𝑅‘𝑧)) = (2nd ‘(𝑅‘∅))) |
| 4 | 2, 3 | opeq12d 4881 |
. . . . 5
⊢ (𝑧 = ∅ → 〈(𝐺‘𝑧), (2nd ‘(𝑅‘𝑧))〉 = 〈(𝐺‘∅), (2nd
‘(𝑅‘∅))〉) |
| 5 | 1, 4 | eqeq12d 2753 |
. . . 4
⊢ (𝑧 = ∅ → ((𝑅‘𝑧) = 〈(𝐺‘𝑧), (2nd ‘(𝑅‘𝑧))〉 ↔ (𝑅‘∅) = 〈(𝐺‘∅), (2nd
‘(𝑅‘∅))〉)) |
| 6 | 5 | imbi2d 340 |
. . 3
⊢ (𝑧 = ∅ → ((𝜑 → (𝑅‘𝑧) = 〈(𝐺‘𝑧), (2nd ‘(𝑅‘𝑧))〉) ↔ (𝜑 → (𝑅‘∅) = 〈(𝐺‘∅), (2nd
‘(𝑅‘∅))〉))) |
| 7 | | fveq2 6906 |
. . . . 5
⊢ (𝑧 = 𝑣 → (𝑅‘𝑧) = (𝑅‘𝑣)) |
| 8 | | fveq2 6906 |
. . . . . 6
⊢ (𝑧 = 𝑣 → (𝐺‘𝑧) = (𝐺‘𝑣)) |
| 9 | | 2fveq3 6911 |
. . . . . 6
⊢ (𝑧 = 𝑣 → (2nd ‘(𝑅‘𝑧)) = (2nd ‘(𝑅‘𝑣))) |
| 10 | 8, 9 | opeq12d 4881 |
. . . . 5
⊢ (𝑧 = 𝑣 → 〈(𝐺‘𝑧), (2nd ‘(𝑅‘𝑧))〉 = 〈(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))〉) |
| 11 | 7, 10 | eqeq12d 2753 |
. . . 4
⊢ (𝑧 = 𝑣 → ((𝑅‘𝑧) = 〈(𝐺‘𝑧), (2nd ‘(𝑅‘𝑧))〉 ↔ (𝑅‘𝑣) = 〈(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))〉)) |
| 12 | 11 | imbi2d 340 |
. . 3
⊢ (𝑧 = 𝑣 → ((𝜑 → (𝑅‘𝑧) = 〈(𝐺‘𝑧), (2nd ‘(𝑅‘𝑧))〉) ↔ (𝜑 → (𝑅‘𝑣) = 〈(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))〉))) |
| 13 | | fveq2 6906 |
. . . . 5
⊢ (𝑧 = suc 𝑣 → (𝑅‘𝑧) = (𝑅‘suc 𝑣)) |
| 14 | | fveq2 6906 |
. . . . . 6
⊢ (𝑧 = suc 𝑣 → (𝐺‘𝑧) = (𝐺‘suc 𝑣)) |
| 15 | | 2fveq3 6911 |
. . . . . 6
⊢ (𝑧 = suc 𝑣 → (2nd ‘(𝑅‘𝑧)) = (2nd ‘(𝑅‘suc 𝑣))) |
| 16 | 14, 15 | opeq12d 4881 |
. . . . 5
⊢ (𝑧 = suc 𝑣 → 〈(𝐺‘𝑧), (2nd ‘(𝑅‘𝑧))〉 = 〈(𝐺‘suc 𝑣), (2nd ‘(𝑅‘suc 𝑣))〉) |
| 17 | 13, 16 | eqeq12d 2753 |
. . . 4
⊢ (𝑧 = suc 𝑣 → ((𝑅‘𝑧) = 〈(𝐺‘𝑧), (2nd ‘(𝑅‘𝑧))〉 ↔ (𝑅‘suc 𝑣) = 〈(𝐺‘suc 𝑣), (2nd ‘(𝑅‘suc 𝑣))〉)) |
| 18 | 17 | imbi2d 340 |
. . 3
⊢ (𝑧 = suc 𝑣 → ((𝜑 → (𝑅‘𝑧) = 〈(𝐺‘𝑧), (2nd ‘(𝑅‘𝑧))〉) ↔ (𝜑 → (𝑅‘suc 𝑣) = 〈(𝐺‘suc 𝑣), (2nd ‘(𝑅‘suc 𝑣))〉))) |
| 19 | | fveq2 6906 |
. . . . 5
⊢ (𝑧 = 𝐵 → (𝑅‘𝑧) = (𝑅‘𝐵)) |
| 20 | | fveq2 6906 |
. . . . . 6
⊢ (𝑧 = 𝐵 → (𝐺‘𝑧) = (𝐺‘𝐵)) |
| 21 | | 2fveq3 6911 |
. . . . . 6
⊢ (𝑧 = 𝐵 → (2nd ‘(𝑅‘𝑧)) = (2nd ‘(𝑅‘𝐵))) |
| 22 | 20, 21 | opeq12d 4881 |
. . . . 5
⊢ (𝑧 = 𝐵 → 〈(𝐺‘𝑧), (2nd ‘(𝑅‘𝑧))〉 = 〈(𝐺‘𝐵), (2nd ‘(𝑅‘𝐵))〉) |
| 23 | 19, 22 | eqeq12d 2753 |
. . . 4
⊢ (𝑧 = 𝐵 → ((𝑅‘𝑧) = 〈(𝐺‘𝑧), (2nd ‘(𝑅‘𝑧))〉 ↔ (𝑅‘𝐵) = 〈(𝐺‘𝐵), (2nd ‘(𝑅‘𝐵))〉)) |
| 24 | 23 | imbi2d 340 |
. . 3
⊢ (𝑧 = 𝐵 → ((𝜑 → (𝑅‘𝑧) = 〈(𝐺‘𝑧), (2nd ‘(𝑅‘𝑧))〉) ↔ (𝜑 → (𝑅‘𝐵) = 〈(𝐺‘𝐵), (2nd ‘(𝑅‘𝐵))〉))) |
| 25 | | noseqrdg.2 |
. . . . . 6
⊢ (𝜑 → 𝑅 = (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 +s 1s ), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉) ↾ ω)) |
| 26 | 25 | fveq1d 6908 |
. . . . 5
⊢ (𝜑 → (𝑅‘∅) = ((rec((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 +s 1s ), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉) ↾
ω)‘∅)) |
| 27 | | opex 5469 |
. . . . . 6
⊢
〈𝐶, 𝐴〉 ∈ V |
| 28 | | fr0g 8476 |
. . . . . 6
⊢
(〈𝐶, 𝐴〉 ∈ V →
((rec((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 +s 1s ),
(𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉) ↾ ω)‘∅) =
〈𝐶, 𝐴〉) |
| 29 | 27, 28 | ax-mp 5 |
. . . . 5
⊢
((rec((𝑥 ∈ V,
𝑦 ∈ V ↦
〈(𝑥 +s
1s ), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉) ↾ ω)‘∅) =
〈𝐶, 𝐴〉 |
| 30 | 26, 29 | eqtrdi 2793 |
. . . 4
⊢ (𝜑 → (𝑅‘∅) = 〈𝐶, 𝐴〉) |
| 31 | | om2noseq.1 |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ No
) |
| 32 | | om2noseq.2 |
. . . . . 6
⊢ (𝜑 → 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) ↾
ω)) |
| 33 | 31, 32 | om2noseq0 28302 |
. . . . 5
⊢ (𝜑 → (𝐺‘∅) = 𝐶) |
| 34 | 30 | fveq2d 6910 |
. . . . . 6
⊢ (𝜑 → (2nd
‘(𝑅‘∅)) =
(2nd ‘〈𝐶, 𝐴〉)) |
| 35 | | noseqrdg.1 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
| 36 | | op2ndg 8027 |
. . . . . . 7
⊢ ((𝐶 ∈
No ∧ 𝐴 ∈
𝑉) → (2nd
‘〈𝐶, 𝐴〉) = 𝐴) |
| 37 | 31, 35, 36 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → (2nd
‘〈𝐶, 𝐴〉) = 𝐴) |
| 38 | 34, 37 | eqtrd 2777 |
. . . . 5
⊢ (𝜑 → (2nd
‘(𝑅‘∅)) =
𝐴) |
| 39 | 33, 38 | opeq12d 4881 |
. . . 4
⊢ (𝜑 → 〈(𝐺‘∅), (2nd
‘(𝑅‘∅))〉 = 〈𝐶, 𝐴〉) |
| 40 | 30, 39 | eqtr4d 2780 |
. . 3
⊢ (𝜑 → (𝑅‘∅) = 〈(𝐺‘∅), (2nd
‘(𝑅‘∅))〉) |
| 41 | | frsuc 8477 |
. . . . . . . . . . 11
⊢ (𝑣 ∈ ω →
((rec((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 +s 1s ),
(𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉) ↾ ω)‘suc 𝑣) = ((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 +s 1s ), (𝑥𝐹𝑦)〉)‘((rec((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 +s 1s ), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉) ↾ ω)‘𝑣))) |
| 42 | 41 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑣 ∈ ω) → ((rec((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 +s 1s ), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉) ↾ ω)‘suc 𝑣) = ((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 +s 1s ), (𝑥𝐹𝑦)〉)‘((rec((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 +s 1s ), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉) ↾ ω)‘𝑣))) |
| 43 | 25 | fveq1d 6908 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑅‘suc 𝑣) = ((rec((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 +s 1s ), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉) ↾ ω)‘suc 𝑣)) |
| 44 | 43 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑣 ∈ ω) → (𝑅‘suc 𝑣) = ((rec((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 +s 1s ), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉) ↾ ω)‘suc 𝑣)) |
| 45 | 25 | fveq1d 6908 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑅‘𝑣) = ((rec((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 +s 1s ), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉) ↾ ω)‘𝑣)) |
| 46 | 45 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 +s 1s ), (𝑥𝐹𝑦)〉)‘(𝑅‘𝑣)) = ((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 +s 1s ), (𝑥𝐹𝑦)〉)‘((rec((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 +s 1s ), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉) ↾ ω)‘𝑣))) |
| 47 | 46 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑣 ∈ ω) → ((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 +s 1s ), (𝑥𝐹𝑦)〉)‘(𝑅‘𝑣)) = ((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 +s 1s ), (𝑥𝐹𝑦)〉)‘((rec((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 +s 1s ), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉) ↾ ω)‘𝑣))) |
| 48 | 42, 44, 47 | 3eqtr4d 2787 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑣 ∈ ω) → (𝑅‘suc 𝑣) = ((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 +s 1s ), (𝑥𝐹𝑦)〉)‘(𝑅‘𝑣))) |
| 49 | 48 | adantrr 717 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑣 ∈ ω ∧ (𝑅‘𝑣) = 〈(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))〉)) → (𝑅‘suc 𝑣) = ((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 +s 1s ), (𝑥𝐹𝑦)〉)‘(𝑅‘𝑣))) |
| 50 | | fveq2 6906 |
. . . . . . . . . 10
⊢ ((𝑅‘𝑣) = 〈(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))〉 → ((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 +s 1s ), (𝑥𝐹𝑦)〉)‘(𝑅‘𝑣)) = ((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 +s 1s ), (𝑥𝐹𝑦)〉)‘〈(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))〉)) |
| 51 | | df-ov 7434 |
. . . . . . . . . . 11
⊢ ((𝐺‘𝑣)(𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 +s 1s ), (𝑥𝐹𝑦)〉)(2nd ‘(𝑅‘𝑣))) = ((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 +s 1s ), (𝑥𝐹𝑦)〉)‘〈(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))〉) |
| 52 | | fvex 6919 |
. . . . . . . . . . . 12
⊢ (𝐺‘𝑣) ∈ V |
| 53 | | fvex 6919 |
. . . . . . . . . . . 12
⊢
(2nd ‘(𝑅‘𝑣)) ∈ V |
| 54 | | oveq1 7438 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = (𝐺‘𝑣) → (𝑤 +s 1s ) = ((𝐺‘𝑣) +s 1s
)) |
| 55 | | oveq1 7438 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = (𝐺‘𝑣) → (𝑤𝐹𝑧) = ((𝐺‘𝑣)𝐹𝑧)) |
| 56 | 54, 55 | opeq12d 4881 |
. . . . . . . . . . . . 13
⊢ (𝑤 = (𝐺‘𝑣) → 〈(𝑤 +s 1s ), (𝑤𝐹𝑧)〉 = 〈((𝐺‘𝑣) +s 1s ), ((𝐺‘𝑣)𝐹𝑧)〉) |
| 57 | | oveq2 7439 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = (2nd ‘(𝑅‘𝑣)) → ((𝐺‘𝑣)𝐹𝑧) = ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣)))) |
| 58 | 57 | opeq2d 4880 |
. . . . . . . . . . . . 13
⊢ (𝑧 = (2nd ‘(𝑅‘𝑣)) → 〈((𝐺‘𝑣) +s 1s ), ((𝐺‘𝑣)𝐹𝑧)〉 = 〈((𝐺‘𝑣) +s 1s ), ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣)))〉) |
| 59 | | oveq1 7438 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑤 → (𝑥 +s 1s ) = (𝑤 +s 1s
)) |
| 60 | | oveq1 7438 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑤 → (𝑥𝐹𝑦) = (𝑤𝐹𝑦)) |
| 61 | 59, 60 | opeq12d 4881 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑤 → 〈(𝑥 +s 1s ), (𝑥𝐹𝑦)〉 = 〈(𝑤 +s 1s ), (𝑤𝐹𝑦)〉) |
| 62 | | oveq2 7439 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑧 → (𝑤𝐹𝑦) = (𝑤𝐹𝑧)) |
| 63 | 62 | opeq2d 4880 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑧 → 〈(𝑤 +s 1s ), (𝑤𝐹𝑦)〉 = 〈(𝑤 +s 1s ), (𝑤𝐹𝑧)〉) |
| 64 | 61, 63 | cbvmpov 7528 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 +s 1s ), (𝑥𝐹𝑦)〉) = (𝑤 ∈ V, 𝑧 ∈ V ↦ 〈(𝑤 +s 1s ), (𝑤𝐹𝑧)〉) |
| 65 | | opex 5469 |
. . . . . . . . . . . . 13
⊢
〈((𝐺‘𝑣) +s 1s ), ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣)))〉 ∈ V |
| 66 | 56, 58, 64, 65 | ovmpo 7593 |
. . . . . . . . . . . 12
⊢ (((𝐺‘𝑣) ∈ V ∧ (2nd
‘(𝑅‘𝑣)) ∈ V) → ((𝐺‘𝑣)(𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 +s 1s ), (𝑥𝐹𝑦)〉)(2nd ‘(𝑅‘𝑣))) = 〈((𝐺‘𝑣) +s 1s ), ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣)))〉) |
| 67 | 52, 53, 66 | mp2an 692 |
. . . . . . . . . . 11
⊢ ((𝐺‘𝑣)(𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 +s 1s ), (𝑥𝐹𝑦)〉)(2nd ‘(𝑅‘𝑣))) = 〈((𝐺‘𝑣) +s 1s ), ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣)))〉 |
| 68 | 51, 67 | eqtr3i 2767 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 +s 1s ), (𝑥𝐹𝑦)〉)‘〈(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))〉) = 〈((𝐺‘𝑣) +s 1s ), ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣)))〉 |
| 69 | 50, 68 | eqtrdi 2793 |
. . . . . . . . 9
⊢ ((𝑅‘𝑣) = 〈(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))〉 → ((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 +s 1s ), (𝑥𝐹𝑦)〉)‘(𝑅‘𝑣)) = 〈((𝐺‘𝑣) +s 1s ), ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣)))〉) |
| 70 | 69 | ad2antll 729 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑣 ∈ ω ∧ (𝑅‘𝑣) = 〈(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))〉)) → ((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 +s 1s ), (𝑥𝐹𝑦)〉)‘(𝑅‘𝑣)) = 〈((𝐺‘𝑣) +s 1s ), ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣)))〉) |
| 71 | 49, 70 | eqtrd 2777 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑣 ∈ ω ∧ (𝑅‘𝑣) = 〈(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))〉)) → (𝑅‘suc 𝑣) = 〈((𝐺‘𝑣) +s 1s ), ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣)))〉) |
| 72 | 31 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑣 ∈ ω) → 𝐶 ∈ No
) |
| 73 | 32 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑣 ∈ ω) → 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) ↾
ω)) |
| 74 | | simpr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑣 ∈ ω) → 𝑣 ∈ ω) |
| 75 | 72, 73, 74 | om2noseqsuc 28303 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑣 ∈ ω) → (𝐺‘suc 𝑣) = ((𝐺‘𝑣) +s 1s
)) |
| 76 | 75 | adantrr 717 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑣 ∈ ω ∧ (𝑅‘𝑣) = 〈(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))〉)) → (𝐺‘suc 𝑣) = ((𝐺‘𝑣) +s 1s
)) |
| 77 | 71 | fveq2d 6910 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑣 ∈ ω ∧ (𝑅‘𝑣) = 〈(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))〉)) → (2nd
‘(𝑅‘suc 𝑣)) = (2nd
‘〈((𝐺‘𝑣) +s 1s ), ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣)))〉)) |
| 78 | | ovex 7464 |
. . . . . . . . . 10
⊢ ((𝐺‘𝑣) +s 1s ) ∈
V |
| 79 | | ovex 7464 |
. . . . . . . . . 10
⊢ ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣))) ∈ V |
| 80 | 78, 79 | op2nd 8023 |
. . . . . . . . 9
⊢
(2nd ‘〈((𝐺‘𝑣) +s 1s ), ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣)))〉) = ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣))) |
| 81 | 77, 80 | eqtrdi 2793 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑣 ∈ ω ∧ (𝑅‘𝑣) = 〈(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))〉)) → (2nd
‘(𝑅‘suc 𝑣)) = ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣)))) |
| 82 | 76, 81 | opeq12d 4881 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑣 ∈ ω ∧ (𝑅‘𝑣) = 〈(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))〉)) → 〈(𝐺‘suc 𝑣), (2nd ‘(𝑅‘suc 𝑣))〉 = 〈((𝐺‘𝑣) +s 1s ), ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣)))〉) |
| 83 | 71, 82 | eqtr4d 2780 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑣 ∈ ω ∧ (𝑅‘𝑣) = 〈(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))〉)) → (𝑅‘suc 𝑣) = 〈(𝐺‘suc 𝑣), (2nd ‘(𝑅‘suc 𝑣))〉) |
| 84 | 83 | exp32 420 |
. . . . 5
⊢ (𝜑 → (𝑣 ∈ ω → ((𝑅‘𝑣) = 〈(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))〉 → (𝑅‘suc 𝑣) = 〈(𝐺‘suc 𝑣), (2nd ‘(𝑅‘suc 𝑣))〉))) |
| 85 | 84 | com12 32 |
. . . 4
⊢ (𝑣 ∈ ω → (𝜑 → ((𝑅‘𝑣) = 〈(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))〉 → (𝑅‘suc 𝑣) = 〈(𝐺‘suc 𝑣), (2nd ‘(𝑅‘suc 𝑣))〉))) |
| 86 | 85 | a2d 29 |
. . 3
⊢ (𝑣 ∈ ω → ((𝜑 → (𝑅‘𝑣) = 〈(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))〉) → (𝜑 → (𝑅‘suc 𝑣) = 〈(𝐺‘suc 𝑣), (2nd ‘(𝑅‘suc 𝑣))〉))) |
| 87 | 6, 12, 18, 24, 40, 86 | finds 7918 |
. 2
⊢ (𝐵 ∈ ω → (𝜑 → (𝑅‘𝐵) = 〈(𝐺‘𝐵), (2nd ‘(𝑅‘𝐵))〉)) |
| 88 | 87 | impcom 407 |
1
⊢ ((𝜑 ∧ 𝐵 ∈ ω) → (𝑅‘𝐵) = 〈(𝐺‘𝐵), (2nd ‘(𝑅‘𝐵))〉) |