Metamath Proof Explorer


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 𝑋 ∣ ( 𝑋𝑖 ) ≠ 𝑍 } )