Proof of Theorem tfrlem11
Step | Hyp | Ref
| Expression |
1 | | elsuci 5708 |
. 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 7370 |
. . . . . . . 8
⊢ (dom
recs(𝐹) ∈ On →
𝐶 Fn suc dom recs(𝐹)) |
5 | | fnfun 5902 |
. . . . . . . 8
⊢ (𝐶 Fn suc dom recs(𝐹) → Fun 𝐶) |
6 | 4, 5 | syl 17 |
. . . . . . 7
⊢ (dom
recs(𝐹) ∈ On →
Fun 𝐶) |
7 | | ssun1 3738 |
. . . . . . . . 9
⊢
recs(𝐹) ⊆
(recs(𝐹) ∪ {〈dom
recs(𝐹), (𝐹‘recs(𝐹))〉}) |
8 | 7, 3 | sseqtr4i 3601 |
. . . . . . . 8
⊢
recs(𝐹) ⊆
𝐶 |
9 | 2 | tfrlem9 7368 |
. . . . . . . . 9
⊢ (𝐵 ∈ dom recs(𝐹) → (recs(𝐹)‘𝐵) = (𝐹‘(recs(𝐹) ↾ 𝐵))) |
10 | | funssfv 6119 |
. . . . . . . . . . . 12
⊢ ((Fun
𝐶 ∧ recs(𝐹) ⊆ 𝐶 ∧ 𝐵 ∈ dom recs(𝐹)) → (𝐶‘𝐵) = (recs(𝐹)‘𝐵)) |
11 | 10 | 3expa 1257 |
. . . . . . . . . . 11
⊢ (((Fun
𝐶 ∧ recs(𝐹) ⊆ 𝐶) ∧ 𝐵 ∈ dom recs(𝐹)) → (𝐶‘𝐵) = (recs(𝐹)‘𝐵)) |
12 | 11 | adantrl 748 |
. . . . . . . . . 10
⊢ (((Fun
𝐶 ∧ recs(𝐹) ⊆ 𝐶) ∧ (dom recs(𝐹) ∈ On ∧ 𝐵 ∈ dom recs(𝐹))) → (𝐶‘𝐵) = (recs(𝐹)‘𝐵)) |
13 | | onelss 5683 |
. . . . . . . . . . . 12
⊢ (dom
recs(𝐹) ∈ On →
(𝐵 ∈ dom recs(𝐹) → 𝐵 ⊆ dom recs(𝐹))) |
14 | 13 | imp 444 |
. . . . . . . . . . 11
⊢ ((dom
recs(𝐹) ∈ On ∧
𝐵 ∈ dom recs(𝐹)) → 𝐵 ⊆ dom recs(𝐹)) |
15 | | fun2ssres 5845 |
. . . . . . . . . . . . 13
⊢ ((Fun
𝐶 ∧ recs(𝐹) ⊆ 𝐶 ∧ 𝐵 ⊆ dom recs(𝐹)) → (𝐶 ↾ 𝐵) = (recs(𝐹) ↾ 𝐵)) |
16 | 15 | 3expa 1257 |
. . . . . . . . . . . 12
⊢ (((Fun
𝐶 ∧ recs(𝐹) ⊆ 𝐶) ∧ 𝐵 ⊆ dom recs(𝐹)) → (𝐶 ↾ 𝐵) = (recs(𝐹) ↾ 𝐵)) |
17 | 16 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (((Fun
𝐶 ∧ recs(𝐹) ⊆ 𝐶) ∧ 𝐵 ⊆ dom recs(𝐹)) → (𝐹‘(𝐶 ↾ 𝐵)) = (𝐹‘(recs(𝐹) ↾ 𝐵))) |
18 | 14, 17 | sylan2 490 |
. . . . . . . . . 10
⊢ (((Fun
𝐶 ∧ recs(𝐹) ⊆ 𝐶) ∧ (dom recs(𝐹) ∈ On ∧ 𝐵 ∈ dom recs(𝐹))) → (𝐹‘(𝐶 ↾ 𝐵)) = (𝐹‘(recs(𝐹) ↾ 𝐵))) |
19 | 12, 18 | eqeq12d 2625 |
. . . . . . . . 9
⊢ (((Fun
𝐶 ∧ recs(𝐹) ⊆ 𝐶) ∧ (dom recs(𝐹) ∈ On ∧ 𝐵 ∈ dom recs(𝐹))) → ((𝐶‘𝐵) = (𝐹‘(𝐶 ↾ 𝐵)) ↔ (recs(𝐹)‘𝐵) = (𝐹‘(recs(𝐹) ↾ 𝐵)))) |
20 | 9, 19 | syl5ibr 235 |
. . . . . . . 8
⊢ (((Fun
𝐶 ∧ recs(𝐹) ⊆ 𝐶) ∧ (dom recs(𝐹) ∈ On ∧ 𝐵 ∈ dom recs(𝐹))) → (𝐵 ∈ dom recs(𝐹) → (𝐶‘𝐵) = (𝐹‘(𝐶 ↾ 𝐵)))) |
21 | 8, 20 | mpanl2 713 |
. . . . . . 7
⊢ ((Fun
𝐶 ∧ (dom recs(𝐹) ∈ On ∧ 𝐵 ∈ dom recs(𝐹))) → (𝐵 ∈ dom recs(𝐹) → (𝐶‘𝐵) = (𝐹‘(𝐶 ↾ 𝐵)))) |
22 | 6, 21 | sylan 487 |
. . . . . 6
⊢ ((dom
recs(𝐹) ∈ On ∧
(dom recs(𝐹) ∈ On
∧ 𝐵 ∈ dom
recs(𝐹))) → (𝐵 ∈ dom recs(𝐹) → (𝐶‘𝐵) = (𝐹‘(𝐶 ↾ 𝐵)))) |
23 | 22 | exp32 629 |
. . . . 5
⊢ (dom
recs(𝐹) ∈ On →
(dom recs(𝐹) ∈ On
→ (𝐵 ∈ dom
recs(𝐹) → (𝐵 ∈ dom recs(𝐹) → (𝐶‘𝐵) = (𝐹‘(𝐶 ↾ 𝐵)))))) |
24 | 23 | pm2.43i 50 |
. . . 4
⊢ (dom
recs(𝐹) ∈ On →
(𝐵 ∈ dom recs(𝐹) → (𝐵 ∈ dom recs(𝐹) → (𝐶‘𝐵) = (𝐹‘(𝐶 ↾ 𝐵))))) |
25 | 24 | pm2.43d 51 |
. . 3
⊢ (dom
recs(𝐹) ∈ On →
(𝐵 ∈ dom recs(𝐹) → (𝐶‘𝐵) = (𝐹‘(𝐶 ↾ 𝐵)))) |
26 | | opex 4859 |
. . . . . . . . 9
⊢
〈𝐵, (𝐹‘(𝐶 ↾ 𝐵))〉 ∈ V |
27 | 26 | snid 4155 |
. . . . . . . 8
⊢
〈𝐵, (𝐹‘(𝐶 ↾ 𝐵))〉 ∈ {〈𝐵, (𝐹‘(𝐶 ↾ 𝐵))〉} |
28 | | opeq1 4340 |
. . . . . . . . . . 11
⊢ (𝐵 = dom recs(𝐹) → 〈𝐵, (𝐹‘(𝐶 ↾ 𝐵))〉 = 〈dom recs(𝐹), (𝐹‘(𝐶 ↾ 𝐵))〉) |
29 | 28 | adantl 481 |
. . . . . . . . . 10
⊢ ((dom
recs(𝐹) ∈ On ∧
𝐵 = dom recs(𝐹)) → 〈𝐵, (𝐹‘(𝐶 ↾ 𝐵))〉 = 〈dom recs(𝐹), (𝐹‘(𝐶 ↾ 𝐵))〉) |
30 | | eqimss 3620 |
. . . . . . . . . . . . . 14
⊢ (𝐵 = dom recs(𝐹) → 𝐵 ⊆ dom recs(𝐹)) |
31 | 8, 15 | mp3an2 1404 |
. . . . . . . . . . . . . 14
⊢ ((Fun
𝐶 ∧ 𝐵 ⊆ dom recs(𝐹)) → (𝐶 ↾ 𝐵) = (recs(𝐹) ↾ 𝐵)) |
32 | 6, 30, 31 | syl2an 493 |
. . . . . . . . . . . . 13
⊢ ((dom
recs(𝐹) ∈ On ∧
𝐵 = dom recs(𝐹)) → (𝐶 ↾ 𝐵) = (recs(𝐹) ↾ 𝐵)) |
33 | | reseq2 5312 |
. . . . . . . . . . . . . . 15
⊢ (𝐵 = dom recs(𝐹) → (recs(𝐹) ↾ 𝐵) = (recs(𝐹) ↾ dom recs(𝐹))) |
34 | 2 | tfrlem6 7365 |
. . . . . . . . . . . . . . . 16
⊢ Rel
recs(𝐹) |
35 | | resdm 5361 |
. . . . . . . . . . . . . . . 16
⊢ (Rel
recs(𝐹) → (recs(𝐹) ↾ dom recs(𝐹)) = recs(𝐹)) |
36 | 34, 35 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢
(recs(𝐹) ↾ dom
recs(𝐹)) = recs(𝐹) |
37 | 33, 36 | syl6eq 2660 |
. . . . . . . . . . . . . 14
⊢ (𝐵 = dom recs(𝐹) → (recs(𝐹) ↾ 𝐵) = recs(𝐹)) |
38 | 37 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((dom
recs(𝐹) ∈ On ∧
𝐵 = dom recs(𝐹)) → (recs(𝐹) ↾ 𝐵) = recs(𝐹)) |
39 | 32, 38 | eqtrd 2644 |
. . . . . . . . . . . 12
⊢ ((dom
recs(𝐹) ∈ On ∧
𝐵 = dom recs(𝐹)) → (𝐶 ↾ 𝐵) = recs(𝐹)) |
40 | 39 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ ((dom
recs(𝐹) ∈ On ∧
𝐵 = dom recs(𝐹)) → (𝐹‘(𝐶 ↾ 𝐵)) = (𝐹‘recs(𝐹))) |
41 | 40 | opeq2d 4347 |
. . . . . . . . . 10
⊢ ((dom
recs(𝐹) ∈ On ∧
𝐵 = dom recs(𝐹)) → 〈dom recs(𝐹), (𝐹‘(𝐶 ↾ 𝐵))〉 = 〈dom recs(𝐹), (𝐹‘recs(𝐹))〉) |
42 | 29, 41 | eqtrd 2644 |
. . . . . . . . 9
⊢ ((dom
recs(𝐹) ∈ On ∧
𝐵 = dom recs(𝐹)) → 〈𝐵, (𝐹‘(𝐶 ↾ 𝐵))〉 = 〈dom recs(𝐹), (𝐹‘recs(𝐹))〉) |
43 | 42 | sneqd 4137 |
. . . . . . . 8
⊢ ((dom
recs(𝐹) ∈ On ∧
𝐵 = dom recs(𝐹)) → {〈𝐵, (𝐹‘(𝐶 ↾ 𝐵))〉} = {〈dom recs(𝐹), (𝐹‘recs(𝐹))〉}) |
44 | 27, 43 | syl5eleq 2694 |
. . . . . . 7
⊢ ((dom
recs(𝐹) ∈ On ∧
𝐵 = dom recs(𝐹)) → 〈𝐵, (𝐹‘(𝐶 ↾ 𝐵))〉 ∈ {〈dom recs(𝐹), (𝐹‘recs(𝐹))〉}) |
45 | | elun2 3743 |
. . . . . . 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 | syl6eleqr 2699 |
. . . . 5
⊢ ((dom
recs(𝐹) ∈ On ∧
𝐵 = dom recs(𝐹)) → 〈𝐵, (𝐹‘(𝐶 ↾ 𝐵))〉 ∈ 𝐶) |
48 | 4 | adantr 480 |
. . . . . 6
⊢ ((dom
recs(𝐹) ∈ On ∧
𝐵 = dom recs(𝐹)) → 𝐶 Fn suc dom recs(𝐹)) |
49 | | simpr 476 |
. . . . . . 7
⊢ ((dom
recs(𝐹) ∈ On ∧
𝐵 = dom recs(𝐹)) → 𝐵 = dom recs(𝐹)) |
50 | | sucidg 5720 |
. . . . . . . 8
⊢ (dom
recs(𝐹) ∈ On →
dom recs(𝐹) ∈ suc dom
recs(𝐹)) |
51 | 50 | adantr 480 |
. . . . . . 7
⊢ ((dom
recs(𝐹) ∈ On ∧
𝐵 = dom recs(𝐹)) → dom recs(𝐹) ∈ suc dom recs(𝐹)) |
52 | 49, 51 | eqeltrd 2688 |
. . . . . 6
⊢ ((dom
recs(𝐹) ∈ On ∧
𝐵 = dom recs(𝐹)) → 𝐵 ∈ suc dom recs(𝐹)) |
53 | | fnopfvb 6147 |
. . . . . 6
⊢ ((𝐶 Fn suc dom recs(𝐹) ∧ 𝐵 ∈ suc dom recs(𝐹)) → ((𝐶‘𝐵) = (𝐹‘(𝐶 ↾ 𝐵)) ↔ 〈𝐵, (𝐹‘(𝐶 ↾ 𝐵))〉 ∈ 𝐶)) |
54 | 48, 52, 53 | syl2anc 691 |
. . . . 5
⊢ ((dom
recs(𝐹) ∈ On ∧
𝐵 = dom recs(𝐹)) → ((𝐶‘𝐵) = (𝐹‘(𝐶 ↾ 𝐵)) ↔ 〈𝐵, (𝐹‘(𝐶 ↾ 𝐵))〉 ∈ 𝐶)) |
55 | 47, 54 | mpbird 246 |
. . . 4
⊢ ((dom
recs(𝐹) ∈ On ∧
𝐵 = dom recs(𝐹)) → (𝐶‘𝐵) = (𝐹‘(𝐶 ↾ 𝐵))) |
56 | 55 | ex 449 |
. . 3
⊢ (dom
recs(𝐹) ∈ On →
(𝐵 = dom recs(𝐹) → (𝐶‘𝐵) = (𝐹‘(𝐶 ↾ 𝐵)))) |
57 | 25, 56 | jaod 394 |
. 2
⊢ (dom
recs(𝐹) ∈ On →
((𝐵 ∈ dom recs(𝐹) ∨ 𝐵 = dom recs(𝐹)) → (𝐶‘𝐵) = (𝐹‘(𝐶 ↾ 𝐵)))) |
58 | 1, 57 | syl5 33 |
1
⊢ (dom
recs(𝐹) ∈ On →
(𝐵 ∈ suc dom
recs(𝐹) → (𝐶‘𝐵) = (𝐹‘(𝐶 ↾ 𝐵)))) |