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