This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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