Proof of Theorem tfrlem11
Step | Hyp | Ref
| Expression |
1 | | elsuci 6332 |
. 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 8218 |
. . . . . . . 8
⊢ (dom
recs(𝐹) ∈ On →
𝐶 Fn suc dom recs(𝐹)) |
5 | | fnfun 6533 |
. . . . . . . 8
⊢ (𝐶 Fn suc dom recs(𝐹) → Fun 𝐶) |
6 | 4, 5 | syl 17 |
. . . . . . 7
⊢ (dom
recs(𝐹) ∈ On →
Fun 𝐶) |
7 | | ssun1 4106 |
. . . . . . . . 9
⊢
recs(𝐹) ⊆
(recs(𝐹) ∪ {〈dom
recs(𝐹), (𝐹‘recs(𝐹))〉}) |
8 | 7, 3 | sseqtrri 3958 |
. . . . . . . 8
⊢
recs(𝐹) ⊆
𝐶 |
9 | 2 | tfrlem9 8216 |
. . . . . . . . 9
⊢ (𝐵 ∈ dom recs(𝐹) → (recs(𝐹)‘𝐵) = (𝐹‘(recs(𝐹) ↾ 𝐵))) |
10 | | funssfv 6795 |
. . . . . . . . . . . 12
⊢ ((Fun
𝐶 ∧ recs(𝐹) ⊆ 𝐶 ∧ 𝐵 ∈ dom recs(𝐹)) → (𝐶‘𝐵) = (recs(𝐹)‘𝐵)) |
11 | 10 | 3expa 1117 |
. . . . . . . . . . 11
⊢ (((Fun
𝐶 ∧ recs(𝐹) ⊆ 𝐶) ∧ 𝐵 ∈ dom recs(𝐹)) → (𝐶‘𝐵) = (recs(𝐹)‘𝐵)) |
12 | 11 | adantrl 713 |
. . . . . . . . . 10
⊢ (((Fun
𝐶 ∧ recs(𝐹) ⊆ 𝐶) ∧ (dom recs(𝐹) ∈ On ∧ 𝐵 ∈ dom recs(𝐹))) → (𝐶‘𝐵) = (recs(𝐹)‘𝐵)) |
13 | | onelss 6308 |
. . . . . . . . . . . 12
⊢ (dom
recs(𝐹) ∈ On →
(𝐵 ∈ dom recs(𝐹) → 𝐵 ⊆ dom recs(𝐹))) |
14 | 13 | imp 407 |
. . . . . . . . . . 11
⊢ ((dom
recs(𝐹) ∈ On ∧
𝐵 ∈ dom recs(𝐹)) → 𝐵 ⊆ dom recs(𝐹)) |
15 | | fun2ssres 6479 |
. . . . . . . . . . . . 13
⊢ ((Fun
𝐶 ∧ recs(𝐹) ⊆ 𝐶 ∧ 𝐵 ⊆ dom recs(𝐹)) → (𝐶 ↾ 𝐵) = (recs(𝐹) ↾ 𝐵)) |
16 | 15 | 3expa 1117 |
. . . . . . . . . . . 12
⊢ (((Fun
𝐶 ∧ recs(𝐹) ⊆ 𝐶) ∧ 𝐵 ⊆ dom recs(𝐹)) → (𝐶 ↾ 𝐵) = (recs(𝐹) ↾ 𝐵)) |
17 | 16 | fveq2d 6778 |
. . . . . . . . . . 11
⊢ (((Fun
𝐶 ∧ recs(𝐹) ⊆ 𝐶) ∧ 𝐵 ⊆ dom recs(𝐹)) → (𝐹‘(𝐶 ↾ 𝐵)) = (𝐹‘(recs(𝐹) ↾ 𝐵))) |
18 | 14, 17 | sylan2 593 |
. . . . . . . . . 10
⊢ (((Fun
𝐶 ∧ recs(𝐹) ⊆ 𝐶) ∧ (dom recs(𝐹) ∈ On ∧ 𝐵 ∈ dom recs(𝐹))) → (𝐹‘(𝐶 ↾ 𝐵)) = (𝐹‘(recs(𝐹) ↾ 𝐵))) |
19 | 12, 18 | eqeq12d 2754 |
. . . . . . . . 9
⊢ (((Fun
𝐶 ∧ recs(𝐹) ⊆ 𝐶) ∧ (dom recs(𝐹) ∈ On ∧ 𝐵 ∈ dom recs(𝐹))) → ((𝐶‘𝐵) = (𝐹‘(𝐶 ↾ 𝐵)) ↔ (recs(𝐹)‘𝐵) = (𝐹‘(recs(𝐹) ↾ 𝐵)))) |
20 | 9, 19 | syl5ibr 245 |
. . . . . . . 8
⊢ (((Fun
𝐶 ∧ recs(𝐹) ⊆ 𝐶) ∧ (dom recs(𝐹) ∈ On ∧ 𝐵 ∈ dom recs(𝐹))) → (𝐵 ∈ dom recs(𝐹) → (𝐶‘𝐵) = (𝐹‘(𝐶 ↾ 𝐵)))) |
21 | 8, 20 | mpanl2 698 |
. . . . . . 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 421 |
. . . . 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 5379 |
. . . . . . . . 9
⊢
〈𝐵, (𝐹‘(𝐶 ↾ 𝐵))〉 ∈ V |
27 | 26 | snid 4597 |
. . . . . . . 8
⊢
〈𝐵, (𝐹‘(𝐶 ↾ 𝐵))〉 ∈ {〈𝐵, (𝐹‘(𝐶 ↾ 𝐵))〉} |
28 | | opeq1 4804 |
. . . . . . . . . . 11
⊢ (𝐵 = dom recs(𝐹) → 〈𝐵, (𝐹‘(𝐶 ↾ 𝐵))〉 = 〈dom recs(𝐹), (𝐹‘(𝐶 ↾ 𝐵))〉) |
29 | 28 | adantl 482 |
. . . . . . . . . 10
⊢ ((dom
recs(𝐹) ∈ On ∧
𝐵 = dom recs(𝐹)) → 〈𝐵, (𝐹‘(𝐶 ↾ 𝐵))〉 = 〈dom recs(𝐹), (𝐹‘(𝐶 ↾ 𝐵))〉) |
30 | | eqimss 3977 |
. . . . . . . . . . . . . 14
⊢ (𝐵 = dom recs(𝐹) → 𝐵 ⊆ dom recs(𝐹)) |
31 | 8, 15 | mp3an2 1448 |
. . . . . . . . . . . . . 14
⊢ ((Fun
𝐶 ∧ 𝐵 ⊆ dom recs(𝐹)) → (𝐶 ↾ 𝐵) = (recs(𝐹) ↾ 𝐵)) |
32 | 6, 30, 31 | syl2an 596 |
. . . . . . . . . . . . 13
⊢ ((dom
recs(𝐹) ∈ On ∧
𝐵 = dom recs(𝐹)) → (𝐶 ↾ 𝐵) = (recs(𝐹) ↾ 𝐵)) |
33 | | reseq2 5886 |
. . . . . . . . . . . . . . 15
⊢ (𝐵 = dom recs(𝐹) → (recs(𝐹) ↾ 𝐵) = (recs(𝐹) ↾ dom recs(𝐹))) |
34 | 2 | tfrlem6 8213 |
. . . . . . . . . . . . . . . 16
⊢ Rel
recs(𝐹) |
35 | | resdm 5936 |
. . . . . . . . . . . . . . . 16
⊢ (Rel
recs(𝐹) → (recs(𝐹) ↾ dom recs(𝐹)) = recs(𝐹)) |
36 | 34, 35 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢
(recs(𝐹) ↾ dom
recs(𝐹)) = recs(𝐹) |
37 | 33, 36 | eqtrdi 2794 |
. . . . . . . . . . . . . 14
⊢ (𝐵 = dom recs(𝐹) → (recs(𝐹) ↾ 𝐵) = recs(𝐹)) |
38 | 37 | adantl 482 |
. . . . . . . . . . . . 13
⊢ ((dom
recs(𝐹) ∈ On ∧
𝐵 = dom recs(𝐹)) → (recs(𝐹) ↾ 𝐵) = recs(𝐹)) |
39 | 32, 38 | eqtrd 2778 |
. . . . . . . . . . . 12
⊢ ((dom
recs(𝐹) ∈ On ∧
𝐵 = dom recs(𝐹)) → (𝐶 ↾ 𝐵) = recs(𝐹)) |
40 | 39 | fveq2d 6778 |
. . . . . . . . . . 11
⊢ ((dom
recs(𝐹) ∈ On ∧
𝐵 = dom recs(𝐹)) → (𝐹‘(𝐶 ↾ 𝐵)) = (𝐹‘recs(𝐹))) |
41 | 40 | opeq2d 4811 |
. . . . . . . . . 10
⊢ ((dom
recs(𝐹) ∈ On ∧
𝐵 = dom recs(𝐹)) → 〈dom recs(𝐹), (𝐹‘(𝐶 ↾ 𝐵))〉 = 〈dom recs(𝐹), (𝐹‘recs(𝐹))〉) |
42 | 29, 41 | eqtrd 2778 |
. . . . . . . . 9
⊢ ((dom
recs(𝐹) ∈ On ∧
𝐵 = dom recs(𝐹)) → 〈𝐵, (𝐹‘(𝐶 ↾ 𝐵))〉 = 〈dom recs(𝐹), (𝐹‘recs(𝐹))〉) |
43 | 42 | sneqd 4573 |
. . . . . . . 8
⊢ ((dom
recs(𝐹) ∈ On ∧
𝐵 = dom recs(𝐹)) → {〈𝐵, (𝐹‘(𝐶 ↾ 𝐵))〉} = {〈dom recs(𝐹), (𝐹‘recs(𝐹))〉}) |
44 | 27, 43 | eleqtrid 2845 |
. . . . . . 7
⊢ ((dom
recs(𝐹) ∈ On ∧
𝐵 = dom recs(𝐹)) → 〈𝐵, (𝐹‘(𝐶 ↾ 𝐵))〉 ∈ {〈dom recs(𝐹), (𝐹‘recs(𝐹))〉}) |
45 | | elun2 4111 |
. . . . . . 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 2850 |
. . . . 5
⊢ ((dom
recs(𝐹) ∈ On ∧
𝐵 = dom recs(𝐹)) → 〈𝐵, (𝐹‘(𝐶 ↾ 𝐵))〉 ∈ 𝐶) |
48 | | simpr 485 |
. . . . . . 7
⊢ ((dom
recs(𝐹) ∈ On ∧
𝐵 = dom recs(𝐹)) → 𝐵 = dom recs(𝐹)) |
49 | | sucidg 6344 |
. . . . . . . 8
⊢ (dom
recs(𝐹) ∈ On →
dom recs(𝐹) ∈ suc dom
recs(𝐹)) |
50 | 49 | adantr 481 |
. . . . . . 7
⊢ ((dom
recs(𝐹) ∈ On ∧
𝐵 = dom recs(𝐹)) → dom recs(𝐹) ∈ suc dom recs(𝐹)) |
51 | 48, 50 | eqeltrd 2839 |
. . . . . 6
⊢ ((dom
recs(𝐹) ∈ On ∧
𝐵 = dom recs(𝐹)) → 𝐵 ∈ suc dom recs(𝐹)) |
52 | | fnopfvb 6823 |
. . . . . 6
⊢ ((𝐶 Fn suc dom recs(𝐹) ∧ 𝐵 ∈ suc dom recs(𝐹)) → ((𝐶‘𝐵) = (𝐹‘(𝐶 ↾ 𝐵)) ↔ 〈𝐵, (𝐹‘(𝐶 ↾ 𝐵))〉 ∈ 𝐶)) |
53 | 4, 51, 52 | syl2an2r 682 |
. . . . 5
⊢ ((dom
recs(𝐹) ∈ On ∧
𝐵 = dom recs(𝐹)) → ((𝐶‘𝐵) = (𝐹‘(𝐶 ↾ 𝐵)) ↔ 〈𝐵, (𝐹‘(𝐶 ↾ 𝐵))〉 ∈ 𝐶)) |
54 | 47, 53 | mpbird 256 |
. . . 4
⊢ ((dom
recs(𝐹) ∈ On ∧
𝐵 = dom recs(𝐹)) → (𝐶‘𝐵) = (𝐹‘(𝐶 ↾ 𝐵))) |
55 | 54 | ex 413 |
. . 3
⊢ (dom
recs(𝐹) ∈ On →
(𝐵 = dom recs(𝐹) → (𝐶‘𝐵) = (𝐹‘(𝐶 ↾ 𝐵)))) |
56 | 25, 55 | jaod 856 |
. 2
⊢ (dom
recs(𝐹) ∈ On →
((𝐵 ∈ dom recs(𝐹) ∨ 𝐵 = dom recs(𝐹)) → (𝐶‘𝐵) = (𝐹‘(𝐶 ↾ 𝐵)))) |
57 | 1, 56 | syl5 34 |
1
⊢ (dom
recs(𝐹) ∈ On →
(𝐵 ∈ suc dom
recs(𝐹) → (𝐶‘𝐵) = (𝐹‘(𝐶 ↾ 𝐵)))) |