Step | Hyp | Ref
| Expression |
1 | | fvsnun.3 |
. . . . . 6
⊢ 𝐺 = ({⟨𝐴, 𝐵⟩} ∪ (𝐹 ↾ (𝐶 ∖ {𝐴}))) |
2 | 1 | reseq1i 5934 |
. . . . 5
⊢ (𝐺 ↾ (𝐶 ∖ {𝐴})) = (({⟨𝐴, 𝐵⟩} ∪ (𝐹 ↾ (𝐶 ∖ {𝐴}))) ↾ (𝐶 ∖ {𝐴})) |
3 | 2 | a1i 11 |
. . . 4
⊢ (𝜑 → (𝐺 ↾ (𝐶 ∖ {𝐴})) = (({⟨𝐴, 𝐵⟩} ∪ (𝐹 ↾ (𝐶 ∖ {𝐴}))) ↾ (𝐶 ∖ {𝐴}))) |
4 | | resundir 5953 |
. . . . 5
⊢
(({⟨𝐴, 𝐵⟩} ∪ (𝐹 ↾ (𝐶 ∖ {𝐴}))) ↾ (𝐶 ∖ {𝐴})) = (({⟨𝐴, 𝐵⟩} ↾ (𝐶 ∖ {𝐴})) ∪ ((𝐹 ↾ (𝐶 ∖ {𝐴})) ↾ (𝐶 ∖ {𝐴}))) |
5 | 4 | a1i 11 |
. . . 4
⊢ (𝜑 → (({⟨𝐴, 𝐵⟩} ∪ (𝐹 ↾ (𝐶 ∖ {𝐴}))) ↾ (𝐶 ∖ {𝐴})) = (({⟨𝐴, 𝐵⟩} ↾ (𝐶 ∖ {𝐴})) ∪ ((𝐹 ↾ (𝐶 ∖ {𝐴})) ↾ (𝐶 ∖ {𝐴})))) |
6 | | disjdif 4432 |
. . . . . . 7
⊢ ({𝐴} ∩ (𝐶 ∖ {𝐴})) = ∅ |
7 | | fvsnun.1 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
8 | | fvsnun.2 |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 ∈ 𝑊) |
9 | | fnsng 6554 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {⟨𝐴, 𝐵⟩} Fn {𝐴}) |
10 | 7, 8, 9 | syl2anc 585 |
. . . . . . . 8
⊢ (𝜑 → {⟨𝐴, 𝐵⟩} Fn {𝐴}) |
11 | | fnresdisj 6622 |
. . . . . . . 8
⊢
({⟨𝐴, 𝐵⟩} Fn {𝐴} → (({𝐴} ∩ (𝐶 ∖ {𝐴})) = ∅ ↔ ({⟨𝐴, 𝐵⟩} ↾ (𝐶 ∖ {𝐴})) = ∅)) |
12 | 10, 11 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (({𝐴} ∩ (𝐶 ∖ {𝐴})) = ∅ ↔ ({⟨𝐴, 𝐵⟩} ↾ (𝐶 ∖ {𝐴})) = ∅)) |
13 | 6, 12 | mpbii 232 |
. . . . . 6
⊢ (𝜑 → ({⟨𝐴, 𝐵⟩} ↾ (𝐶 ∖ {𝐴})) = ∅) |
14 | | residm 5971 |
. . . . . . 7
⊢ ((𝐹 ↾ (𝐶 ∖ {𝐴})) ↾ (𝐶 ∖ {𝐴})) = (𝐹 ↾ (𝐶 ∖ {𝐴})) |
15 | 14 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ((𝐹 ↾ (𝐶 ∖ {𝐴})) ↾ (𝐶 ∖ {𝐴})) = (𝐹 ↾ (𝐶 ∖ {𝐴}))) |
16 | 13, 15 | uneq12d 4125 |
. . . . 5
⊢ (𝜑 → (({⟨𝐴, 𝐵⟩} ↾ (𝐶 ∖ {𝐴})) ∪ ((𝐹 ↾ (𝐶 ∖ {𝐴})) ↾ (𝐶 ∖ {𝐴}))) = (∅ ∪ (𝐹 ↾ (𝐶 ∖ {𝐴})))) |
17 | | uncom 4114 |
. . . . . 6
⊢ (∅
∪ (𝐹 ↾ (𝐶 ∖ {𝐴}))) = ((𝐹 ↾ (𝐶 ∖ {𝐴})) ∪ ∅) |
18 | 17 | a1i 11 |
. . . . 5
⊢ (𝜑 → (∅ ∪ (𝐹 ↾ (𝐶 ∖ {𝐴}))) = ((𝐹 ↾ (𝐶 ∖ {𝐴})) ∪ ∅)) |
19 | | un0 4351 |
. . . . . 6
⊢ ((𝐹 ↾ (𝐶 ∖ {𝐴})) ∪ ∅) = (𝐹 ↾ (𝐶 ∖ {𝐴})) |
20 | 19 | a1i 11 |
. . . . 5
⊢ (𝜑 → ((𝐹 ↾ (𝐶 ∖ {𝐴})) ∪ ∅) = (𝐹 ↾ (𝐶 ∖ {𝐴}))) |
21 | 16, 18, 20 | 3eqtrd 2777 |
. . . 4
⊢ (𝜑 → (({⟨𝐴, 𝐵⟩} ↾ (𝐶 ∖ {𝐴})) ∪ ((𝐹 ↾ (𝐶 ∖ {𝐴})) ↾ (𝐶 ∖ {𝐴}))) = (𝐹 ↾ (𝐶 ∖ {𝐴}))) |
22 | 3, 5, 21 | 3eqtrd 2777 |
. . 3
⊢ (𝜑 → (𝐺 ↾ (𝐶 ∖ {𝐴})) = (𝐹 ↾ (𝐶 ∖ {𝐴}))) |
23 | 22 | fveq1d 6845 |
. 2
⊢ (𝜑 → ((𝐺 ↾ (𝐶 ∖ {𝐴}))‘𝐷) = ((𝐹 ↾ (𝐶 ∖ {𝐴}))‘𝐷)) |
24 | | fvsnun2.4 |
. . 3
⊢ (𝜑 → 𝐷 ∈ (𝐶 ∖ {𝐴})) |
25 | 24 | fvresd 6863 |
. 2
⊢ (𝜑 → ((𝐺 ↾ (𝐶 ∖ {𝐴}))‘𝐷) = (𝐺‘𝐷)) |
26 | 24 | fvresd 6863 |
. 2
⊢ (𝜑 → ((𝐹 ↾ (𝐶 ∖ {𝐴}))‘𝐷) = (𝐹‘𝐷)) |
27 | 23, 25, 26 | 3eqtr3d 2781 |
1
⊢ (𝜑 → (𝐺‘𝐷) = (𝐹‘𝐷)) |