This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝑍 ) ∖ 𝐵 ) )