Step | Hyp | Ref
| Expression |
1 | | fdifsupp.3 |
. . . . 5
⊢ (𝜑 → 𝐹 Fn 𝐴) |
2 | | difssd 4146 |
. . . . 5
⊢ (𝜑 → (𝐴 ∖ 𝐵) ⊆ 𝐴) |
3 | 1, 2 | fnssresd 6692 |
. . . 4
⊢ (𝜑 → (𝐹 ↾ (𝐴 ∖ 𝐵)) Fn (𝐴 ∖ 𝐵)) |
4 | | fdifsupp.1 |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
5 | 4 | difexd 5336 |
. . . 4
⊢ (𝜑 → (𝐴 ∖ 𝐵) ∈ V) |
6 | | fdifsupp.2 |
. . . 4
⊢ (𝜑 → 𝑍 ∈ 𝑊) |
7 | | elsuppfn 8193 |
. . . 4
⊢ (((𝐹 ↾ (𝐴 ∖ 𝐵)) Fn (𝐴 ∖ 𝐵) ∧ (𝐴 ∖ 𝐵) ∈ V ∧ 𝑍 ∈ 𝑊) → (𝑥 ∈ ((𝐹 ↾ (𝐴 ∖ 𝐵)) supp 𝑍) ↔ (𝑥 ∈ (𝐴 ∖ 𝐵) ∧ ((𝐹 ↾ (𝐴 ∖ 𝐵))‘𝑥) ≠ 𝑍))) |
8 | 3, 5, 6, 7 | syl3anc 1370 |
. . 3
⊢ (𝜑 → (𝑥 ∈ ((𝐹 ↾ (𝐴 ∖ 𝐵)) supp 𝑍) ↔ (𝑥 ∈ (𝐴 ∖ 𝐵) ∧ ((𝐹 ↾ (𝐴 ∖ 𝐵))‘𝑥) ≠ 𝑍))) |
9 | | eldif 3972 |
. . . . . 6
⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵)) |
10 | 9 | anbi1i 624 |
. . . . 5
⊢ ((𝑥 ∈ (𝐴 ∖ 𝐵) ∧ (𝐹‘𝑥) ≠ 𝑍) ↔ ((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ≠ 𝑍)) |
11 | 10 | a1i 11 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ (𝐴 ∖ 𝐵) ∧ (𝐹‘𝑥) ≠ 𝑍) ↔ ((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ≠ 𝑍))) |
12 | | simpr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ 𝐵)) → 𝑥 ∈ (𝐴 ∖ 𝐵)) |
13 | 12 | fvresd 6926 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ 𝐵)) → ((𝐹 ↾ (𝐴 ∖ 𝐵))‘𝑥) = (𝐹‘𝑥)) |
14 | 13 | neeq1d 2997 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ 𝐵)) → (((𝐹 ↾ (𝐴 ∖ 𝐵))‘𝑥) ≠ 𝑍 ↔ (𝐹‘𝑥) ≠ 𝑍)) |
15 | 14 | pm5.32da 579 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ (𝐴 ∖ 𝐵) ∧ ((𝐹 ↾ (𝐴 ∖ 𝐵))‘𝑥) ≠ 𝑍) ↔ (𝑥 ∈ (𝐴 ∖ 𝐵) ∧ (𝐹‘𝑥) ≠ 𝑍))) |
16 | | an32 646 |
. . . . 5
⊢ (((𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) ≠ 𝑍) ∧ ¬ 𝑥 ∈ 𝐵) ↔ ((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ≠ 𝑍)) |
17 | 16 | a1i 11 |
. . . 4
⊢ (𝜑 → (((𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) ≠ 𝑍) ∧ ¬ 𝑥 ∈ 𝐵) ↔ ((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ≠ 𝑍))) |
18 | 11, 15, 17 | 3bitr4d 311 |
. . 3
⊢ (𝜑 → ((𝑥 ∈ (𝐴 ∖ 𝐵) ∧ ((𝐹 ↾ (𝐴 ∖ 𝐵))‘𝑥) ≠ 𝑍) ↔ ((𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) ≠ 𝑍) ∧ ¬ 𝑥 ∈ 𝐵))) |
19 | | eldif 3972 |
. . . 4
⊢ (𝑥 ∈ ((𝐹 supp 𝑍) ∖ 𝐵) ↔ (𝑥 ∈ (𝐹 supp 𝑍) ∧ ¬ 𝑥 ∈ 𝐵)) |
20 | 4 | elexd 3501 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ V) |
21 | | elsuppfn 8193 |
. . . . . 6
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ V ∧ 𝑍 ∈ 𝑊) → (𝑥 ∈ (𝐹 supp 𝑍) ↔ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) ≠ 𝑍))) |
22 | 1, 20, 6, 21 | syl3anc 1370 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (𝐹 supp 𝑍) ↔ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) ≠ 𝑍))) |
23 | 22 | anbi1d 631 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ (𝐹 supp 𝑍) ∧ ¬ 𝑥 ∈ 𝐵) ↔ ((𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) ≠ 𝑍) ∧ ¬ 𝑥 ∈ 𝐵))) |
24 | 19, 23 | bitr2id 284 |
. . 3
⊢ (𝜑 → (((𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) ≠ 𝑍) ∧ ¬ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ ((𝐹 supp 𝑍) ∖ 𝐵))) |
25 | 8, 18, 24 | 3bitrd 305 |
. 2
⊢ (𝜑 → (𝑥 ∈ ((𝐹 ↾ (𝐴 ∖ 𝐵)) supp 𝑍) ↔ 𝑥 ∈ ((𝐹 supp 𝑍) ∖ 𝐵))) |
26 | 25 | eqrdv 2732 |
1
⊢ (𝜑 → ((𝐹 ↾ (𝐴 ∖ 𝐵)) supp 𝑍) = ((𝐹 supp 𝑍) ∖ 𝐵)) |