Step | Hyp | Ref
| Expression |
1 | | simpl 484 |
. . . . . . . 8
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (Fun 𝐹 ∧ 𝑋 ∉ dom 𝐹)) → (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) |
2 | 1 | anim2i 618 |
. . . . . . 7
⊢ ((𝑍 ∈ V ∧ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (Fun 𝐹 ∧ 𝑋 ∉ dom 𝐹))) → (𝑍 ∈ V ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) |
3 | 2 | ancomd 463 |
. . . . . 6
⊢ ((𝑍 ∈ V ∧ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (Fun 𝐹 ∧ 𝑋 ∉ dom 𝐹))) → ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ 𝑍 ∈ V)) |
4 | | df-3an 1090 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ V) ↔ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ 𝑍 ∈ V)) |
5 | 3, 4 | sylibr 233 |
. . . . 5
⊢ ((𝑍 ∈ V ∧ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (Fun 𝐹 ∧ 𝑋 ∉ dom 𝐹))) → (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ V)) |
6 | | snopfsupp 9386 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ V) → {⟨𝑋, 𝑌⟩} finSupp 𝑍) |
7 | 5, 6 | syl 17 |
. . . 4
⊢ ((𝑍 ∈ V ∧ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (Fun 𝐹 ∧ 𝑋 ∉ dom 𝐹))) → {⟨𝑋, 𝑌⟩} finSupp 𝑍) |
8 | | funsng 6600 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → Fun {⟨𝑋, 𝑌⟩}) |
9 | | simpl 484 |
. . . . . . . . 9
⊢ ((Fun
𝐹 ∧ 𝑋 ∉ dom 𝐹) → Fun 𝐹) |
10 | 8, 9 | anim12ci 615 |
. . . . . . . 8
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (Fun 𝐹 ∧ 𝑋 ∉ dom 𝐹)) → (Fun 𝐹 ∧ Fun {⟨𝑋, 𝑌⟩})) |
11 | | dmsnopg 6213 |
. . . . . . . . . . 11
⊢ (𝑌 ∈ 𝑊 → dom {⟨𝑋, 𝑌⟩} = {𝑋}) |
12 | 11 | adantl 483 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → dom {⟨𝑋, 𝑌⟩} = {𝑋}) |
13 | 12 | ineq2d 4213 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → (dom 𝐹 ∩ dom {⟨𝑋, 𝑌⟩}) = (dom 𝐹 ∩ {𝑋})) |
14 | | df-nel 3048 |
. . . . . . . . . . 11
⊢ (𝑋 ∉ dom 𝐹 ↔ ¬ 𝑋 ∈ dom 𝐹) |
15 | | disjsn 4716 |
. . . . . . . . . . 11
⊢ ((dom
𝐹 ∩ {𝑋}) = ∅ ↔ ¬ 𝑋 ∈ dom 𝐹) |
16 | 14, 15 | sylbb2 237 |
. . . . . . . . . 10
⊢ (𝑋 ∉ dom 𝐹 → (dom 𝐹 ∩ {𝑋}) = ∅) |
17 | 16 | adantl 483 |
. . . . . . . . 9
⊢ ((Fun
𝐹 ∧ 𝑋 ∉ dom 𝐹) → (dom 𝐹 ∩ {𝑋}) = ∅) |
18 | 13, 17 | sylan9eq 2793 |
. . . . . . . 8
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (Fun 𝐹 ∧ 𝑋 ∉ dom 𝐹)) → (dom 𝐹 ∩ dom {⟨𝑋, 𝑌⟩}) = ∅) |
19 | 10, 18 | jca 513 |
. . . . . . 7
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (Fun 𝐹 ∧ 𝑋 ∉ dom 𝐹)) → ((Fun 𝐹 ∧ Fun {⟨𝑋, 𝑌⟩}) ∧ (dom 𝐹 ∩ dom {⟨𝑋, 𝑌⟩}) = ∅)) |
20 | 19 | adantl 483 |
. . . . . 6
⊢ ((𝑍 ∈ V ∧ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (Fun 𝐹 ∧ 𝑋 ∉ dom 𝐹))) → ((Fun 𝐹 ∧ Fun {⟨𝑋, 𝑌⟩}) ∧ (dom 𝐹 ∩ dom {⟨𝑋, 𝑌⟩}) = ∅)) |
21 | | funun 6595 |
. . . . . 6
⊢ (((Fun
𝐹 ∧ Fun {⟨𝑋, 𝑌⟩}) ∧ (dom 𝐹 ∩ dom {⟨𝑋, 𝑌⟩}) = ∅) → Fun (𝐹 ∪ {⟨𝑋, 𝑌⟩})) |
22 | 20, 21 | syl 17 |
. . . . 5
⊢ ((𝑍 ∈ V ∧ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (Fun 𝐹 ∧ 𝑋 ∉ dom 𝐹))) → Fun (𝐹 ∪ {⟨𝑋, 𝑌⟩})) |
23 | 22 | fsuppunbi 9384 |
. . . 4
⊢ ((𝑍 ∈ V ∧ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (Fun 𝐹 ∧ 𝑋 ∉ dom 𝐹))) → ((𝐹 ∪ {⟨𝑋, 𝑌⟩}) finSupp 𝑍 ↔ (𝐹 finSupp 𝑍 ∧ {⟨𝑋, 𝑌⟩} finSupp 𝑍))) |
24 | 7, 23 | mpbiran2d 707 |
. . 3
⊢ ((𝑍 ∈ V ∧ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (Fun 𝐹 ∧ 𝑋 ∉ dom 𝐹))) → ((𝐹 ∪ {⟨𝑋, 𝑌⟩}) finSupp 𝑍 ↔ 𝐹 finSupp 𝑍)) |
25 | 24 | ex 414 |
. 2
⊢ (𝑍 ∈ V → (((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (Fun 𝐹 ∧ 𝑋 ∉ dom 𝐹)) → ((𝐹 ∪ {⟨𝑋, 𝑌⟩}) finSupp 𝑍 ↔ 𝐹 finSupp 𝑍))) |
26 | | relfsupp 9363 |
. . . . 5
⊢ Rel
finSupp |
27 | 26 | brrelex2i 5734 |
. . . 4
⊢ ((𝐹 ∪ {⟨𝑋, 𝑌⟩}) finSupp 𝑍 → 𝑍 ∈ V) |
28 | 26 | brrelex2i 5734 |
. . . 4
⊢ (𝐹 finSupp 𝑍 → 𝑍 ∈ V) |
29 | 27, 28 | pm5.21ni 379 |
. . 3
⊢ (¬
𝑍 ∈ V → ((𝐹 ∪ {⟨𝑋, 𝑌⟩}) finSupp 𝑍 ↔ 𝐹 finSupp 𝑍)) |
30 | 29 | a1d 25 |
. 2
⊢ (¬
𝑍 ∈ V → (((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (Fun 𝐹 ∧ 𝑋 ∉ dom 𝐹)) → ((𝐹 ∪ {⟨𝑋, 𝑌⟩}) finSupp 𝑍 ↔ 𝐹 finSupp 𝑍))) |
31 | 25, 30 | pm2.61i 182 |
1
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (Fun 𝐹 ∧ 𝑋 ∉ dom 𝐹)) → ((𝐹 ∪ {⟨𝑋, 𝑌⟩}) finSupp 𝑍 ↔ 𝐹 finSupp 𝑍)) |