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

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