Proof of Theorem tfrlem11
| Step | Hyp | Ref
| Expression |
| 1 | | elsuci 6451 |
. 2
⊢ (𝐵 ∈ suc dom recs(𝐹) → (𝐵 ∈ dom recs(𝐹) ∨ 𝐵 = dom recs(𝐹))) |
| 2 | | tfrlem.1 |
. . . . . . . . 9
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))} |
| 3 | | tfrlem.3 |
. . . . . . . . 9
⊢ 𝐶 = (recs(𝐹) ∪ {〈dom recs(𝐹), (𝐹‘recs(𝐹))〉}) |
| 4 | 2, 3 | tfrlem10 8427 |
. . . . . . . 8
⊢ (dom
recs(𝐹) ∈ On →
𝐶 Fn suc dom recs(𝐹)) |
| 5 | | fnfun 6668 |
. . . . . . . 8
⊢ (𝐶 Fn suc dom recs(𝐹) → Fun 𝐶) |
| 6 | 4, 5 | syl 17 |
. . . . . . 7
⊢ (dom
recs(𝐹) ∈ On →
Fun 𝐶) |
| 7 | | ssun1 4178 |
. . . . . . . . 9
⊢
recs(𝐹) ⊆
(recs(𝐹) ∪ {〈dom
recs(𝐹), (𝐹‘recs(𝐹))〉}) |
| 8 | 7, 3 | sseqtrri 4033 |
. . . . . . . 8
⊢
recs(𝐹) ⊆
𝐶 |
| 9 | 2 | tfrlem9 8425 |
. . . . . . . . 9
⊢ (𝐵 ∈ dom recs(𝐹) → (recs(𝐹)‘𝐵) = (𝐹‘(recs(𝐹) ↾ 𝐵))) |
| 10 | | funssfv 6927 |
. . . . . . . . . . . 12
⊢ ((Fun
𝐶 ∧ recs(𝐹) ⊆ 𝐶 ∧ 𝐵 ∈ dom recs(𝐹)) → (𝐶‘𝐵) = (recs(𝐹)‘𝐵)) |
| 11 | 10 | 3expa 1119 |
. . . . . . . . . . 11
⊢ (((Fun
𝐶 ∧ recs(𝐹) ⊆ 𝐶) ∧ 𝐵 ∈ dom recs(𝐹)) → (𝐶‘𝐵) = (recs(𝐹)‘𝐵)) |
| 12 | 11 | adantrl 716 |
. . . . . . . . . 10
⊢ (((Fun
𝐶 ∧ recs(𝐹) ⊆ 𝐶) ∧ (dom recs(𝐹) ∈ On ∧ 𝐵 ∈ dom recs(𝐹))) → (𝐶‘𝐵) = (recs(𝐹)‘𝐵)) |
| 13 | | onelss 6426 |
. . . . . . . . . . . 12
⊢ (dom
recs(𝐹) ∈ On →
(𝐵 ∈ dom recs(𝐹) → 𝐵 ⊆ dom recs(𝐹))) |
| 14 | 13 | imp 406 |
. . . . . . . . . . 11
⊢ ((dom
recs(𝐹) ∈ On ∧
𝐵 ∈ dom recs(𝐹)) → 𝐵 ⊆ dom recs(𝐹)) |
| 15 | | fun2ssres 6611 |
. . . . . . . . . . . . 13
⊢ ((Fun
𝐶 ∧ recs(𝐹) ⊆ 𝐶 ∧ 𝐵 ⊆ dom recs(𝐹)) → (𝐶 ↾ 𝐵) = (recs(𝐹) ↾ 𝐵)) |
| 16 | 15 | 3expa 1119 |
. . . . . . . . . . . 12
⊢ (((Fun
𝐶 ∧ recs(𝐹) ⊆ 𝐶) ∧ 𝐵 ⊆ dom recs(𝐹)) → (𝐶 ↾ 𝐵) = (recs(𝐹) ↾ 𝐵)) |
| 17 | 16 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ (((Fun
𝐶 ∧ recs(𝐹) ⊆ 𝐶) ∧ 𝐵 ⊆ dom recs(𝐹)) → (𝐹‘(𝐶 ↾ 𝐵)) = (𝐹‘(recs(𝐹) ↾ 𝐵))) |
| 18 | 14, 17 | sylan2 593 |
. . . . . . . . . 10
⊢ (((Fun
𝐶 ∧ recs(𝐹) ⊆ 𝐶) ∧ (dom recs(𝐹) ∈ On ∧ 𝐵 ∈ dom recs(𝐹))) → (𝐹‘(𝐶 ↾ 𝐵)) = (𝐹‘(recs(𝐹) ↾ 𝐵))) |
| 19 | 12, 18 | eqeq12d 2753 |
. . . . . . . . 9
⊢ (((Fun
𝐶 ∧ recs(𝐹) ⊆ 𝐶) ∧ (dom recs(𝐹) ∈ On ∧ 𝐵 ∈ dom recs(𝐹))) → ((𝐶‘𝐵) = (𝐹‘(𝐶 ↾ 𝐵)) ↔ (recs(𝐹)‘𝐵) = (𝐹‘(recs(𝐹) ↾ 𝐵)))) |
| 20 | 9, 19 | imbitrrid 246 |
. . . . . . . 8
⊢ (((Fun
𝐶 ∧ recs(𝐹) ⊆ 𝐶) ∧ (dom recs(𝐹) ∈ On ∧ 𝐵 ∈ dom recs(𝐹))) → (𝐵 ∈ dom recs(𝐹) → (𝐶‘𝐵) = (𝐹‘(𝐶 ↾ 𝐵)))) |
| 21 | 8, 20 | mpanl2 701 |
. . . . . . 7
⊢ ((Fun
𝐶 ∧ (dom recs(𝐹) ∈ On ∧ 𝐵 ∈ dom recs(𝐹))) → (𝐵 ∈ dom recs(𝐹) → (𝐶‘𝐵) = (𝐹‘(𝐶 ↾ 𝐵)))) |
| 22 | 6, 21 | sylan 580 |
. . . . . 6
⊢ ((dom
recs(𝐹) ∈ On ∧
(dom recs(𝐹) ∈ On
∧ 𝐵 ∈ dom
recs(𝐹))) → (𝐵 ∈ dom recs(𝐹) → (𝐶‘𝐵) = (𝐹‘(𝐶 ↾ 𝐵)))) |
| 23 | 22 | exp32 420 |
. . . . 5
⊢ (dom
recs(𝐹) ∈ On →
(dom recs(𝐹) ∈ On
→ (𝐵 ∈ dom
recs(𝐹) → (𝐵 ∈ dom recs(𝐹) → (𝐶‘𝐵) = (𝐹‘(𝐶 ↾ 𝐵)))))) |
| 24 | 23 | pm2.43i 52 |
. . . 4
⊢ (dom
recs(𝐹) ∈ On →
(𝐵 ∈ dom recs(𝐹) → (𝐵 ∈ dom recs(𝐹) → (𝐶‘𝐵) = (𝐹‘(𝐶 ↾ 𝐵))))) |
| 25 | 24 | pm2.43d 53 |
. . 3
⊢ (dom
recs(𝐹) ∈ On →
(𝐵 ∈ dom recs(𝐹) → (𝐶‘𝐵) = (𝐹‘(𝐶 ↾ 𝐵)))) |
| 26 | | opex 5469 |
. . . . . . . . 9
⊢
〈𝐵, (𝐹‘(𝐶 ↾ 𝐵))〉 ∈ V |
| 27 | 26 | snid 4662 |
. . . . . . . 8
⊢
〈𝐵, (𝐹‘(𝐶 ↾ 𝐵))〉 ∈ {〈𝐵, (𝐹‘(𝐶 ↾ 𝐵))〉} |
| 28 | | opeq1 4873 |
. . . . . . . . . . 11
⊢ (𝐵 = dom recs(𝐹) → 〈𝐵, (𝐹‘(𝐶 ↾ 𝐵))〉 = 〈dom recs(𝐹), (𝐹‘(𝐶 ↾ 𝐵))〉) |
| 29 | 28 | adantl 481 |
. . . . . . . . . 10
⊢ ((dom
recs(𝐹) ∈ On ∧
𝐵 = dom recs(𝐹)) → 〈𝐵, (𝐹‘(𝐶 ↾ 𝐵))〉 = 〈dom recs(𝐹), (𝐹‘(𝐶 ↾ 𝐵))〉) |
| 30 | | eqimss 4042 |
. . . . . . . . . . . . . 14
⊢ (𝐵 = dom recs(𝐹) → 𝐵 ⊆ dom recs(𝐹)) |
| 31 | 8, 15 | mp3an2 1451 |
. . . . . . . . . . . . . 14
⊢ ((Fun
𝐶 ∧ 𝐵 ⊆ dom recs(𝐹)) → (𝐶 ↾ 𝐵) = (recs(𝐹) ↾ 𝐵)) |
| 32 | 6, 30, 31 | syl2an 596 |
. . . . . . . . . . . . 13
⊢ ((dom
recs(𝐹) ∈ On ∧
𝐵 = dom recs(𝐹)) → (𝐶 ↾ 𝐵) = (recs(𝐹) ↾ 𝐵)) |
| 33 | | reseq2 5992 |
. . . . . . . . . . . . . . 15
⊢ (𝐵 = dom recs(𝐹) → (recs(𝐹) ↾ 𝐵) = (recs(𝐹) ↾ dom recs(𝐹))) |
| 34 | 2 | tfrlem6 8422 |
. . . . . . . . . . . . . . . 16
⊢ Rel
recs(𝐹) |
| 35 | | resdm 6044 |
. . . . . . . . . . . . . . . 16
⊢ (Rel
recs(𝐹) → (recs(𝐹) ↾ dom recs(𝐹)) = recs(𝐹)) |
| 36 | 34, 35 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢
(recs(𝐹) ↾ dom
recs(𝐹)) = recs(𝐹) |
| 37 | 33, 36 | eqtrdi 2793 |
. . . . . . . . . . . . . 14
⊢ (𝐵 = dom recs(𝐹) → (recs(𝐹) ↾ 𝐵) = recs(𝐹)) |
| 38 | 37 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((dom
recs(𝐹) ∈ On ∧
𝐵 = dom recs(𝐹)) → (recs(𝐹) ↾ 𝐵) = recs(𝐹)) |
| 39 | 32, 38 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ ((dom
recs(𝐹) ∈ On ∧
𝐵 = dom recs(𝐹)) → (𝐶 ↾ 𝐵) = recs(𝐹)) |
| 40 | 39 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ ((dom
recs(𝐹) ∈ On ∧
𝐵 = dom recs(𝐹)) → (𝐹‘(𝐶 ↾ 𝐵)) = (𝐹‘recs(𝐹))) |
| 41 | 40 | opeq2d 4880 |
. . . . . . . . . 10
⊢ ((dom
recs(𝐹) ∈ On ∧
𝐵 = dom recs(𝐹)) → 〈dom recs(𝐹), (𝐹‘(𝐶 ↾ 𝐵))〉 = 〈dom recs(𝐹), (𝐹‘recs(𝐹))〉) |
| 42 | 29, 41 | eqtrd 2777 |
. . . . . . . . 9
⊢ ((dom
recs(𝐹) ∈ On ∧
𝐵 = dom recs(𝐹)) → 〈𝐵, (𝐹‘(𝐶 ↾ 𝐵))〉 = 〈dom recs(𝐹), (𝐹‘recs(𝐹))〉) |
| 43 | 42 | sneqd 4638 |
. . . . . . . 8
⊢ ((dom
recs(𝐹) ∈ On ∧
𝐵 = dom recs(𝐹)) → {〈𝐵, (𝐹‘(𝐶 ↾ 𝐵))〉} = {〈dom recs(𝐹), (𝐹‘recs(𝐹))〉}) |
| 44 | 27, 43 | eleqtrid 2847 |
. . . . . . 7
⊢ ((dom
recs(𝐹) ∈ On ∧
𝐵 = dom recs(𝐹)) → 〈𝐵, (𝐹‘(𝐶 ↾ 𝐵))〉 ∈ {〈dom recs(𝐹), (𝐹‘recs(𝐹))〉}) |
| 45 | | elun2 4183 |
. . . . . . 7
⊢
(〈𝐵, (𝐹‘(𝐶 ↾ 𝐵))〉 ∈ {〈dom recs(𝐹), (𝐹‘recs(𝐹))〉} → 〈𝐵, (𝐹‘(𝐶 ↾ 𝐵))〉 ∈ (recs(𝐹) ∪ {〈dom recs(𝐹), (𝐹‘recs(𝐹))〉})) |
| 46 | 44, 45 | syl 17 |
. . . . . 6
⊢ ((dom
recs(𝐹) ∈ On ∧
𝐵 = dom recs(𝐹)) → 〈𝐵, (𝐹‘(𝐶 ↾ 𝐵))〉 ∈ (recs(𝐹) ∪ {〈dom recs(𝐹), (𝐹‘recs(𝐹))〉})) |
| 47 | 46, 3 | eleqtrrdi 2852 |
. . . . 5
⊢ ((dom
recs(𝐹) ∈ On ∧
𝐵 = dom recs(𝐹)) → 〈𝐵, (𝐹‘(𝐶 ↾ 𝐵))〉 ∈ 𝐶) |
| 48 | | simpr 484 |
. . . . . . 7
⊢ ((dom
recs(𝐹) ∈ On ∧
𝐵 = dom recs(𝐹)) → 𝐵 = dom recs(𝐹)) |
| 49 | | sucidg 6465 |
. . . . . . . 8
⊢ (dom
recs(𝐹) ∈ On →
dom recs(𝐹) ∈ suc dom
recs(𝐹)) |
| 50 | 49 | adantr 480 |
. . . . . . 7
⊢ ((dom
recs(𝐹) ∈ On ∧
𝐵 = dom recs(𝐹)) → dom recs(𝐹) ∈ suc dom recs(𝐹)) |
| 51 | 48, 50 | eqeltrd 2841 |
. . . . . 6
⊢ ((dom
recs(𝐹) ∈ On ∧
𝐵 = dom recs(𝐹)) → 𝐵 ∈ suc dom recs(𝐹)) |
| 52 | | fnopfvb 6960 |
. . . . . 6
⊢ ((𝐶 Fn suc dom recs(𝐹) ∧ 𝐵 ∈ suc dom recs(𝐹)) → ((𝐶‘𝐵) = (𝐹‘(𝐶 ↾ 𝐵)) ↔ 〈𝐵, (𝐹‘(𝐶 ↾ 𝐵))〉 ∈ 𝐶)) |
| 53 | 4, 51, 52 | syl2an2r 685 |
. . . . 5
⊢ ((dom
recs(𝐹) ∈ On ∧
𝐵 = dom recs(𝐹)) → ((𝐶‘𝐵) = (𝐹‘(𝐶 ↾ 𝐵)) ↔ 〈𝐵, (𝐹‘(𝐶 ↾ 𝐵))〉 ∈ 𝐶)) |
| 54 | 47, 53 | mpbird 257 |
. . . 4
⊢ ((dom
recs(𝐹) ∈ On ∧
𝐵 = dom recs(𝐹)) → (𝐶‘𝐵) = (𝐹‘(𝐶 ↾ 𝐵))) |
| 55 | 54 | ex 412 |
. . 3
⊢ (dom
recs(𝐹) ∈ On →
(𝐵 = dom recs(𝐹) → (𝐶‘𝐵) = (𝐹‘(𝐶 ↾ 𝐵)))) |
| 56 | 25, 55 | jaod 860 |
. 2
⊢ (dom
recs(𝐹) ∈ On →
((𝐵 ∈ dom recs(𝐹) ∨ 𝐵 = dom recs(𝐹)) → (𝐶‘𝐵) = (𝐹‘(𝐶 ↾ 𝐵)))) |
| 57 | 1, 56 | syl5 34 |
1
⊢ (dom
recs(𝐹) ∈ On →
(𝐵 ∈ suc dom
recs(𝐹) → (𝐶‘𝐵) = (𝐹‘(𝐶 ↾ 𝐵)))) |