Proof of Theorem funsnfsupp
Step | Hyp | Ref
| Expression |
1 | | funsng 5851 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → Fun {〈𝑋, 𝑌〉}) |
2 | | simpl 472 |
. . . . . . . . 9
⊢ ((Fun
𝐹 ∧ 𝑋 ∉ dom 𝐹) → Fun 𝐹) |
3 | 1, 2 | anim12ci 589 |
. . . . . . . 8
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (Fun 𝐹 ∧ 𝑋 ∉ dom 𝐹)) → (Fun 𝐹 ∧ Fun {〈𝑋, 𝑌〉})) |
4 | | dmsnopg 5524 |
. . . . . . . . . . 11
⊢ (𝑌 ∈ 𝑊 → dom {〈𝑋, 𝑌〉} = {𝑋}) |
5 | 4 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → dom {〈𝑋, 𝑌〉} = {𝑋}) |
6 | 5 | ineq2d 3776 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → (dom 𝐹 ∩ dom {〈𝑋, 𝑌〉}) = (dom 𝐹 ∩ {𝑋})) |
7 | | df-nel 2783 |
. . . . . . . . . . 11
⊢ (𝑋 ∉ dom 𝐹 ↔ ¬ 𝑋 ∈ dom 𝐹) |
8 | | disjsn 4192 |
. . . . . . . . . . 11
⊢ ((dom
𝐹 ∩ {𝑋}) = ∅ ↔ ¬ 𝑋 ∈ dom 𝐹) |
9 | 7, 8 | sylbb2 227 |
. . . . . . . . . 10
⊢ (𝑋 ∉ dom 𝐹 → (dom 𝐹 ∩ {𝑋}) = ∅) |
10 | 9 | adantl 481 |
. . . . . . . . 9
⊢ ((Fun
𝐹 ∧ 𝑋 ∉ dom 𝐹) → (dom 𝐹 ∩ {𝑋}) = ∅) |
11 | 6, 10 | sylan9eq 2664 |
. . . . . . . 8
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (Fun 𝐹 ∧ 𝑋 ∉ dom 𝐹)) → (dom 𝐹 ∩ dom {〈𝑋, 𝑌〉}) = ∅) |
12 | 3, 11 | jca 553 |
. . . . . . 7
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (Fun 𝐹 ∧ 𝑋 ∉ dom 𝐹)) → ((Fun 𝐹 ∧ Fun {〈𝑋, 𝑌〉}) ∧ (dom 𝐹 ∩ dom {〈𝑋, 𝑌〉}) = ∅)) |
13 | 12 | adantl 481 |
. . . . . 6
⊢ ((𝑍 ∈ V ∧ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (Fun 𝐹 ∧ 𝑋 ∉ dom 𝐹))) → ((Fun 𝐹 ∧ Fun {〈𝑋, 𝑌〉}) ∧ (dom 𝐹 ∩ dom {〈𝑋, 𝑌〉}) = ∅)) |
14 | | funun 5846 |
. . . . . 6
⊢ (((Fun
𝐹 ∧ Fun {〈𝑋, 𝑌〉}) ∧ (dom 𝐹 ∩ dom {〈𝑋, 𝑌〉}) = ∅) → Fun (𝐹 ∪ {〈𝑋, 𝑌〉})) |
15 | 13, 14 | syl 17 |
. . . . 5
⊢ ((𝑍 ∈ V ∧ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (Fun 𝐹 ∧ 𝑋 ∉ dom 𝐹))) → Fun (𝐹 ∪ {〈𝑋, 𝑌〉})) |
16 | 15 | fsuppunbi 8179 |
. . . 4
⊢ ((𝑍 ∈ V ∧ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (Fun 𝐹 ∧ 𝑋 ∉ dom 𝐹))) → ((𝐹 ∪ {〈𝑋, 𝑌〉}) finSupp 𝑍 ↔ (𝐹 finSupp 𝑍 ∧ {〈𝑋, 𝑌〉} finSupp 𝑍))) |
17 | | simpl 472 |
. . . . . . . . 9
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (Fun 𝐹 ∧ 𝑋 ∉ dom 𝐹)) → (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) |
18 | 17 | anim2i 591 |
. . . . . . . 8
⊢ ((𝑍 ∈ V ∧ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (Fun 𝐹 ∧ 𝑋 ∉ dom 𝐹))) → (𝑍 ∈ V ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) |
19 | 18 | ancomd 466 |
. . . . . . 7
⊢ ((𝑍 ∈ V ∧ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (Fun 𝐹 ∧ 𝑋 ∉ dom 𝐹))) → ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ 𝑍 ∈ V)) |
20 | | df-3an 1033 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ V) ↔ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ 𝑍 ∈ V)) |
21 | 19, 20 | sylibr 223 |
. . . . . 6
⊢ ((𝑍 ∈ V ∧ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (Fun 𝐹 ∧ 𝑋 ∉ dom 𝐹))) → (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ V)) |
22 | | snopfsupp 8181 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ V) → {〈𝑋, 𝑌〉} finSupp 𝑍) |
23 | 21, 22 | syl 17 |
. . . . 5
⊢ ((𝑍 ∈ V ∧ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (Fun 𝐹 ∧ 𝑋 ∉ dom 𝐹))) → {〈𝑋, 𝑌〉} finSupp 𝑍) |
24 | 23 | biantrud 527 |
. . . 4
⊢ ((𝑍 ∈ V ∧ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (Fun 𝐹 ∧ 𝑋 ∉ dom 𝐹))) → (𝐹 finSupp 𝑍 ↔ (𝐹 finSupp 𝑍 ∧ {〈𝑋, 𝑌〉} finSupp 𝑍))) |
25 | 16, 24 | bitr4d 270 |
. . 3
⊢ ((𝑍 ∈ V ∧ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (Fun 𝐹 ∧ 𝑋 ∉ dom 𝐹))) → ((𝐹 ∪ {〈𝑋, 𝑌〉}) finSupp 𝑍 ↔ 𝐹 finSupp 𝑍)) |
26 | 25 | ex 449 |
. 2
⊢ (𝑍 ∈ V → (((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (Fun 𝐹 ∧ 𝑋 ∉ dom 𝐹)) → ((𝐹 ∪ {〈𝑋, 𝑌〉}) finSupp 𝑍 ↔ 𝐹 finSupp 𝑍))) |
27 | | relfsupp 8160 |
. . . . 5
⊢ Rel
finSupp |
28 | 27 | brrelex2i 5083 |
. . . 4
⊢ ((𝐹 ∪ {〈𝑋, 𝑌〉}) finSupp 𝑍 → 𝑍 ∈ V) |
29 | 27 | brrelex2i 5083 |
. . . 4
⊢ (𝐹 finSupp 𝑍 → 𝑍 ∈ V) |
30 | 28, 29 | pm5.21ni 366 |
. . 3
⊢ (¬
𝑍 ∈ V → ((𝐹 ∪ {〈𝑋, 𝑌〉}) finSupp 𝑍 ↔ 𝐹 finSupp 𝑍)) |
31 | 30 | a1d 25 |
. 2
⊢ (¬
𝑍 ∈ V → (((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (Fun 𝐹 ∧ 𝑋 ∉ dom 𝐹)) → ((𝐹 ∪ {〈𝑋, 𝑌〉}) finSupp 𝑍 ↔ 𝐹 finSupp 𝑍))) |
32 | 26, 31 | pm2.61i 175 |
1
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (Fun 𝐹 ∧ 𝑋 ∉ dom 𝐹)) → ((𝐹 ∪ {〈𝑋, 𝑌〉}) finSupp 𝑍 ↔ 𝐹 finSupp 𝑍)) |