| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | om2noseq.1 | . . . . . . 7
⊢ (𝜑 → 𝐶 ∈  No
) | 
| 2 |  | om2noseq.2 | . . . . . . 7
⊢ (𝜑 → 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) ↾
ω)) | 
| 3 |  | om2noseq.3 | . . . . . . 7
⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) “
ω)) | 
| 4 |  | noseqrdg.1 | . . . . . . 7
⊢ (𝜑 → 𝐴 ∈ 𝑉) | 
| 5 |  | noseqrdg.2 | . . . . . . 7
⊢ (𝜑 → 𝑅 = (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 +s 1s ), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉) ↾ ω)) | 
| 6 |  | noseqrdg.3 | . . . . . . 7
⊢ (𝜑 → 𝑆 = ran 𝑅) | 
| 7 | 1, 2, 3, 4, 5, 6 | noseqrdgfn 28312 | . . . . . 6
⊢ (𝜑 → 𝑆 Fn 𝑍) | 
| 8 | 7 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝐵 ∈ 𝑍) → 𝑆 Fn 𝑍) | 
| 9 | 8 | fnfund 6669 | . . . 4
⊢ ((𝜑 ∧ 𝐵 ∈ 𝑍) → Fun 𝑆) | 
| 10 | 3 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐵 ∈ 𝑍) → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) “
ω)) | 
| 11 | 1 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐵 ∈ 𝑍) → 𝐶 ∈  No
) | 
| 12 |  | simpr 484 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐵 ∈ 𝑍) → 𝐵 ∈ 𝑍) | 
| 13 | 10, 11, 12 | noseqp1 28297 | . . . . . 6
⊢ ((𝜑 ∧ 𝐵 ∈ 𝑍) → (𝐵 +s 1s ) ∈ 𝑍) | 
| 14 | 1, 2, 3, 4, 5 | noseqrdglem 28311 | . . . . . 6
⊢ ((𝜑 ∧ (𝐵 +s 1s ) ∈ 𝑍) → 〈(𝐵 +s 1s ),
(2nd ‘(𝑅‘(◡𝐺‘(𝐵 +s 1s ))))〉
∈ ran 𝑅) | 
| 15 | 13, 14 | syldan 591 | . . . . 5
⊢ ((𝜑 ∧ 𝐵 ∈ 𝑍) → 〈(𝐵 +s 1s ),
(2nd ‘(𝑅‘(◡𝐺‘(𝐵 +s 1s ))))〉
∈ ran 𝑅) | 
| 16 | 6 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝐵 ∈ 𝑍) → 𝑆 = ran 𝑅) | 
| 17 | 15, 16 | eleqtrrd 2844 | . . . 4
⊢ ((𝜑 ∧ 𝐵 ∈ 𝑍) → 〈(𝐵 +s 1s ),
(2nd ‘(𝑅‘(◡𝐺‘(𝐵 +s 1s ))))〉
∈ 𝑆) | 
| 18 |  | funopfv 6958 | . . . 4
⊢ (Fun
𝑆 → (〈(𝐵 +s 1s ),
(2nd ‘(𝑅‘(◡𝐺‘(𝐵 +s 1s ))))〉
∈ 𝑆 → (𝑆‘(𝐵 +s 1s )) =
(2nd ‘(𝑅‘(◡𝐺‘(𝐵 +s 1s
)))))) | 
| 19 | 9, 17, 18 | sylc 65 | . . 3
⊢ ((𝜑 ∧ 𝐵 ∈ 𝑍) → (𝑆‘(𝐵 +s 1s )) =
(2nd ‘(𝑅‘(◡𝐺‘(𝐵 +s 1s
))))) | 
| 20 | 1, 2, 3 | om2noseqf1o 28307 | . . . . . . . 8
⊢ (𝜑 → 𝐺:ω–1-1-onto→𝑍) | 
| 21 | 20 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐵 ∈ 𝑍) → 𝐺:ω–1-1-onto→𝑍) | 
| 22 |  | f1ocnvdm 7305 | . . . . . . . . 9
⊢ ((𝐺:ω–1-1-onto→𝑍 ∧ 𝐵 ∈ 𝑍) → (◡𝐺‘𝐵) ∈ ω) | 
| 23 | 20, 22 | sylan 580 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐵 ∈ 𝑍) → (◡𝐺‘𝐵) ∈ ω) | 
| 24 |  | peano2 7912 | . . . . . . . 8
⊢ ((◡𝐺‘𝐵) ∈ ω → suc (◡𝐺‘𝐵) ∈ ω) | 
| 25 | 23, 24 | syl 17 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐵 ∈ 𝑍) → suc (◡𝐺‘𝐵) ∈ ω) | 
| 26 | 21, 25 | jca 511 | . . . . . 6
⊢ ((𝜑 ∧ 𝐵 ∈ 𝑍) → (𝐺:ω–1-1-onto→𝑍 ∧ suc (◡𝐺‘𝐵) ∈ ω)) | 
| 27 | 2 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐵 ∈ 𝑍) → 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) ↾
ω)) | 
| 28 | 11, 27, 23 | om2noseqsuc 28303 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐵 ∈ 𝑍) → (𝐺‘suc (◡𝐺‘𝐵)) = ((𝐺‘(◡𝐺‘𝐵)) +s 1s
)) | 
| 29 |  | f1ocnvfv2 7297 | . . . . . . . . 9
⊢ ((𝐺:ω–1-1-onto→𝑍 ∧ 𝐵 ∈ 𝑍) → (𝐺‘(◡𝐺‘𝐵)) = 𝐵) | 
| 30 | 20, 29 | sylan 580 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐵 ∈ 𝑍) → (𝐺‘(◡𝐺‘𝐵)) = 𝐵) | 
| 31 | 30 | oveq1d 7446 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐵 ∈ 𝑍) → ((𝐺‘(◡𝐺‘𝐵)) +s 1s ) = (𝐵 +s 1s
)) | 
| 32 | 28, 31 | eqtrd 2777 | . . . . . 6
⊢ ((𝜑 ∧ 𝐵 ∈ 𝑍) → (𝐺‘suc (◡𝐺‘𝐵)) = (𝐵 +s 1s
)) | 
| 33 |  | f1ocnvfv 7298 | . . . . . 6
⊢ ((𝐺:ω–1-1-onto→𝑍 ∧ suc (◡𝐺‘𝐵) ∈ ω) → ((𝐺‘suc (◡𝐺‘𝐵)) = (𝐵 +s 1s ) → (◡𝐺‘(𝐵 +s 1s )) = suc (◡𝐺‘𝐵))) | 
| 34 | 26, 32, 33 | sylc 65 | . . . . 5
⊢ ((𝜑 ∧ 𝐵 ∈ 𝑍) → (◡𝐺‘(𝐵 +s 1s )) = suc (◡𝐺‘𝐵)) | 
| 35 | 34 | fveq2d 6910 | . . . 4
⊢ ((𝜑 ∧ 𝐵 ∈ 𝑍) → (𝑅‘(◡𝐺‘(𝐵 +s 1s ))) = (𝑅‘suc (◡𝐺‘𝐵))) | 
| 36 | 35 | fveq2d 6910 | . . 3
⊢ ((𝜑 ∧ 𝐵 ∈ 𝑍) → (2nd ‘(𝑅‘(◡𝐺‘(𝐵 +s 1s )))) =
(2nd ‘(𝑅‘suc (◡𝐺‘𝐵)))) | 
| 37 | 19, 36 | eqtrd 2777 | . 2
⊢ ((𝜑 ∧ 𝐵 ∈ 𝑍) → (𝑆‘(𝐵 +s 1s )) =
(2nd ‘(𝑅‘suc (◡𝐺‘𝐵)))) | 
| 38 |  | frsuc 8477 | . . . . . . . . 9
⊢ ((◡𝐺‘𝐵) ∈ ω → ((rec((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 +s 1s ), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉) ↾ ω)‘suc (◡𝐺‘𝐵)) = ((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 +s 1s ), (𝑥𝐹𝑦)〉)‘((rec((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 +s 1s ), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉) ↾ ω)‘(◡𝐺‘𝐵)))) | 
| 39 | 38 | adantl 481 | . . . . . . . 8
⊢ ((𝜑 ∧ (◡𝐺‘𝐵) ∈ ω) → ((rec((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 +s 1s ), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉) ↾ ω)‘suc (◡𝐺‘𝐵)) = ((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 +s 1s ), (𝑥𝐹𝑦)〉)‘((rec((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 +s 1s ), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉) ↾ ω)‘(◡𝐺‘𝐵)))) | 
| 40 | 5 | fveq1d 6908 | . . . . . . . . 9
⊢ (𝜑 → (𝑅‘suc (◡𝐺‘𝐵)) = ((rec((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 +s 1s ), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉) ↾ ω)‘suc (◡𝐺‘𝐵))) | 
| 41 | 40 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ (◡𝐺‘𝐵) ∈ ω) → (𝑅‘suc (◡𝐺‘𝐵)) = ((rec((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 +s 1s ), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉) ↾ ω)‘suc (◡𝐺‘𝐵))) | 
| 42 | 5 | fveq1d 6908 | . . . . . . . . . 10
⊢ (𝜑 → (𝑅‘(◡𝐺‘𝐵)) = ((rec((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 +s 1s ), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉) ↾ ω)‘(◡𝐺‘𝐵))) | 
| 43 | 42 | fveq2d 6910 | . . . . . . . . 9
⊢ (𝜑 → ((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 +s 1s ), (𝑥𝐹𝑦)〉)‘(𝑅‘(◡𝐺‘𝐵))) = ((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 +s 1s ), (𝑥𝐹𝑦)〉)‘((rec((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 +s 1s ), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉) ↾ ω)‘(◡𝐺‘𝐵)))) | 
| 44 | 43 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ (◡𝐺‘𝐵) ∈ ω) → ((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 +s 1s ), (𝑥𝐹𝑦)〉)‘(𝑅‘(◡𝐺‘𝐵))) = ((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 +s 1s ), (𝑥𝐹𝑦)〉)‘((rec((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 +s 1s ), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉) ↾ ω)‘(◡𝐺‘𝐵)))) | 
| 45 | 39, 41, 44 | 3eqtr4d 2787 | . . . . . . 7
⊢ ((𝜑 ∧ (◡𝐺‘𝐵) ∈ ω) → (𝑅‘suc (◡𝐺‘𝐵)) = ((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 +s 1s ), (𝑥𝐹𝑦)〉)‘(𝑅‘(◡𝐺‘𝐵)))) | 
| 46 | 1, 2, 3, 4, 5 | om2noseqrdg 28310 | . . . . . . . . 9
⊢ ((𝜑 ∧ (◡𝐺‘𝐵) ∈ ω) → (𝑅‘(◡𝐺‘𝐵)) = 〈(𝐺‘(◡𝐺‘𝐵)), (2nd ‘(𝑅‘(◡𝐺‘𝐵)))〉) | 
| 47 | 46 | fveq2d 6910 | . . . . . . . 8
⊢ ((𝜑 ∧ (◡𝐺‘𝐵) ∈ ω) → ((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 +s 1s ), (𝑥𝐹𝑦)〉)‘(𝑅‘(◡𝐺‘𝐵))) = ((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 +s 1s ), (𝑥𝐹𝑦)〉)‘〈(𝐺‘(◡𝐺‘𝐵)), (2nd ‘(𝑅‘(◡𝐺‘𝐵)))〉)) | 
| 48 |  | df-ov 7434 | . . . . . . . 8
⊢ ((𝐺‘(◡𝐺‘𝐵))(𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 +s 1s ), (𝑥𝐹𝑦)〉)(2nd ‘(𝑅‘(◡𝐺‘𝐵)))) = ((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 +s 1s ), (𝑥𝐹𝑦)〉)‘〈(𝐺‘(◡𝐺‘𝐵)), (2nd ‘(𝑅‘(◡𝐺‘𝐵)))〉) | 
| 49 | 47, 48 | eqtr4di 2795 | . . . . . . 7
⊢ ((𝜑 ∧ (◡𝐺‘𝐵) ∈ ω) → ((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 +s 1s ), (𝑥𝐹𝑦)〉)‘(𝑅‘(◡𝐺‘𝐵))) = ((𝐺‘(◡𝐺‘𝐵))(𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 +s 1s ), (𝑥𝐹𝑦)〉)(2nd ‘(𝑅‘(◡𝐺‘𝐵))))) | 
| 50 | 45, 49 | eqtrd 2777 | . . . . . 6
⊢ ((𝜑 ∧ (◡𝐺‘𝐵) ∈ ω) → (𝑅‘suc (◡𝐺‘𝐵)) = ((𝐺‘(◡𝐺‘𝐵))(𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 +s 1s ), (𝑥𝐹𝑦)〉)(2nd ‘(𝑅‘(◡𝐺‘𝐵))))) | 
| 51 |  | fvex 6919 | . . . . . . 7
⊢ (𝐺‘(◡𝐺‘𝐵)) ∈ V | 
| 52 |  | fvex 6919 | . . . . . . 7
⊢
(2nd ‘(𝑅‘(◡𝐺‘𝐵))) ∈ V | 
| 53 |  | oveq1 7438 | . . . . . . . . 9
⊢ (𝑧 = (𝐺‘(◡𝐺‘𝐵)) → (𝑧 +s 1s ) = ((𝐺‘(◡𝐺‘𝐵)) +s 1s
)) | 
| 54 |  | oveq1 7438 | . . . . . . . . 9
⊢ (𝑧 = (𝐺‘(◡𝐺‘𝐵)) → (𝑧𝐹𝑤) = ((𝐺‘(◡𝐺‘𝐵))𝐹𝑤)) | 
| 55 | 53, 54 | opeq12d 4881 | . . . . . . . 8
⊢ (𝑧 = (𝐺‘(◡𝐺‘𝐵)) → 〈(𝑧 +s 1s ), (𝑧𝐹𝑤)〉 = 〈((𝐺‘(◡𝐺‘𝐵)) +s 1s ), ((𝐺‘(◡𝐺‘𝐵))𝐹𝑤)〉) | 
| 56 |  | oveq2 7439 | . . . . . . . . 9
⊢ (𝑤 = (2nd ‘(𝑅‘(◡𝐺‘𝐵))) → ((𝐺‘(◡𝐺‘𝐵))𝐹𝑤) = ((𝐺‘(◡𝐺‘𝐵))𝐹(2nd ‘(𝑅‘(◡𝐺‘𝐵))))) | 
| 57 | 56 | opeq2d 4880 | . . . . . . . 8
⊢ (𝑤 = (2nd ‘(𝑅‘(◡𝐺‘𝐵))) → 〈((𝐺‘(◡𝐺‘𝐵)) +s 1s ), ((𝐺‘(◡𝐺‘𝐵))𝐹𝑤)〉 = 〈((𝐺‘(◡𝐺‘𝐵)) +s 1s ), ((𝐺‘(◡𝐺‘𝐵))𝐹(2nd ‘(𝑅‘(◡𝐺‘𝐵))))〉) | 
| 58 |  | oveq1 7438 | . . . . . . . . . 10
⊢ (𝑥 = 𝑧 → (𝑥 +s 1s ) = (𝑧 +s 1s
)) | 
| 59 |  | oveq1 7438 | . . . . . . . . . 10
⊢ (𝑥 = 𝑧 → (𝑥𝐹𝑦) = (𝑧𝐹𝑦)) | 
| 60 | 58, 59 | opeq12d 4881 | . . . . . . . . 9
⊢ (𝑥 = 𝑧 → 〈(𝑥 +s 1s ), (𝑥𝐹𝑦)〉 = 〈(𝑧 +s 1s ), (𝑧𝐹𝑦)〉) | 
| 61 |  | oveq2 7439 | . . . . . . . . . 10
⊢ (𝑦 = 𝑤 → (𝑧𝐹𝑦) = (𝑧𝐹𝑤)) | 
| 62 | 61 | opeq2d 4880 | . . . . . . . . 9
⊢ (𝑦 = 𝑤 → 〈(𝑧 +s 1s ), (𝑧𝐹𝑦)〉 = 〈(𝑧 +s 1s ), (𝑧𝐹𝑤)〉) | 
| 63 | 60, 62 | cbvmpov 7528 | . . . . . . . 8
⊢ (𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 +s 1s ), (𝑥𝐹𝑦)〉) = (𝑧 ∈ V, 𝑤 ∈ V ↦ 〈(𝑧 +s 1s ), (𝑧𝐹𝑤)〉) | 
| 64 |  | opex 5469 | . . . . . . . 8
⊢
〈((𝐺‘(◡𝐺‘𝐵)) +s 1s ), ((𝐺‘(◡𝐺‘𝐵))𝐹(2nd ‘(𝑅‘(◡𝐺‘𝐵))))〉 ∈ V | 
| 65 | 55, 57, 63, 64 | ovmpo 7593 | . . . . . . 7
⊢ (((𝐺‘(◡𝐺‘𝐵)) ∈ V ∧ (2nd
‘(𝑅‘(◡𝐺‘𝐵))) ∈ V) → ((𝐺‘(◡𝐺‘𝐵))(𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 +s 1s ), (𝑥𝐹𝑦)〉)(2nd ‘(𝑅‘(◡𝐺‘𝐵)))) = 〈((𝐺‘(◡𝐺‘𝐵)) +s 1s ), ((𝐺‘(◡𝐺‘𝐵))𝐹(2nd ‘(𝑅‘(◡𝐺‘𝐵))))〉) | 
| 66 | 51, 52, 65 | mp2an 692 | . . . . . 6
⊢ ((𝐺‘(◡𝐺‘𝐵))(𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 +s 1s ), (𝑥𝐹𝑦)〉)(2nd ‘(𝑅‘(◡𝐺‘𝐵)))) = 〈((𝐺‘(◡𝐺‘𝐵)) +s 1s ), ((𝐺‘(◡𝐺‘𝐵))𝐹(2nd ‘(𝑅‘(◡𝐺‘𝐵))))〉 | 
| 67 | 50, 66 | eqtrdi 2793 | . . . . 5
⊢ ((𝜑 ∧ (◡𝐺‘𝐵) ∈ ω) → (𝑅‘suc (◡𝐺‘𝐵)) = 〈((𝐺‘(◡𝐺‘𝐵)) +s 1s ), ((𝐺‘(◡𝐺‘𝐵))𝐹(2nd ‘(𝑅‘(◡𝐺‘𝐵))))〉) | 
| 68 | 67 | fveq2d 6910 | . . . 4
⊢ ((𝜑 ∧ (◡𝐺‘𝐵) ∈ ω) → (2nd
‘(𝑅‘suc (◡𝐺‘𝐵))) = (2nd ‘〈((𝐺‘(◡𝐺‘𝐵)) +s 1s ), ((𝐺‘(◡𝐺‘𝐵))𝐹(2nd ‘(𝑅‘(◡𝐺‘𝐵))))〉)) | 
| 69 |  | ovex 7464 | . . . . 5
⊢ ((𝐺‘(◡𝐺‘𝐵)) +s 1s ) ∈
V | 
| 70 |  | ovex 7464 | . . . . 5
⊢ ((𝐺‘(◡𝐺‘𝐵))𝐹(2nd ‘(𝑅‘(◡𝐺‘𝐵)))) ∈ V | 
| 71 | 69, 70 | op2nd 8023 | . . . 4
⊢
(2nd ‘〈((𝐺‘(◡𝐺‘𝐵)) +s 1s ), ((𝐺‘(◡𝐺‘𝐵))𝐹(2nd ‘(𝑅‘(◡𝐺‘𝐵))))〉) = ((𝐺‘(◡𝐺‘𝐵))𝐹(2nd ‘(𝑅‘(◡𝐺‘𝐵)))) | 
| 72 | 68, 71 | eqtrdi 2793 | . . 3
⊢ ((𝜑 ∧ (◡𝐺‘𝐵) ∈ ω) → (2nd
‘(𝑅‘suc (◡𝐺‘𝐵))) = ((𝐺‘(◡𝐺‘𝐵))𝐹(2nd ‘(𝑅‘(◡𝐺‘𝐵))))) | 
| 73 | 23, 72 | syldan 591 | . 2
⊢ ((𝜑 ∧ 𝐵 ∈ 𝑍) → (2nd ‘(𝑅‘suc (◡𝐺‘𝐵))) = ((𝐺‘(◡𝐺‘𝐵))𝐹(2nd ‘(𝑅‘(◡𝐺‘𝐵))))) | 
| 74 | 1, 2, 3, 4, 5 | noseqrdglem 28311 | . . . . . 6
⊢ ((𝜑 ∧ 𝐵 ∈ 𝑍) → 〈𝐵, (2nd ‘(𝑅‘(◡𝐺‘𝐵)))〉 ∈ ran 𝑅) | 
| 75 | 74, 16 | eleqtrrd 2844 | . . . . 5
⊢ ((𝜑 ∧ 𝐵 ∈ 𝑍) → 〈𝐵, (2nd ‘(𝑅‘(◡𝐺‘𝐵)))〉 ∈ 𝑆) | 
| 76 |  | funopfv 6958 | . . . . 5
⊢ (Fun
𝑆 → (〈𝐵, (2nd ‘(𝑅‘(◡𝐺‘𝐵)))〉 ∈ 𝑆 → (𝑆‘𝐵) = (2nd ‘(𝑅‘(◡𝐺‘𝐵))))) | 
| 77 | 9, 75, 76 | sylc 65 | . . . 4
⊢ ((𝜑 ∧ 𝐵 ∈ 𝑍) → (𝑆‘𝐵) = (2nd ‘(𝑅‘(◡𝐺‘𝐵)))) | 
| 78 | 77 | eqcomd 2743 | . . 3
⊢ ((𝜑 ∧ 𝐵 ∈ 𝑍) → (2nd ‘(𝑅‘(◡𝐺‘𝐵))) = (𝑆‘𝐵)) | 
| 79 | 30, 78 | oveq12d 7449 | . 2
⊢ ((𝜑 ∧ 𝐵 ∈ 𝑍) → ((𝐺‘(◡𝐺‘𝐵))𝐹(2nd ‘(𝑅‘(◡𝐺‘𝐵)))) = (𝐵𝐹(𝑆‘𝐵))) | 
| 80 | 37, 73, 79 | 3eqtrd 2781 | 1
⊢ ((𝜑 ∧ 𝐵 ∈ 𝑍) → (𝑆‘(𝐵 +s 1s )) = (𝐵𝐹(𝑆‘𝐵))) |