Step | Hyp | Ref
| Expression |
1 | | wfrlem13OLD.1 |
. . 3
⊢ 𝑅 We 𝐴 |
2 | | wfrlem13OLD.2 |
. . 3
⊢ 𝑅 Se 𝐴 |
3 | | wfrlem13OLD.3 |
. . 3
⊢ 𝐹 = wrecs(𝑅, 𝐴, 𝐺) |
4 | | wfrlem13OLD.4 |
. . 3
⊢ 𝐶 = (𝐹 ∪ {⟨𝑧, (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}) |
5 | 1, 2, 3, 4 | wfrlem13OLD 8268 |
. 2
⊢ (𝑧 ∈ (𝐴 ∖ dom 𝐹) → 𝐶 Fn (dom 𝐹 ∪ {𝑧})) |
6 | | elun 4109 |
. . . 4
⊢ (𝑦 ∈ (dom 𝐹 ∪ {𝑧}) ↔ (𝑦 ∈ dom 𝐹 ∨ 𝑦 ∈ {𝑧})) |
7 | | velsn 4603 |
. . . . 5
⊢ (𝑦 ∈ {𝑧} ↔ 𝑦 = 𝑧) |
8 | 7 | orbi2i 912 |
. . . 4
⊢ ((𝑦 ∈ dom 𝐹 ∨ 𝑦 ∈ {𝑧}) ↔ (𝑦 ∈ dom 𝐹 ∨ 𝑦 = 𝑧)) |
9 | 6, 8 | bitri 275 |
. . 3
⊢ (𝑦 ∈ (dom 𝐹 ∪ {𝑧}) ↔ (𝑦 ∈ dom 𝐹 ∨ 𝑦 = 𝑧)) |
10 | 1, 2, 3 | wfrlem12OLD 8267 |
. . . . . . 7
⊢ (𝑦 ∈ dom 𝐹 → (𝐹‘𝑦) = (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦)))) |
11 | | fnfun 6603 |
. . . . . . . 8
⊢ (𝐶 Fn (dom 𝐹 ∪ {𝑧}) → Fun 𝐶) |
12 | | ssun1 4133 |
. . . . . . . . . 10
⊢ 𝐹 ⊆ (𝐹 ∪ {⟨𝑧, (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}) |
13 | 12, 4 | sseqtrri 3982 |
. . . . . . . . 9
⊢ 𝐹 ⊆ 𝐶 |
14 | | funssfv 6864 |
. . . . . . . . . 10
⊢ ((Fun
𝐶 ∧ 𝐹 ⊆ 𝐶 ∧ 𝑦 ∈ dom 𝐹) → (𝐶‘𝑦) = (𝐹‘𝑦)) |
15 | 3 | wfrdmclOLD 8264 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ dom 𝐹 → Pred(𝑅, 𝐴, 𝑦) ⊆ dom 𝐹) |
16 | | fun2ssres 6547 |
. . . . . . . . . . . 12
⊢ ((Fun
𝐶 ∧ 𝐹 ⊆ 𝐶 ∧ Pred(𝑅, 𝐴, 𝑦) ⊆ dom 𝐹) → (𝐶 ↾ Pred(𝑅, 𝐴, 𝑦)) = (𝐹 ↾ Pred(𝑅, 𝐴, 𝑦))) |
17 | 15, 16 | syl3an3 1166 |
. . . . . . . . . . 11
⊢ ((Fun
𝐶 ∧ 𝐹 ⊆ 𝐶 ∧ 𝑦 ∈ dom 𝐹) → (𝐶 ↾ Pred(𝑅, 𝐴, 𝑦)) = (𝐹 ↾ Pred(𝑅, 𝐴, 𝑦))) |
18 | 17 | fveq2d 6847 |
. . . . . . . . . 10
⊢ ((Fun
𝐶 ∧ 𝐹 ⊆ 𝐶 ∧ 𝑦 ∈ dom 𝐹) → (𝐺‘(𝐶 ↾ Pred(𝑅, 𝐴, 𝑦))) = (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦)))) |
19 | 14, 18 | eqeq12d 2753 |
. . . . . . . . 9
⊢ ((Fun
𝐶 ∧ 𝐹 ⊆ 𝐶 ∧ 𝑦 ∈ dom 𝐹) → ((𝐶‘𝑦) = (𝐺‘(𝐶 ↾ Pred(𝑅, 𝐴, 𝑦))) ↔ (𝐹‘𝑦) = (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦))))) |
20 | 13, 19 | mp3an2 1450 |
. . . . . . . 8
⊢ ((Fun
𝐶 ∧ 𝑦 ∈ dom 𝐹) → ((𝐶‘𝑦) = (𝐺‘(𝐶 ↾ Pred(𝑅, 𝐴, 𝑦))) ↔ (𝐹‘𝑦) = (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦))))) |
21 | 11, 20 | sylan 581 |
. . . . . . 7
⊢ ((𝐶 Fn (dom 𝐹 ∪ {𝑧}) ∧ 𝑦 ∈ dom 𝐹) → ((𝐶‘𝑦) = (𝐺‘(𝐶 ↾ Pred(𝑅, 𝐴, 𝑦))) ↔ (𝐹‘𝑦) = (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦))))) |
22 | 10, 21 | syl5ibr 246 |
. . . . . 6
⊢ ((𝐶 Fn (dom 𝐹 ∪ {𝑧}) ∧ 𝑦 ∈ dom 𝐹) → (𝑦 ∈ dom 𝐹 → (𝐶‘𝑦) = (𝐺‘(𝐶 ↾ Pred(𝑅, 𝐴, 𝑦))))) |
23 | 22 | ex 414 |
. . . . 5
⊢ (𝐶 Fn (dom 𝐹 ∪ {𝑧}) → (𝑦 ∈ dom 𝐹 → (𝑦 ∈ dom 𝐹 → (𝐶‘𝑦) = (𝐺‘(𝐶 ↾ Pred(𝑅, 𝐴, 𝑦)))))) |
24 | 23 | pm2.43d 53 |
. . . 4
⊢ (𝐶 Fn (dom 𝐹 ∪ {𝑧}) → (𝑦 ∈ dom 𝐹 → (𝐶‘𝑦) = (𝐺‘(𝐶 ↾ Pred(𝑅, 𝐴, 𝑦))))) |
25 | | vsnid 4624 |
. . . . . . 7
⊢ 𝑧 ∈ {𝑧} |
26 | | elun2 4138 |
. . . . . . 7
⊢ (𝑧 ∈ {𝑧} → 𝑧 ∈ (dom 𝐹 ∪ {𝑧})) |
27 | 25, 26 | ax-mp 5 |
. . . . . 6
⊢ 𝑧 ∈ (dom 𝐹 ∪ {𝑧}) |
28 | 4 | reseq1i 5934 |
. . . . . . . . . . . . 13
⊢ (𝐶 ↾ Pred(𝑅, 𝐴, 𝑧)) = ((𝐹 ∪ {⟨𝑧, (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}) ↾ Pred(𝑅, 𝐴, 𝑧)) |
29 | | resundir 5953 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∪ {⟨𝑧, (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}) ↾ Pred(𝑅, 𝐴, 𝑧)) = ((𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)) ∪ ({⟨𝑧, (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} ↾ Pred(𝑅, 𝐴, 𝑧))) |
30 | | wefr 5624 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑅 We 𝐴 → 𝑅 Fr 𝐴) |
31 | 1, 30 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢ 𝑅 Fr 𝐴 |
32 | | predfrirr 6289 |
. . . . . . . . . . . . . . . 16
⊢ (𝑅 Fr 𝐴 → ¬ 𝑧 ∈ Pred(𝑅, 𝐴, 𝑧)) |
33 | | ressnop0 7100 |
. . . . . . . . . . . . . . . 16
⊢ (¬
𝑧 ∈ Pred(𝑅, 𝐴, 𝑧) → ({⟨𝑧, (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} ↾ Pred(𝑅, 𝐴, 𝑧)) = ∅) |
34 | 31, 32, 33 | mp2b 10 |
. . . . . . . . . . . . . . 15
⊢
({⟨𝑧, (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} ↾ Pred(𝑅, 𝐴, 𝑧)) = ∅ |
35 | 34 | uneq2i 4121 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)) ∪ ({⟨𝑧, (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} ↾ Pred(𝑅, 𝐴, 𝑧))) = ((𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)) ∪ ∅) |
36 | | un0 4351 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)) ∪ ∅) = (𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)) |
37 | 35, 36 | eqtri 2765 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)) ∪ ({⟨𝑧, (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} ↾ Pred(𝑅, 𝐴, 𝑧))) = (𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)) |
38 | 28, 29, 37 | 3eqtri 2769 |
. . . . . . . . . . . 12
⊢ (𝐶 ↾ Pred(𝑅, 𝐴, 𝑧)) = (𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)) |
39 | 38 | fveq2i 6846 |
. . . . . . . . . . 11
⊢ (𝐺‘(𝐶 ↾ Pred(𝑅, 𝐴, 𝑧))) = (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧))) |
40 | 39 | opeq2i 4835 |
. . . . . . . . . 10
⊢
⟨𝑧, (𝐺‘(𝐶 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩ = ⟨𝑧, (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩ |
41 | | opex 5422 |
. . . . . . . . . . 11
⊢
⟨𝑧, (𝐺‘(𝐶 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩ ∈ V |
42 | 41 | elsn 4602 |
. . . . . . . . . 10
⊢
(⟨𝑧, (𝐺‘(𝐶 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩ ∈ {⟨𝑧, (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} ↔ ⟨𝑧, (𝐺‘(𝐶 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩ = ⟨𝑧, (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩) |
43 | 40, 42 | mpbir 230 |
. . . . . . . . 9
⊢
⟨𝑧, (𝐺‘(𝐶 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩ ∈ {⟨𝑧, (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} |
44 | | elun2 4138 |
. . . . . . . . 9
⊢
(⟨𝑧, (𝐺‘(𝐶 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩ ∈ {⟨𝑧, (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} → ⟨𝑧, (𝐺‘(𝐶 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩ ∈ (𝐹 ∪ {⟨𝑧, (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩})) |
45 | 43, 44 | ax-mp 5 |
. . . . . . . 8
⊢
⟨𝑧, (𝐺‘(𝐶 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩ ∈ (𝐹 ∪ {⟨𝑧, (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}) |
46 | 45, 4 | eleqtrri 2837 |
. . . . . . 7
⊢
⟨𝑧, (𝐺‘(𝐶 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩ ∈ 𝐶 |
47 | | fnopfvb 6897 |
. . . . . . 7
⊢ ((𝐶 Fn (dom 𝐹 ∪ {𝑧}) ∧ 𝑧 ∈ (dom 𝐹 ∪ {𝑧})) → ((𝐶‘𝑧) = (𝐺‘(𝐶 ↾ Pred(𝑅, 𝐴, 𝑧))) ↔ ⟨𝑧, (𝐺‘(𝐶 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩ ∈ 𝐶)) |
48 | 46, 47 | mpbiri 258 |
. . . . . 6
⊢ ((𝐶 Fn (dom 𝐹 ∪ {𝑧}) ∧ 𝑧 ∈ (dom 𝐹 ∪ {𝑧})) → (𝐶‘𝑧) = (𝐺‘(𝐶 ↾ Pred(𝑅, 𝐴, 𝑧)))) |
49 | 27, 48 | mpan2 690 |
. . . . 5
⊢ (𝐶 Fn (dom 𝐹 ∪ {𝑧}) → (𝐶‘𝑧) = (𝐺‘(𝐶 ↾ Pred(𝑅, 𝐴, 𝑧)))) |
50 | | fveq2 6843 |
. . . . . 6
⊢ (𝑦 = 𝑧 → (𝐶‘𝑦) = (𝐶‘𝑧)) |
51 | | predeq3 6258 |
. . . . . . . 8
⊢ (𝑦 = 𝑧 → Pred(𝑅, 𝐴, 𝑦) = Pred(𝑅, 𝐴, 𝑧)) |
52 | 51 | reseq2d 5938 |
. . . . . . 7
⊢ (𝑦 = 𝑧 → (𝐶 ↾ Pred(𝑅, 𝐴, 𝑦)) = (𝐶 ↾ Pred(𝑅, 𝐴, 𝑧))) |
53 | 52 | fveq2d 6847 |
. . . . . 6
⊢ (𝑦 = 𝑧 → (𝐺‘(𝐶 ↾ Pred(𝑅, 𝐴, 𝑦))) = (𝐺‘(𝐶 ↾ Pred(𝑅, 𝐴, 𝑧)))) |
54 | 50, 53 | eqeq12d 2753 |
. . . . 5
⊢ (𝑦 = 𝑧 → ((𝐶‘𝑦) = (𝐺‘(𝐶 ↾ Pred(𝑅, 𝐴, 𝑦))) ↔ (𝐶‘𝑧) = (𝐺‘(𝐶 ↾ Pred(𝑅, 𝐴, 𝑧))))) |
55 | 49, 54 | syl5ibrcom 247 |
. . . 4
⊢ (𝐶 Fn (dom 𝐹 ∪ {𝑧}) → (𝑦 = 𝑧 → (𝐶‘𝑦) = (𝐺‘(𝐶 ↾ Pred(𝑅, 𝐴, 𝑦))))) |
56 | 24, 55 | jaod 858 |
. . 3
⊢ (𝐶 Fn (dom 𝐹 ∪ {𝑧}) → ((𝑦 ∈ dom 𝐹 ∨ 𝑦 = 𝑧) → (𝐶‘𝑦) = (𝐺‘(𝐶 ↾ Pred(𝑅, 𝐴, 𝑦))))) |
57 | 9, 56 | biimtrid 241 |
. 2
⊢ (𝐶 Fn (dom 𝐹 ∪ {𝑧}) → (𝑦 ∈ (dom 𝐹 ∪ {𝑧}) → (𝐶‘𝑦) = (𝐺‘(𝐶 ↾ Pred(𝑅, 𝐴, 𝑦))))) |
58 | 5, 57 | syl 17 |
1
⊢ (𝑧 ∈ (𝐴 ∖ dom 𝐹) → (𝑦 ∈ (dom 𝐹 ∪ {𝑧}) → (𝐶‘𝑦) = (𝐺‘(𝐶 ↾ Pred(𝑅, 𝐴, 𝑦))))) |