Theorem suppvalbr

Description: The value of the operation constructing the support of a function expressed by binary relations. (Contributed by AV, 7-Apr-2019) (Proof shortened by Sky Winter, 14-Oct-2026)

	Ref	Expression
Assertion	suppvalbr	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝑅 supp 𝑍 ) = { 𝑥 ∣ ( ∃ 𝑦 𝑥 𝑅 𝑦 ∧ ∃ 𝑦 ( 𝑥 𝑅 𝑦 ↔ 𝑦 ≠ 𝑍 ) ) } )

Proof

Step	Hyp	Ref	Expression
1		suppval	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝑅 supp 𝑍 ) = { 𝑥 ∈ dom 𝑅 ∣ ( 𝑅 “ { 𝑥 } ) ≠ { 𝑍 } } )
2		df-rab	⊢ { 𝑥 ∈ dom 𝑅 ∣ ( 𝑅 “ { 𝑥 } ) ≠ { 𝑍 } } = { 𝑥 ∣ ( 𝑥 ∈ dom 𝑅 ∧ ( 𝑅 “ { 𝑥 } ) ≠ { 𝑍 } ) }
3		vex	⊢ 𝑥 ∈ V
4	3	eldm	⊢ ( 𝑥 ∈ dom 𝑅 ↔ ∃ 𝑦 𝑥 𝑅 𝑦 )
5		nabbib	⊢ ( { 𝑦 ∣ 𝑥 𝑅 𝑦 } ≠ { 𝑦 ∣ 𝑦 = 𝑍 } ↔ ∃ 𝑦 ( 𝑥 𝑅 𝑦 ↔ ¬ 𝑦 = 𝑍 ) )
6		imasng	⊢ ( 𝑥 ∈ V → ( 𝑅 “ { 𝑥 } ) = { 𝑦 ∣ 𝑥 𝑅 𝑦 } )
7	6	elv	⊢ ( 𝑅 “ { 𝑥 } ) = { 𝑦 ∣ 𝑥 𝑅 𝑦 }
8		df-sn	⊢ { 𝑍 } = { 𝑦 ∣ 𝑦 = 𝑍 }
9	7 8	neeq12i	⊢ ( ( 𝑅 “ { 𝑥 } ) ≠ { 𝑍 } ↔ { 𝑦 ∣ 𝑥 𝑅 𝑦 } ≠ { 𝑦 ∣ 𝑦 = 𝑍 } )
10		df-ne	⊢ ( 𝑦 ≠ 𝑍 ↔ ¬ 𝑦 = 𝑍 )
11	10	bibi2i	⊢ ( ( 𝑥 𝑅 𝑦 ↔ 𝑦 ≠ 𝑍 ) ↔ ( 𝑥 𝑅 𝑦 ↔ ¬ 𝑦 = 𝑍 ) )
12	11	exbii	⊢ ( ∃ 𝑦 ( 𝑥 𝑅 𝑦 ↔ 𝑦 ≠ 𝑍 ) ↔ ∃ 𝑦 ( 𝑥 𝑅 𝑦 ↔ ¬ 𝑦 = 𝑍 ) )
13	5 9 12	3bitr4i	⊢ ( ( 𝑅 “ { 𝑥 } ) ≠ { 𝑍 } ↔ ∃ 𝑦 ( 𝑥 𝑅 𝑦 ↔ 𝑦 ≠ 𝑍 ) )
14	4 13	anbi12i	⊢ ( ( 𝑥 ∈ dom 𝑅 ∧ ( 𝑅 “ { 𝑥 } ) ≠ { 𝑍 } ) ↔ ( ∃ 𝑦 𝑥 𝑅 𝑦 ∧ ∃ 𝑦 ( 𝑥 𝑅 𝑦 ↔ 𝑦 ≠ 𝑍 ) ) )
15	14	abbii	⊢ { 𝑥 ∣ ( 𝑥 ∈ dom 𝑅 ∧ ( 𝑅 “ { 𝑥 } ) ≠ { 𝑍 } ) } = { 𝑥 ∣ ( ∃ 𝑦 𝑥 𝑅 𝑦 ∧ ∃ 𝑦 ( 𝑥 𝑅 𝑦 ↔ 𝑦 ≠ 𝑍 ) ) }
16	2 15	eqtri	⊢ { 𝑥 ∈ dom 𝑅 ∣ ( 𝑅 “ { 𝑥 } ) ≠ { 𝑍 } } = { 𝑥 ∣ ( ∃ 𝑦 𝑥 𝑅 𝑦 ∧ ∃ 𝑦 ( 𝑥 𝑅 𝑦 ↔ 𝑦 ≠ 𝑍 ) ) }
17	1 16	eqtrdi	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝑅 supp 𝑍 ) = { 𝑥 ∣ ( ∃ 𝑦 𝑥 𝑅 𝑦 ∧ ∃ 𝑦 ( 𝑥 𝑅 𝑦 ↔ 𝑦 ≠ 𝑍 ) ) } )