Theorem suppval1

Description: The value of the operation constructing the support of a function. (Contributed by AV, 6-Apr-2019)

	Ref	Expression
Assertion	suppval1	⊢ ( ( Fun 𝑋 ∧ 𝑋 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝑋 supp 𝑍 ) = { 𝑖 ∈ dom 𝑋 ∣ ( 𝑋 ‘ 𝑖 ) ≠ 𝑍 } )

Proof

Step	Hyp	Ref	Expression
1		suppval	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝑋 supp 𝑍 ) = { 𝑖 ∈ dom 𝑋 ∣ ( 𝑋 “ { 𝑖 } ) ≠ { 𝑍 } } )
2	1	3adant1	⊢ ( ( Fun 𝑋 ∧ 𝑋 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝑋 supp 𝑍 ) = { 𝑖 ∈ dom 𝑋 ∣ ( 𝑋 “ { 𝑖 } ) ≠ { 𝑍 } } )
3		funfn	⊢ ( Fun 𝑋 ↔ 𝑋 Fn dom 𝑋 )
4	3	biimpi	⊢ ( Fun 𝑋 → 𝑋 Fn dom 𝑋 )
5	4	3ad2ant1	⊢ ( ( Fun 𝑋 ∧ 𝑋 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → 𝑋 Fn dom 𝑋 )
6		fnsnfv	⊢ ( ( 𝑋 Fn dom 𝑋 ∧ 𝑖 ∈ dom 𝑋 ) → { ( 𝑋 ‘ 𝑖 ) } = ( 𝑋 “ { 𝑖 } ) )
7	5 6	sylan	⊢ ( ( ( Fun 𝑋 ∧ 𝑋 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑖 ∈ dom 𝑋 ) → { ( 𝑋 ‘ 𝑖 ) } = ( 𝑋 “ { 𝑖 } ) )
8	7	eqcomd	⊢ ( ( ( Fun 𝑋 ∧ 𝑋 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑖 ∈ dom 𝑋 ) → ( 𝑋 “ { 𝑖 } ) = { ( 𝑋 ‘ 𝑖 ) } )
9	8	neeq1d	⊢ ( ( ( Fun 𝑋 ∧ 𝑋 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑖 ∈ dom 𝑋 ) → ( ( 𝑋 “ { 𝑖 } ) ≠ { 𝑍 } ↔ { ( 𝑋 ‘ 𝑖 ) } ≠ { 𝑍 } ) )
10		fvex	⊢ ( 𝑋 ‘ 𝑖 ) ∈ V
11		sneqbg	⊢ ( ( 𝑋 ‘ 𝑖 ) ∈ V → ( { ( 𝑋 ‘ 𝑖 ) } = { 𝑍 } ↔ ( 𝑋 ‘ 𝑖 ) = 𝑍 ) )
12	10 11	mp1i	⊢ ( ( ( Fun 𝑋 ∧ 𝑋 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑖 ∈ dom 𝑋 ) → ( { ( 𝑋 ‘ 𝑖 ) } = { 𝑍 } ↔ ( 𝑋 ‘ 𝑖 ) = 𝑍 ) )
13	12	necon3bid	⊢ ( ( ( Fun 𝑋 ∧ 𝑋 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑖 ∈ dom 𝑋 ) → ( { ( 𝑋 ‘ 𝑖 ) } ≠ { 𝑍 } ↔ ( 𝑋 ‘ 𝑖 ) ≠ 𝑍 ) )
14	9 13	bitrd	⊢ ( ( ( Fun 𝑋 ∧ 𝑋 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑖 ∈ dom 𝑋 ) → ( ( 𝑋 “ { 𝑖 } ) ≠ { 𝑍 } ↔ ( 𝑋 ‘ 𝑖 ) ≠ 𝑍 ) )
15	14	rabbidva	⊢ ( ( Fun 𝑋 ∧ 𝑋 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → { 𝑖 ∈ dom 𝑋 ∣ ( 𝑋 “ { 𝑖 } ) ≠ { 𝑍 } } = { 𝑖 ∈ dom 𝑋 ∣ ( 𝑋 ‘ 𝑖 ) ≠ 𝑍 } )
16	2 15	eqtrd	⊢ ( ( Fun 𝑋 ∧ 𝑋 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝑋 supp 𝑍 ) = { 𝑖 ∈ dom 𝑋 ∣ ( 𝑋 ‘ 𝑖 ) ≠ 𝑍 } )