Theorem suppvalfng

Description: The value of the operation constructing the support of a function with a given domain. This version of suppvalfn assumes F is a set rather than its domain X , avoiding ax-rep . (Contributed by SN, 5-Aug-2024)

	Ref	Expression
Assertion	suppvalfng	⊢ ( ( 𝐹 Fn 𝑋 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝐹 supp 𝑍 ) = { 𝑖 ∈ 𝑋 ∣ ( 𝐹 ‘ 𝑖 ) ≠ 𝑍 } )

Proof

Step	Hyp	Ref	Expression
1		fnfun	⊢ ( 𝐹 Fn 𝑋 → Fun 𝐹 )
2		suppval1	⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝐹 supp 𝑍 ) = { 𝑖 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑖 ) ≠ 𝑍 } )
3	1 2	syl3an1	⊢ ( ( 𝐹 Fn 𝑋 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝐹 supp 𝑍 ) = { 𝑖 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑖 ) ≠ 𝑍 } )
4		fndm	⊢ ( 𝐹 Fn 𝑋 → dom 𝐹 = 𝑋 )
5	4	3ad2ant1	⊢ ( ( 𝐹 Fn 𝑋 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → dom 𝐹 = 𝑋 )
6	5	rabeqdv	⊢ ( ( 𝐹 Fn 𝑋 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → { 𝑖 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑖 ) ≠ 𝑍 } = { 𝑖 ∈ 𝑋 ∣ ( 𝐹 ‘ 𝑖 ) ≠ 𝑍 } )
7	3 6	eqtrd	⊢ ( ( 𝐹 Fn 𝑋 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝐹 supp 𝑍 ) = { 𝑖 ∈ 𝑋 ∣ ( 𝐹 ‘ 𝑖 ) ≠ 𝑍 } )