Proof of Theorem fvsnun2
| Step | Hyp | Ref
| Expression |
| 1 | | fvsnun.3 |
. . . . . 6
⊢ 𝐺 = ({〈𝐴, 𝐵〉} ∪ (𝐹 ↾ (𝐶 ∖ {𝐴}))) |
| 2 | 1 | reseq1i 5993 |
. . . . 5
⊢ (𝐺 ↾ (𝐶 ∖ {𝐴})) = (({〈𝐴, 𝐵〉} ∪ (𝐹 ↾ (𝐶 ∖ {𝐴}))) ↾ (𝐶 ∖ {𝐴})) |
| 3 | 2 | a1i 11 |
. . . 4
⊢ (𝜑 → (𝐺 ↾ (𝐶 ∖ {𝐴})) = (({〈𝐴, 𝐵〉} ∪ (𝐹 ↾ (𝐶 ∖ {𝐴}))) ↾ (𝐶 ∖ {𝐴}))) |
| 4 | | resundir 6012 |
. . . . 5
⊢
(({〈𝐴, 𝐵〉} ∪ (𝐹 ↾ (𝐶 ∖ {𝐴}))) ↾ (𝐶 ∖ {𝐴})) = (({〈𝐴, 𝐵〉} ↾ (𝐶 ∖ {𝐴})) ∪ ((𝐹 ↾ (𝐶 ∖ {𝐴})) ↾ (𝐶 ∖ {𝐴}))) |
| 5 | 4 | a1i 11 |
. . . 4
⊢ (𝜑 → (({〈𝐴, 𝐵〉} ∪ (𝐹 ↾ (𝐶 ∖ {𝐴}))) ↾ (𝐶 ∖ {𝐴})) = (({〈𝐴, 𝐵〉} ↾ (𝐶 ∖ {𝐴})) ∪ ((𝐹 ↾ (𝐶 ∖ {𝐴})) ↾ (𝐶 ∖ {𝐴})))) |
| 6 | | disjdif 4472 |
. . . . . . 7
⊢ ({𝐴} ∩ (𝐶 ∖ {𝐴})) = ∅ |
| 7 | | fvsnun.1 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
| 8 | | fvsnun.2 |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 ∈ 𝑊) |
| 9 | | fnsng 6618 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {〈𝐴, 𝐵〉} Fn {𝐴}) |
| 10 | 7, 8, 9 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 → {〈𝐴, 𝐵〉} Fn {𝐴}) |
| 11 | | fnresdisj 6688 |
. . . . . . . 8
⊢
({〈𝐴, 𝐵〉} Fn {𝐴} → (({𝐴} ∩ (𝐶 ∖ {𝐴})) = ∅ ↔ ({〈𝐴, 𝐵〉} ↾ (𝐶 ∖ {𝐴})) = ∅)) |
| 12 | 10, 11 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (({𝐴} ∩ (𝐶 ∖ {𝐴})) = ∅ ↔ ({〈𝐴, 𝐵〉} ↾ (𝐶 ∖ {𝐴})) = ∅)) |
| 13 | 6, 12 | mpbii 233 |
. . . . . 6
⊢ (𝜑 → ({〈𝐴, 𝐵〉} ↾ (𝐶 ∖ {𝐴})) = ∅) |
| 14 | | residm 6028 |
. . . . . . 7
⊢ ((𝐹 ↾ (𝐶 ∖ {𝐴})) ↾ (𝐶 ∖ {𝐴})) = (𝐹 ↾ (𝐶 ∖ {𝐴})) |
| 15 | 14 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ((𝐹 ↾ (𝐶 ∖ {𝐴})) ↾ (𝐶 ∖ {𝐴})) = (𝐹 ↾ (𝐶 ∖ {𝐴}))) |
| 16 | 13, 15 | uneq12d 4169 |
. . . . 5
⊢ (𝜑 → (({〈𝐴, 𝐵〉} ↾ (𝐶 ∖ {𝐴})) ∪ ((𝐹 ↾ (𝐶 ∖ {𝐴})) ↾ (𝐶 ∖ {𝐴}))) = (∅ ∪ (𝐹 ↾ (𝐶 ∖ {𝐴})))) |
| 17 | | uncom 4158 |
. . . . . 6
⊢ (∅
∪ (𝐹 ↾ (𝐶 ∖ {𝐴}))) = ((𝐹 ↾ (𝐶 ∖ {𝐴})) ∪ ∅) |
| 18 | 17 | a1i 11 |
. . . . 5
⊢ (𝜑 → (∅ ∪ (𝐹 ↾ (𝐶 ∖ {𝐴}))) = ((𝐹 ↾ (𝐶 ∖ {𝐴})) ∪ ∅)) |
| 19 | | un0 4394 |
. . . . . 6
⊢ ((𝐹 ↾ (𝐶 ∖ {𝐴})) ∪ ∅) = (𝐹 ↾ (𝐶 ∖ {𝐴})) |
| 20 | 19 | a1i 11 |
. . . . 5
⊢ (𝜑 → ((𝐹 ↾ (𝐶 ∖ {𝐴})) ∪ ∅) = (𝐹 ↾ (𝐶 ∖ {𝐴}))) |
| 21 | 16, 18, 20 | 3eqtrd 2781 |
. . . 4
⊢ (𝜑 → (({〈𝐴, 𝐵〉} ↾ (𝐶 ∖ {𝐴})) ∪ ((𝐹 ↾ (𝐶 ∖ {𝐴})) ↾ (𝐶 ∖ {𝐴}))) = (𝐹 ↾ (𝐶 ∖ {𝐴}))) |
| 22 | 3, 5, 21 | 3eqtrd 2781 |
. . 3
⊢ (𝜑 → (𝐺 ↾ (𝐶 ∖ {𝐴})) = (𝐹 ↾ (𝐶 ∖ {𝐴}))) |
| 23 | 22 | fveq1d 6908 |
. 2
⊢ (𝜑 → ((𝐺 ↾ (𝐶 ∖ {𝐴}))‘𝐷) = ((𝐹 ↾ (𝐶 ∖ {𝐴}))‘𝐷)) |
| 24 | | fvsnun2.4 |
. . 3
⊢ (𝜑 → 𝐷 ∈ (𝐶 ∖ {𝐴})) |
| 25 | 24 | fvresd 6926 |
. 2
⊢ (𝜑 → ((𝐺 ↾ (𝐶 ∖ {𝐴}))‘𝐷) = (𝐺‘𝐷)) |
| 26 | 24 | fvresd 6926 |
. 2
⊢ (𝜑 → ((𝐹 ↾ (𝐶 ∖ {𝐴}))‘𝐷) = (𝐹‘𝐷)) |
| 27 | 23, 25, 26 | 3eqtr3d 2785 |
1
⊢ (𝜑 → (𝐺‘𝐷) = (𝐹‘𝐷)) |