Theorem suppssr

Description: A function is zero outside its support. (Contributed by Mario Carneiro, 19-Dec-2014) (Revised by AV, 28-May-2019)

	Ref	Expression
Hypotheses	suppssr.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
	suppssr.n	⊢ ( 𝜑 → ( 𝐹 supp 𝑍 ) ⊆ 𝑊 )
	suppssr.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	suppssr.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑈 )
Assertion	suppssr	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝑊 ) ) → ( 𝐹 ‘ 𝑋 ) = 𝑍 )

Proof

Step	Hyp	Ref	Expression
1		suppssr.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
2		suppssr.n	⊢ ( 𝜑 → ( 𝐹 supp 𝑍 ) ⊆ 𝑊 )
3		suppssr.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
4		suppssr.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑈 )
5		eldif	⊢ ( 𝑋 ∈ ( 𝐴 ∖ 𝑊 ) ↔ ( 𝑋 ∈ 𝐴 ∧ ¬ 𝑋 ∈ 𝑊 ) )
6		fvex	⊢ ( 𝐹 ‘ 𝑋 ) ∈ V
7		eldifsn	⊢ ( ( 𝐹 ‘ 𝑋 ) ∈ ( V ∖ { 𝑍 } ) ↔ ( ( 𝐹 ‘ 𝑋 ) ∈ V ∧ ( 𝐹 ‘ 𝑋 ) ≠ 𝑍 ) )
8	6 7	mpbiran	⊢ ( ( 𝐹 ‘ 𝑋 ) ∈ ( V ∖ { 𝑍 } ) ↔ ( 𝐹 ‘ 𝑋 ) ≠ 𝑍 )
9	1	ffnd	⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
10		elsuppfn	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑉 ∧ 𝑍 ∈ 𝑈 ) → ( 𝑋 ∈ ( 𝐹 supp 𝑍 ) ↔ ( 𝑋 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑋 ) ≠ 𝑍 ) ) )
11	9 3 4 10	syl3anc	⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐹 supp 𝑍 ) ↔ ( 𝑋 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑋 ) ≠ 𝑍 ) ) )
12		ibar	⊢ ( ( 𝐹 ‘ 𝑋 ) ∈ V → ( ( 𝐹 ‘ 𝑋 ) ≠ 𝑍 ↔ ( ( 𝐹 ‘ 𝑋 ) ∈ V ∧ ( 𝐹 ‘ 𝑋 ) ≠ 𝑍 ) ) )
13	6 12	mp1i	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑋 ) ≠ 𝑍 ↔ ( ( 𝐹 ‘ 𝑋 ) ∈ V ∧ ( 𝐹 ‘ 𝑋 ) ≠ 𝑍 ) ) )
14	13 7	bitr4di	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑋 ) ≠ 𝑍 ↔ ( 𝐹 ‘ 𝑋 ) ∈ ( V ∖ { 𝑍 } ) ) )
15	14	pm5.32da	⊢ ( 𝜑 → ( ( 𝑋 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑋 ) ≠ 𝑍 ) ↔ ( 𝑋 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑋 ) ∈ ( V ∖ { 𝑍 } ) ) ) )
16	11 15	bitrd	⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐹 supp 𝑍 ) ↔ ( 𝑋 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑋 ) ∈ ( V ∖ { 𝑍 } ) ) ) )
17	2	sseld	⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐹 supp 𝑍 ) → 𝑋 ∈ 𝑊 ) )
18	16 17	sylbird	⊢ ( 𝜑 → ( ( 𝑋 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑋 ) ∈ ( V ∖ { 𝑍 } ) ) → 𝑋 ∈ 𝑊 ) )
19	18	expdimp	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑋 ) ∈ ( V ∖ { 𝑍 } ) → 𝑋 ∈ 𝑊 ) )
20	8 19	syl5bir	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑋 ) ≠ 𝑍 → 𝑋 ∈ 𝑊 ) )
21	20	necon1bd	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) → ( ¬ 𝑋 ∈ 𝑊 → ( 𝐹 ‘ 𝑋 ) = 𝑍 ) )
22	21	impr	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐴 ∧ ¬ 𝑋 ∈ 𝑊 ) ) → ( 𝐹 ‘ 𝑋 ) = 𝑍 )
23	5 22	sylan2b	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝑊 ) ) → ( 𝐹 ‘ 𝑋 ) = 𝑍 )