Proof of Theorem fsnunfv
Step | Hyp | Ref
| Expression |
1 | | dmres 5419 |
. . . . . . . . 9
⊢ dom
(𝐹 ↾ {𝑋}) = ({𝑋} ∩ dom 𝐹) |
2 | | incom 3805 |
. . . . . . . . 9
⊢ ({𝑋} ∩ dom 𝐹) = (dom 𝐹 ∩ {𝑋}) |
3 | 1, 2 | eqtri 2644 |
. . . . . . . 8
⊢ dom
(𝐹 ↾ {𝑋}) = (dom 𝐹 ∩ {𝑋}) |
4 | | disjsn 4246 |
. . . . . . . . 9
⊢ ((dom
𝐹 ∩ {𝑋}) = ∅ ↔ ¬ 𝑋 ∈ dom 𝐹) |
5 | 4 | biimpri 218 |
. . . . . . . 8
⊢ (¬
𝑋 ∈ dom 𝐹 → (dom 𝐹 ∩ {𝑋}) = ∅) |
6 | 3, 5 | syl5eq 2668 |
. . . . . . 7
⊢ (¬
𝑋 ∈ dom 𝐹 → dom (𝐹 ↾ {𝑋}) = ∅) |
7 | 6 | 3ad2ant3 1084 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐹) → dom (𝐹 ↾ {𝑋}) = ∅) |
8 | | relres 5426 |
. . . . . . 7
⊢ Rel
(𝐹 ↾ {𝑋}) |
9 | | reldm0 5343 |
. . . . . . 7
⊢ (Rel
(𝐹 ↾ {𝑋}) → ((𝐹 ↾ {𝑋}) = ∅ ↔ dom (𝐹 ↾ {𝑋}) = ∅)) |
10 | 8, 9 | ax-mp 5 |
. . . . . 6
⊢ ((𝐹 ↾ {𝑋}) = ∅ ↔ dom (𝐹 ↾ {𝑋}) = ∅) |
11 | 7, 10 | sylibr 224 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐹) → (𝐹 ↾ {𝑋}) = ∅) |
12 | | fnsng 5938 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → {〈𝑋, 𝑌〉} Fn {𝑋}) |
13 | 12 | 3adant3 1081 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐹) → {〈𝑋, 𝑌〉} Fn {𝑋}) |
14 | | fnresdm 6000 |
. . . . . 6
⊢
({〈𝑋, 𝑌〉} Fn {𝑋} → ({〈𝑋, 𝑌〉} ↾ {𝑋}) = {〈𝑋, 𝑌〉}) |
15 | 13, 14 | syl 17 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐹) → ({〈𝑋, 𝑌〉} ↾ {𝑋}) = {〈𝑋, 𝑌〉}) |
16 | 11, 15 | uneq12d 3768 |
. . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐹) → ((𝐹 ↾ {𝑋}) ∪ ({〈𝑋, 𝑌〉} ↾ {𝑋})) = (∅ ∪ {〈𝑋, 𝑌〉})) |
17 | | resundir 5411 |
. . . 4
⊢ ((𝐹 ∪ {〈𝑋, 𝑌〉}) ↾ {𝑋}) = ((𝐹 ↾ {𝑋}) ∪ ({〈𝑋, 𝑌〉} ↾ {𝑋})) |
18 | | uncom 3757 |
. . . . 5
⊢ (∅
∪ {〈𝑋, 𝑌〉}) = ({〈𝑋, 𝑌〉} ∪ ∅) |
19 | | un0 3967 |
. . . . 5
⊢
({〈𝑋, 𝑌〉} ∪ ∅) =
{〈𝑋, 𝑌〉} |
20 | 18, 19 | eqtr2i 2645 |
. . . 4
⊢
{〈𝑋, 𝑌〉} = (∅ ∪
{〈𝑋, 𝑌〉}) |
21 | 16, 17, 20 | 3eqtr4g 2681 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐹) → ((𝐹 ∪ {〈𝑋, 𝑌〉}) ↾ {𝑋}) = {〈𝑋, 𝑌〉}) |
22 | 21 | fveq1d 6193 |
. 2
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐹) → (((𝐹 ∪ {〈𝑋, 𝑌〉}) ↾ {𝑋})‘𝑋) = ({〈𝑋, 𝑌〉}‘𝑋)) |
23 | | snidg 4206 |
. . . 4
⊢ (𝑋 ∈ 𝑉 → 𝑋 ∈ {𝑋}) |
24 | 23 | 3ad2ant1 1082 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐹) → 𝑋 ∈ {𝑋}) |
25 | | fvres 6207 |
. . 3
⊢ (𝑋 ∈ {𝑋} → (((𝐹 ∪ {〈𝑋, 𝑌〉}) ↾ {𝑋})‘𝑋) = ((𝐹 ∪ {〈𝑋, 𝑌〉})‘𝑋)) |
26 | 24, 25 | syl 17 |
. 2
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐹) → (((𝐹 ∪ {〈𝑋, 𝑌〉}) ↾ {𝑋})‘𝑋) = ((𝐹 ∪ {〈𝑋, 𝑌〉})‘𝑋)) |
27 | | fvsng 6447 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → ({〈𝑋, 𝑌〉}‘𝑋) = 𝑌) |
28 | 27 | 3adant3 1081 |
. 2
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐹) → ({〈𝑋, 𝑌〉}‘𝑋) = 𝑌) |
29 | 22, 26, 28 | 3eqtr3d 2664 |
1
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐹) → ((𝐹 ∪ {〈𝑋, 𝑌〉})‘𝑋) = 𝑌) |