Theorem suppvalfn

Description: The value of the operation constructing the support of a function with a given domain. (Contributed by Stefan O'Rear, 1-Feb-2015) (Revised by AV, 22-Apr-2019)

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

Proof

Step	Hyp	Ref	Expression
1		fnfun	⊢ ( 𝐹 Fn 𝑋 → Fun 𝐹 )
2	1	3ad2ant1	⊢ ( ( 𝐹 Fn 𝑋 ∧ 𝑋 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → Fun 𝐹 )
3		fnex	⊢ ( ( 𝐹 Fn 𝑋 ∧ 𝑋 ∈ 𝑉 ) → 𝐹 ∈ V )
4	3	3adant3	⊢ ( ( 𝐹 Fn 𝑋 ∧ 𝑋 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → 𝐹 ∈ V )
5		simp3	⊢ ( ( 𝐹 Fn 𝑋 ∧ 𝑋 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → 𝑍 ∈ 𝑊 )
6		suppval1	⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ V ∧ 𝑍 ∈ 𝑊 ) → ( 𝐹 supp 𝑍 ) = { 𝑖 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑖 ) ≠ 𝑍 } )
7	2 4 5 6	syl3anc	⊢ ( ( 𝐹 Fn 𝑋 ∧ 𝑋 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝐹 supp 𝑍 ) = { 𝑖 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑖 ) ≠ 𝑍 } )
8		fndm	⊢ ( 𝐹 Fn 𝑋 → dom 𝐹 = 𝑋 )
9	8	3ad2ant1	⊢ ( ( 𝐹 Fn 𝑋 ∧ 𝑋 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → dom 𝐹 = 𝑋 )
10	9	rabeqdv	⊢ ( ( 𝐹 Fn 𝑋 ∧ 𝑋 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → { 𝑖 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑖 ) ≠ 𝑍 } = { 𝑖 ∈ 𝑋 ∣ ( 𝐹 ‘ 𝑖 ) ≠ 𝑍 } )
11	7 10	eqtrd	⊢ ( ( 𝐹 Fn 𝑋 ∧ 𝑋 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝐹 supp 𝑍 ) = { 𝑖 ∈ 𝑋 ∣ ( 𝐹 ‘ 𝑖 ) ≠ 𝑍 } )