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