Proof of Theorem tfrlem11
Step | Hyp | Ref
| Expression |
1 | | elsuci 6423 |
. 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 8374 |
. . . . . . . 8
⊢ (dom
recs(𝐹) ∈ On →
𝐶 Fn suc dom recs(𝐹)) |
5 | | fnfun 6641 |
. . . . . . . 8
⊢ (𝐶 Fn suc dom recs(𝐹) → Fun 𝐶) |
6 | 4, 5 | syl 17 |
. . . . . . 7
⊢ (dom
recs(𝐹) ∈ On →
Fun 𝐶) |
7 | | ssun1 4170 |
. . . . . . . . 9
⊢
recs(𝐹) ⊆
(recs(𝐹) ∪ {〈dom
recs(𝐹), (𝐹‘recs(𝐹))〉}) |
8 | 7, 3 | sseqtrri 4017 |
. . . . . . . 8
⊢
recs(𝐹) ⊆
𝐶 |
9 | 2 | tfrlem9 8372 |
. . . . . . . . 9
⊢ (𝐵 ∈ dom recs(𝐹) → (recs(𝐹)‘𝐵) = (𝐹‘(recs(𝐹) ↾ 𝐵))) |
10 | | funssfv 6902 |
. . . . . . . . . . . 12
⊢ ((Fun
𝐶 ∧ recs(𝐹) ⊆ 𝐶 ∧ 𝐵 ∈ dom recs(𝐹)) → (𝐶‘𝐵) = (recs(𝐹)‘𝐵)) |
11 | 10 | 3expa 1119 |
. . . . . . . . . . 11
⊢ (((Fun
𝐶 ∧ recs(𝐹) ⊆ 𝐶) ∧ 𝐵 ∈ dom recs(𝐹)) → (𝐶‘𝐵) = (recs(𝐹)‘𝐵)) |
12 | 11 | adantrl 715 |
. . . . . . . . . 10
⊢ (((Fun
𝐶 ∧ recs(𝐹) ⊆ 𝐶) ∧ (dom recs(𝐹) ∈ On ∧ 𝐵 ∈ dom recs(𝐹))) → (𝐶‘𝐵) = (recs(𝐹)‘𝐵)) |
13 | | onelss 6398 |
. . . . . . . . . . . 12
⊢ (dom
recs(𝐹) ∈ On →
(𝐵 ∈ dom recs(𝐹) → 𝐵 ⊆ dom recs(𝐹))) |
14 | 13 | imp 408 |
. . . . . . . . . . 11
⊢ ((dom
recs(𝐹) ∈ On ∧
𝐵 ∈ dom recs(𝐹)) → 𝐵 ⊆ dom recs(𝐹)) |
15 | | fun2ssres 6585 |
. . . . . . . . . . . . 13
⊢ ((Fun
𝐶 ∧ recs(𝐹) ⊆ 𝐶 ∧ 𝐵 ⊆ dom recs(𝐹)) → (𝐶 ↾ 𝐵) = (recs(𝐹) ↾ 𝐵)) |
16 | 15 | 3expa 1119 |
. . . . . . . . . . . 12
⊢ (((Fun
𝐶 ∧ recs(𝐹) ⊆ 𝐶) ∧ 𝐵 ⊆ dom recs(𝐹)) → (𝐶 ↾ 𝐵) = (recs(𝐹) ↾ 𝐵)) |
17 | 16 | fveq2d 6885 |
. . . . . . . . . . 11
⊢ (((Fun
𝐶 ∧ recs(𝐹) ⊆ 𝐶) ∧ 𝐵 ⊆ dom recs(𝐹)) → (𝐹‘(𝐶 ↾ 𝐵)) = (𝐹‘(recs(𝐹) ↾ 𝐵))) |
18 | 14, 17 | sylan2 594 |
. . . . . . . . . 10
⊢ (((Fun
𝐶 ∧ recs(𝐹) ⊆ 𝐶) ∧ (dom recs(𝐹) ∈ On ∧ 𝐵 ∈ dom recs(𝐹))) → (𝐹‘(𝐶 ↾ 𝐵)) = (𝐹‘(recs(𝐹) ↾ 𝐵))) |
19 | 12, 18 | eqeq12d 2749 |
. . . . . . . . 9
⊢ (((Fun
𝐶 ∧ recs(𝐹) ⊆ 𝐶) ∧ (dom recs(𝐹) ∈ On ∧ 𝐵 ∈ dom recs(𝐹))) → ((𝐶‘𝐵) = (𝐹‘(𝐶 ↾ 𝐵)) ↔ (recs(𝐹)‘𝐵) = (𝐹‘(recs(𝐹) ↾ 𝐵)))) |
20 | 9, 19 | imbitrrid 245 |
. . . . . . . 8
⊢ (((Fun
𝐶 ∧ recs(𝐹) ⊆ 𝐶) ∧ (dom recs(𝐹) ∈ On ∧ 𝐵 ∈ dom recs(𝐹))) → (𝐵 ∈ dom recs(𝐹) → (𝐶‘𝐵) = (𝐹‘(𝐶 ↾ 𝐵)))) |
21 | 8, 20 | mpanl2 700 |
. . . . . . 7
⊢ ((Fun
𝐶 ∧ (dom recs(𝐹) ∈ On ∧ 𝐵 ∈ dom recs(𝐹))) → (𝐵 ∈ dom recs(𝐹) → (𝐶‘𝐵) = (𝐹‘(𝐶 ↾ 𝐵)))) |
22 | 6, 21 | sylan 581 |
. . . . . 6
⊢ ((dom
recs(𝐹) ∈ On ∧
(dom recs(𝐹) ∈ On
∧ 𝐵 ∈ dom
recs(𝐹))) → (𝐵 ∈ dom recs(𝐹) → (𝐶‘𝐵) = (𝐹‘(𝐶 ↾ 𝐵)))) |
23 | 22 | exp32 422 |
. . . . 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 5460 |
. . . . . . . . 9
⊢
〈𝐵, (𝐹‘(𝐶 ↾ 𝐵))〉 ∈ V |
27 | 26 | snid 4660 |
. . . . . . . 8
⊢
〈𝐵, (𝐹‘(𝐶 ↾ 𝐵))〉 ∈ {〈𝐵, (𝐹‘(𝐶 ↾ 𝐵))〉} |
28 | | opeq1 4869 |
. . . . . . . . . . 11
⊢ (𝐵 = dom recs(𝐹) → 〈𝐵, (𝐹‘(𝐶 ↾ 𝐵))〉 = 〈dom recs(𝐹), (𝐹‘(𝐶 ↾ 𝐵))〉) |
29 | 28 | adantl 483 |
. . . . . . . . . 10
⊢ ((dom
recs(𝐹) ∈ On ∧
𝐵 = dom recs(𝐹)) → 〈𝐵, (𝐹‘(𝐶 ↾ 𝐵))〉 = 〈dom recs(𝐹), (𝐹‘(𝐶 ↾ 𝐵))〉) |
30 | | eqimss 4038 |
. . . . . . . . . . . . . 14
⊢ (𝐵 = dom recs(𝐹) → 𝐵 ⊆ dom recs(𝐹)) |
31 | 8, 15 | mp3an2 1450 |
. . . . . . . . . . . . . 14
⊢ ((Fun
𝐶 ∧ 𝐵 ⊆ dom recs(𝐹)) → (𝐶 ↾ 𝐵) = (recs(𝐹) ↾ 𝐵)) |
32 | 6, 30, 31 | syl2an 597 |
. . . . . . . . . . . . 13
⊢ ((dom
recs(𝐹) ∈ On ∧
𝐵 = dom recs(𝐹)) → (𝐶 ↾ 𝐵) = (recs(𝐹) ↾ 𝐵)) |
33 | | reseq2 5971 |
. . . . . . . . . . . . . . 15
⊢ (𝐵 = dom recs(𝐹) → (recs(𝐹) ↾ 𝐵) = (recs(𝐹) ↾ dom recs(𝐹))) |
34 | 2 | tfrlem6 8369 |
. . . . . . . . . . . . . . . 16
⊢ Rel
recs(𝐹) |
35 | | resdm 6021 |
. . . . . . . . . . . . . . . 16
⊢ (Rel
recs(𝐹) → (recs(𝐹) ↾ dom recs(𝐹)) = recs(𝐹)) |
36 | 34, 35 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢
(recs(𝐹) ↾ dom
recs(𝐹)) = recs(𝐹) |
37 | 33, 36 | eqtrdi 2789 |
. . . . . . . . . . . . . 14
⊢ (𝐵 = dom recs(𝐹) → (recs(𝐹) ↾ 𝐵) = recs(𝐹)) |
38 | 37 | adantl 483 |
. . . . . . . . . . . . 13
⊢ ((dom
recs(𝐹) ∈ On ∧
𝐵 = dom recs(𝐹)) → (recs(𝐹) ↾ 𝐵) = recs(𝐹)) |
39 | 32, 38 | eqtrd 2773 |
. . . . . . . . . . . 12
⊢ ((dom
recs(𝐹) ∈ On ∧
𝐵 = dom recs(𝐹)) → (𝐶 ↾ 𝐵) = recs(𝐹)) |
40 | 39 | fveq2d 6885 |
. . . . . . . . . . 11
⊢ ((dom
recs(𝐹) ∈ On ∧
𝐵 = dom recs(𝐹)) → (𝐹‘(𝐶 ↾ 𝐵)) = (𝐹‘recs(𝐹))) |
41 | 40 | opeq2d 4876 |
. . . . . . . . . 10
⊢ ((dom
recs(𝐹) ∈ On ∧
𝐵 = dom recs(𝐹)) → 〈dom recs(𝐹), (𝐹‘(𝐶 ↾ 𝐵))〉 = 〈dom recs(𝐹), (𝐹‘recs(𝐹))〉) |
42 | 29, 41 | eqtrd 2773 |
. . . . . . . . 9
⊢ ((dom
recs(𝐹) ∈ On ∧
𝐵 = dom recs(𝐹)) → 〈𝐵, (𝐹‘(𝐶 ↾ 𝐵))〉 = 〈dom recs(𝐹), (𝐹‘recs(𝐹))〉) |
43 | 42 | sneqd 4636 |
. . . . . . . 8
⊢ ((dom
recs(𝐹) ∈ On ∧
𝐵 = dom recs(𝐹)) → {〈𝐵, (𝐹‘(𝐶 ↾ 𝐵))〉} = {〈dom recs(𝐹), (𝐹‘recs(𝐹))〉}) |
44 | 27, 43 | eleqtrid 2840 |
. . . . . . 7
⊢ ((dom
recs(𝐹) ∈ On ∧
𝐵 = dom recs(𝐹)) → 〈𝐵, (𝐹‘(𝐶 ↾ 𝐵))〉 ∈ {〈dom recs(𝐹), (𝐹‘recs(𝐹))〉}) |
45 | | elun2 4175 |
. . . . . . 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 2845 |
. . . . 5
⊢ ((dom
recs(𝐹) ∈ On ∧
𝐵 = dom recs(𝐹)) → 〈𝐵, (𝐹‘(𝐶 ↾ 𝐵))〉 ∈ 𝐶) |
48 | | simpr 486 |
. . . . . . 7
⊢ ((dom
recs(𝐹) ∈ On ∧
𝐵 = dom recs(𝐹)) → 𝐵 = dom recs(𝐹)) |
49 | | sucidg 6437 |
. . . . . . . 8
⊢ (dom
recs(𝐹) ∈ On →
dom recs(𝐹) ∈ suc dom
recs(𝐹)) |
50 | 49 | adantr 482 |
. . . . . . 7
⊢ ((dom
recs(𝐹) ∈ On ∧
𝐵 = dom recs(𝐹)) → dom recs(𝐹) ∈ suc dom recs(𝐹)) |
51 | 48, 50 | eqeltrd 2834 |
. . . . . 6
⊢ ((dom
recs(𝐹) ∈ On ∧
𝐵 = dom recs(𝐹)) → 𝐵 ∈ suc dom recs(𝐹)) |
52 | | fnopfvb 6935 |
. . . . . 6
⊢ ((𝐶 Fn suc dom recs(𝐹) ∧ 𝐵 ∈ suc dom recs(𝐹)) → ((𝐶‘𝐵) = (𝐹‘(𝐶 ↾ 𝐵)) ↔ 〈𝐵, (𝐹‘(𝐶 ↾ 𝐵))〉 ∈ 𝐶)) |
53 | 4, 51, 52 | syl2an2r 684 |
. . . . 5
⊢ ((dom
recs(𝐹) ∈ On ∧
𝐵 = dom recs(𝐹)) → ((𝐶‘𝐵) = (𝐹‘(𝐶 ↾ 𝐵)) ↔ 〈𝐵, (𝐹‘(𝐶 ↾ 𝐵))〉 ∈ 𝐶)) |
54 | 47, 53 | mpbird 257 |
. . . 4
⊢ ((dom
recs(𝐹) ∈ On ∧
𝐵 = dom recs(𝐹)) → (𝐶‘𝐵) = (𝐹‘(𝐶 ↾ 𝐵))) |
55 | 54 | ex 414 |
. . 3
⊢ (dom
recs(𝐹) ∈ On →
(𝐵 = dom recs(𝐹) → (𝐶‘𝐵) = (𝐹‘(𝐶 ↾ 𝐵)))) |
56 | 25, 55 | jaod 858 |
. 2
⊢ (dom
recs(𝐹) ∈ On →
((𝐵 ∈ dom recs(𝐹) ∨ 𝐵 = dom recs(𝐹)) → (𝐶‘𝐵) = (𝐹‘(𝐶 ↾ 𝐵)))) |
57 | 1, 56 | syl5 34 |
1
⊢ (dom
recs(𝐹) ∈ On →
(𝐵 ∈ suc dom
recs(𝐹) → (𝐶‘𝐵) = (𝐹‘(𝐶 ↾ 𝐵)))) |