Metamath Proof Explorer


Theorem fdifsupp

Description: Express the support of a function F outside of B in two different ways. (Contributed by Thierry Arnoux, 5-Oct-2025)

Ref Expression
Hypotheses fdifsupp.1 ( 𝜑𝐴𝑉 )
fdifsupp.2 ( 𝜑𝑍𝑊 )
fdifsupp.3 ( 𝜑𝐹 Fn 𝐴 )
Assertion fdifsupp ( 𝜑 → ( ( 𝐹 ↾ ( 𝐴𝐵 ) ) supp 𝑍 ) = ( ( 𝐹 supp 𝑍 ) ∖ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 fdifsupp.1 ( 𝜑𝐴𝑉 )
2 fdifsupp.2 ( 𝜑𝑍𝑊 )
3 fdifsupp.3 ( 𝜑𝐹 Fn 𝐴 )
4 difssd ( 𝜑 → ( 𝐴𝐵 ) ⊆ 𝐴 )
5 3 4 fnssresd ( 𝜑 → ( 𝐹 ↾ ( 𝐴𝐵 ) ) Fn ( 𝐴𝐵 ) )
6 1 difexd ( 𝜑 → ( 𝐴𝐵 ) ∈ V )
7 elsuppfn ( ( ( 𝐹 ↾ ( 𝐴𝐵 ) ) Fn ( 𝐴𝐵 ) ∧ ( 𝐴𝐵 ) ∈ V ∧ 𝑍𝑊 ) → ( 𝑥 ∈ ( ( 𝐹 ↾ ( 𝐴𝐵 ) ) supp 𝑍 ) ↔ ( 𝑥 ∈ ( 𝐴𝐵 ) ∧ ( ( 𝐹 ↾ ( 𝐴𝐵 ) ) ‘ 𝑥 ) ≠ 𝑍 ) ) )
8 5 6 2 7 syl3anc ( 𝜑 → ( 𝑥 ∈ ( ( 𝐹 ↾ ( 𝐴𝐵 ) ) supp 𝑍 ) ↔ ( 𝑥 ∈ ( 𝐴𝐵 ) ∧ ( ( 𝐹 ↾ ( 𝐴𝐵 ) ) ‘ 𝑥 ) ≠ 𝑍 ) ) )
9 eldif ( 𝑥 ∈ ( 𝐴𝐵 ) ↔ ( 𝑥𝐴 ∧ ¬ 𝑥𝐵 ) )
10 9 anbi1i ( ( 𝑥 ∈ ( 𝐴𝐵 ) ∧ ( 𝐹𝑥 ) ≠ 𝑍 ) ↔ ( ( 𝑥𝐴 ∧ ¬ 𝑥𝐵 ) ∧ ( 𝐹𝑥 ) ≠ 𝑍 ) )
11 10 a1i ( 𝜑 → ( ( 𝑥 ∈ ( 𝐴𝐵 ) ∧ ( 𝐹𝑥 ) ≠ 𝑍 ) ↔ ( ( 𝑥𝐴 ∧ ¬ 𝑥𝐵 ) ∧ ( 𝐹𝑥 ) ≠ 𝑍 ) ) )
12 simpr ( ( 𝜑𝑥 ∈ ( 𝐴𝐵 ) ) → 𝑥 ∈ ( 𝐴𝐵 ) )
13 12 fvresd ( ( 𝜑𝑥 ∈ ( 𝐴𝐵 ) ) → ( ( 𝐹 ↾ ( 𝐴𝐵 ) ) ‘ 𝑥 ) = ( 𝐹𝑥 ) )
14 13 neeq1d ( ( 𝜑𝑥 ∈ ( 𝐴𝐵 ) ) → ( ( ( 𝐹 ↾ ( 𝐴𝐵 ) ) ‘ 𝑥 ) ≠ 𝑍 ↔ ( 𝐹𝑥 ) ≠ 𝑍 ) )
15 14 pm5.32da ( 𝜑 → ( ( 𝑥 ∈ ( 𝐴𝐵 ) ∧ ( ( 𝐹 ↾ ( 𝐴𝐵 ) ) ‘ 𝑥 ) ≠ 𝑍 ) ↔ ( 𝑥 ∈ ( 𝐴𝐵 ) ∧ ( 𝐹𝑥 ) ≠ 𝑍 ) ) )
16 an32 ( ( ( 𝑥𝐴 ∧ ( 𝐹𝑥 ) ≠ 𝑍 ) ∧ ¬ 𝑥𝐵 ) ↔ ( ( 𝑥𝐴 ∧ ¬ 𝑥𝐵 ) ∧ ( 𝐹𝑥 ) ≠ 𝑍 ) )
17 16 a1i ( 𝜑 → ( ( ( 𝑥𝐴 ∧ ( 𝐹𝑥 ) ≠ 𝑍 ) ∧ ¬ 𝑥𝐵 ) ↔ ( ( 𝑥𝐴 ∧ ¬ 𝑥𝐵 ) ∧ ( 𝐹𝑥 ) ≠ 𝑍 ) ) )
18 11 15 17 3bitr4d ( 𝜑 → ( ( 𝑥 ∈ ( 𝐴𝐵 ) ∧ ( ( 𝐹 ↾ ( 𝐴𝐵 ) ) ‘ 𝑥 ) ≠ 𝑍 ) ↔ ( ( 𝑥𝐴 ∧ ( 𝐹𝑥 ) ≠ 𝑍 ) ∧ ¬ 𝑥𝐵 ) ) )
19 eldif ( 𝑥 ∈ ( ( 𝐹 supp 𝑍 ) ∖ 𝐵 ) ↔ ( 𝑥 ∈ ( 𝐹 supp 𝑍 ) ∧ ¬ 𝑥𝐵 ) )
20 1 elexd ( 𝜑𝐴 ∈ V )
21 elsuppfn ( ( 𝐹 Fn 𝐴𝐴 ∈ V ∧ 𝑍𝑊 ) → ( 𝑥 ∈ ( 𝐹 supp 𝑍 ) ↔ ( 𝑥𝐴 ∧ ( 𝐹𝑥 ) ≠ 𝑍 ) ) )
22 3 20 2 21 syl3anc ( 𝜑 → ( 𝑥 ∈ ( 𝐹 supp 𝑍 ) ↔ ( 𝑥𝐴 ∧ ( 𝐹𝑥 ) ≠ 𝑍 ) ) )
23 22 anbi1d ( 𝜑 → ( ( 𝑥 ∈ ( 𝐹 supp 𝑍 ) ∧ ¬ 𝑥𝐵 ) ↔ ( ( 𝑥𝐴 ∧ ( 𝐹𝑥 ) ≠ 𝑍 ) ∧ ¬ 𝑥𝐵 ) ) )
24 19 23 bitr2id ( 𝜑 → ( ( ( 𝑥𝐴 ∧ ( 𝐹𝑥 ) ≠ 𝑍 ) ∧ ¬ 𝑥𝐵 ) ↔ 𝑥 ∈ ( ( 𝐹 supp 𝑍 ) ∖ 𝐵 ) ) )
25 8 18 24 3bitrd ( 𝜑 → ( 𝑥 ∈ ( ( 𝐹 ↾ ( 𝐴𝐵 ) ) supp 𝑍 ) ↔ 𝑥 ∈ ( ( 𝐹 supp 𝑍 ) ∖ 𝐵 ) ) )
26 25 eqrdv ( 𝜑 → ( ( 𝐹 ↾ ( 𝐴𝐵 ) ) supp 𝑍 ) = ( ( 𝐹 supp 𝑍 ) ∖ 𝐵 ) )