Theorem suppssrg

Description: A function is zero outside its support. Version of suppssr avoiding ax-rep by assuming F is a set rather than its domain A . (Contributed by SN, 5-May-2024)

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

Proof

Step	Hyp	Ref	Expression
1		suppssrg.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
2		suppssrg.n	⊢ ( 𝜑 → ( 𝐹 supp 𝑍 ) ⊆ 𝑊 )
3		suppssrg.a	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
4		suppssrg.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑈 )
5		eldif	⊢ ( 𝑋 ∈ ( 𝐴 ∖ 𝑊 ) ↔ ( 𝑋 ∈ 𝐴 ∧ ¬ 𝑋 ∈ 𝑊 ) )
6	1	ffnd	⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
7		elsuppfng	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑈 ) → ( 𝑋 ∈ ( 𝐹 supp 𝑍 ) ↔ ( 𝑋 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑋 ) ≠ 𝑍 ) ) )
8	6 3 4 7	syl3anc	⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐹 supp 𝑍 ) ↔ ( 𝑋 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑋 ) ≠ 𝑍 ) ) )
9	2	sseld	⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐹 supp 𝑍 ) → 𝑋 ∈ 𝑊 ) )
10	8 9	sylbird	⊢ ( 𝜑 → ( ( 𝑋 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑋 ) ≠ 𝑍 ) → 𝑋 ∈ 𝑊 ) )
11	10	expdimp	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑋 ) ≠ 𝑍 → 𝑋 ∈ 𝑊 ) )
12	11	necon1bd	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) → ( ¬ 𝑋 ∈ 𝑊 → ( 𝐹 ‘ 𝑋 ) = 𝑍 ) )
13	12	impr	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐴 ∧ ¬ 𝑋 ∈ 𝑊 ) ) → ( 𝐹 ‘ 𝑋 ) = 𝑍 )
14	5 13	sylan2b	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝑊 ) ) → ( 𝐹 ‘ 𝑋 ) = 𝑍 )