Metamath Proof Explorer


Theorem suppval

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

Ref Expression
Assertion suppval ( ( 𝑋𝑉𝑍𝑊 ) → ( 𝑋 supp 𝑍 ) = { 𝑖 ∈ dom 𝑋 ∣ ( 𝑋 “ { 𝑖 } ) ≠ { 𝑍 } } )

Proof

Step Hyp Ref Expression
1 df-supp supp = ( 𝑥 ∈ V , 𝑧 ∈ V ↦ { 𝑖 ∈ dom 𝑥 ∣ ( 𝑥 “ { 𝑖 } ) ≠ { 𝑧 } } )
2 1 a1i ( ( 𝑋𝑉𝑍𝑊 ) → supp = ( 𝑥 ∈ V , 𝑧 ∈ V ↦ { 𝑖 ∈ dom 𝑥 ∣ ( 𝑥 “ { 𝑖 } ) ≠ { 𝑧 } } ) )
3 dmeq ( 𝑥 = 𝑋 → dom 𝑥 = dom 𝑋 )
4 3 adantr ( ( 𝑥 = 𝑋𝑧 = 𝑍 ) → dom 𝑥 = dom 𝑋 )
5 imaeq1 ( 𝑥 = 𝑋 → ( 𝑥 “ { 𝑖 } ) = ( 𝑋 “ { 𝑖 } ) )
6 5 adantr ( ( 𝑥 = 𝑋𝑧 = 𝑍 ) → ( 𝑥 “ { 𝑖 } ) = ( 𝑋 “ { 𝑖 } ) )
7 sneq ( 𝑧 = 𝑍 → { 𝑧 } = { 𝑍 } )
8 7 adantl ( ( 𝑥 = 𝑋𝑧 = 𝑍 ) → { 𝑧 } = { 𝑍 } )
9 6 8 neeq12d ( ( 𝑥 = 𝑋𝑧 = 𝑍 ) → ( ( 𝑥 “ { 𝑖 } ) ≠ { 𝑧 } ↔ ( 𝑋 “ { 𝑖 } ) ≠ { 𝑍 } ) )
10 4 9 rabeqbidv ( ( 𝑥 = 𝑋𝑧 = 𝑍 ) → { 𝑖 ∈ dom 𝑥 ∣ ( 𝑥 “ { 𝑖 } ) ≠ { 𝑧 } } = { 𝑖 ∈ dom 𝑋 ∣ ( 𝑋 “ { 𝑖 } ) ≠ { 𝑍 } } )
11 10 adantl ( ( ( 𝑋𝑉𝑍𝑊 ) ∧ ( 𝑥 = 𝑋𝑧 = 𝑍 ) ) → { 𝑖 ∈ dom 𝑥 ∣ ( 𝑥 “ { 𝑖 } ) ≠ { 𝑧 } } = { 𝑖 ∈ dom 𝑋 ∣ ( 𝑋 “ { 𝑖 } ) ≠ { 𝑍 } } )
12 elex ( 𝑋𝑉𝑋 ∈ V )
13 12 adantr ( ( 𝑋𝑉𝑍𝑊 ) → 𝑋 ∈ V )
14 elex ( 𝑍𝑊𝑍 ∈ V )
15 14 adantl ( ( 𝑋𝑉𝑍𝑊 ) → 𝑍 ∈ V )
16 dmexg ( 𝑋𝑉 → dom 𝑋 ∈ V )
17 16 adantr ( ( 𝑋𝑉𝑍𝑊 ) → dom 𝑋 ∈ V )
18 rabexg ( dom 𝑋 ∈ V → { 𝑖 ∈ dom 𝑋 ∣ ( 𝑋 “ { 𝑖 } ) ≠ { 𝑍 } } ∈ V )
19 17 18 syl ( ( 𝑋𝑉𝑍𝑊 ) → { 𝑖 ∈ dom 𝑋 ∣ ( 𝑋 “ { 𝑖 } ) ≠ { 𝑍 } } ∈ V )
20 2 11 13 15 19 ovmpod ( ( 𝑋𝑉𝑍𝑊 ) → ( 𝑋 supp 𝑍 ) = { 𝑖 ∈ dom 𝑋 ∣ ( 𝑋 “ { 𝑖 } ) ≠ { 𝑍 } } )