Step | Hyp | Ref
| Expression |
1 | | eleq1w 2822 |
. . . 4
⊢ (𝑞 = ℎ → (𝑞 ∈ 𝐶 ↔ ℎ ∈ 𝐶)) |
2 | 1 | 3anbi3d 1440 |
. . 3
⊢ (𝑞 = ℎ → ((𝑅 FrSe 𝐴 ∧ 𝑔 ∈ 𝐶 ∧ 𝑞 ∈ 𝐶) ↔ (𝑅 FrSe 𝐴 ∧ 𝑔 ∈ 𝐶 ∧ ℎ ∈ 𝐶))) |
3 | | dmeq 5809 |
. . . . . . 7
⊢ (𝑞 = ℎ → dom 𝑞 = dom ℎ) |
4 | 3 | ineq2d 4151 |
. . . . . 6
⊢ (𝑞 = ℎ → (dom 𝑔 ∩ dom 𝑞) = (dom 𝑔 ∩ dom ℎ)) |
5 | 4 | reseq2d 5888 |
. . . . 5
⊢ (𝑞 = ℎ → (𝑔 ↾ (dom 𝑔 ∩ dom 𝑞)) = (𝑔 ↾ (dom 𝑔 ∩ dom ℎ))) |
6 | | bnj1326.4 |
. . . . . 6
⊢ 𝐷 = (dom 𝑔 ∩ dom ℎ) |
7 | 6 | reseq2i 5885 |
. . . . 5
⊢ (𝑔 ↾ 𝐷) = (𝑔 ↾ (dom 𝑔 ∩ dom ℎ)) |
8 | 5, 7 | eqtr4di 2797 |
. . . 4
⊢ (𝑞 = ℎ → (𝑔 ↾ (dom 𝑔 ∩ dom 𝑞)) = (𝑔 ↾ 𝐷)) |
9 | 4 | reseq2d 5888 |
. . . . . 6
⊢ (𝑞 = ℎ → (𝑞 ↾ (dom 𝑔 ∩ dom 𝑞)) = (𝑞 ↾ (dom 𝑔 ∩ dom ℎ))) |
10 | | reseq1 5882 |
. . . . . 6
⊢ (𝑞 = ℎ → (𝑞 ↾ (dom 𝑔 ∩ dom ℎ)) = (ℎ ↾ (dom 𝑔 ∩ dom ℎ))) |
11 | 9, 10 | eqtrd 2779 |
. . . . 5
⊢ (𝑞 = ℎ → (𝑞 ↾ (dom 𝑔 ∩ dom 𝑞)) = (ℎ ↾ (dom 𝑔 ∩ dom ℎ))) |
12 | 6 | reseq2i 5885 |
. . . . 5
⊢ (ℎ ↾ 𝐷) = (ℎ ↾ (dom 𝑔 ∩ dom ℎ)) |
13 | 11, 12 | eqtr4di 2797 |
. . . 4
⊢ (𝑞 = ℎ → (𝑞 ↾ (dom 𝑔 ∩ dom 𝑞)) = (ℎ ↾ 𝐷)) |
14 | 8, 13 | eqeq12d 2755 |
. . 3
⊢ (𝑞 = ℎ → ((𝑔 ↾ (dom 𝑔 ∩ dom 𝑞)) = (𝑞 ↾ (dom 𝑔 ∩ dom 𝑞)) ↔ (𝑔 ↾ 𝐷) = (ℎ ↾ 𝐷))) |
15 | 2, 14 | imbi12d 344 |
. 2
⊢ (𝑞 = ℎ → (((𝑅 FrSe 𝐴 ∧ 𝑔 ∈ 𝐶 ∧ 𝑞 ∈ 𝐶) → (𝑔 ↾ (dom 𝑔 ∩ dom 𝑞)) = (𝑞 ↾ (dom 𝑔 ∩ dom 𝑞))) ↔ ((𝑅 FrSe 𝐴 ∧ 𝑔 ∈ 𝐶 ∧ ℎ ∈ 𝐶) → (𝑔 ↾ 𝐷) = (ℎ ↾ 𝐷)))) |
16 | | eleq1w 2822 |
. . . . 5
⊢ (𝑝 = 𝑔 → (𝑝 ∈ 𝐶 ↔ 𝑔 ∈ 𝐶)) |
17 | 16 | 3anbi2d 1439 |
. . . 4
⊢ (𝑝 = 𝑔 → ((𝑅 FrSe 𝐴 ∧ 𝑝 ∈ 𝐶 ∧ 𝑞 ∈ 𝐶) ↔ (𝑅 FrSe 𝐴 ∧ 𝑔 ∈ 𝐶 ∧ 𝑞 ∈ 𝐶))) |
18 | | dmeq 5809 |
. . . . . . . 8
⊢ (𝑝 = 𝑔 → dom 𝑝 = dom 𝑔) |
19 | 18 | ineq1d 4150 |
. . . . . . 7
⊢ (𝑝 = 𝑔 → (dom 𝑝 ∩ dom 𝑞) = (dom 𝑔 ∩ dom 𝑞)) |
20 | 19 | reseq2d 5888 |
. . . . . 6
⊢ (𝑝 = 𝑔 → (𝑝 ↾ (dom 𝑝 ∩ dom 𝑞)) = (𝑝 ↾ (dom 𝑔 ∩ dom 𝑞))) |
21 | | reseq1 5882 |
. . . . . 6
⊢ (𝑝 = 𝑔 → (𝑝 ↾ (dom 𝑔 ∩ dom 𝑞)) = (𝑔 ↾ (dom 𝑔 ∩ dom 𝑞))) |
22 | 20, 21 | eqtrd 2779 |
. . . . 5
⊢ (𝑝 = 𝑔 → (𝑝 ↾ (dom 𝑝 ∩ dom 𝑞)) = (𝑔 ↾ (dom 𝑔 ∩ dom 𝑞))) |
23 | 19 | reseq2d 5888 |
. . . . 5
⊢ (𝑝 = 𝑔 → (𝑞 ↾ (dom 𝑝 ∩ dom 𝑞)) = (𝑞 ↾ (dom 𝑔 ∩ dom 𝑞))) |
24 | 22, 23 | eqeq12d 2755 |
. . . 4
⊢ (𝑝 = 𝑔 → ((𝑝 ↾ (dom 𝑝 ∩ dom 𝑞)) = (𝑞 ↾ (dom 𝑝 ∩ dom 𝑞)) ↔ (𝑔 ↾ (dom 𝑔 ∩ dom 𝑞)) = (𝑞 ↾ (dom 𝑔 ∩ dom 𝑞)))) |
25 | 17, 24 | imbi12d 344 |
. . 3
⊢ (𝑝 = 𝑔 → (((𝑅 FrSe 𝐴 ∧ 𝑝 ∈ 𝐶 ∧ 𝑞 ∈ 𝐶) → (𝑝 ↾ (dom 𝑝 ∩ dom 𝑞)) = (𝑞 ↾ (dom 𝑝 ∩ dom 𝑞))) ↔ ((𝑅 FrSe 𝐴 ∧ 𝑔 ∈ 𝐶 ∧ 𝑞 ∈ 𝐶) → (𝑔 ↾ (dom 𝑔 ∩ dom 𝑞)) = (𝑞 ↾ (dom 𝑔 ∩ dom 𝑞))))) |
26 | | bnj1326.1 |
. . . 4
⊢ 𝐵 = {𝑑 ∣ (𝑑 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝑑 pred(𝑥, 𝐴, 𝑅) ⊆ 𝑑)} |
27 | | bnj1326.2 |
. . . 4
⊢ 𝑌 = 〈𝑥, (𝑓 ↾ pred(𝑥, 𝐴, 𝑅))〉 |
28 | | bnj1326.3 |
. . . 4
⊢ 𝐶 = {𝑓 ∣ ∃𝑑 ∈ 𝐵 (𝑓 Fn 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))} |
29 | | eqid 2739 |
. . . 4
⊢ (dom
𝑝 ∩ dom 𝑞) = (dom 𝑝 ∩ dom 𝑞) |
30 | 26, 27, 28, 29 | bnj1311 32983 |
. . 3
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑝 ∈ 𝐶 ∧ 𝑞 ∈ 𝐶) → (𝑝 ↾ (dom 𝑝 ∩ dom 𝑞)) = (𝑞 ↾ (dom 𝑝 ∩ dom 𝑞))) |
31 | 25, 30 | chvarvv 2005 |
. 2
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑔 ∈ 𝐶 ∧ 𝑞 ∈ 𝐶) → (𝑔 ↾ (dom 𝑔 ∩ dom 𝑞)) = (𝑞 ↾ (dom 𝑔 ∩ dom 𝑞))) |
32 | 15, 31 | chvarvv 2005 |
1
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑔 ∈ 𝐶 ∧ ℎ ∈ 𝐶) → (𝑔 ↾ 𝐷) = (ℎ ↾ 𝐷)) |