Theorem suppvalbr

Description: The value of the operation constructing the support of a function expressed by binary relations. (Contributed by AV, 7-Apr-2019)

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

Proof

Step	Hyp	Ref	Expression
1		df-rab	⊢ { 𝑥 ∈ dom 𝑅 ∣ ( 𝑅 “ { 𝑥 } ) ≠ { 𝑍 } } = { 𝑥 ∣ ( 𝑥 ∈ dom 𝑅 ∧ ( 𝑅 “ { 𝑥 } ) ≠ { 𝑍 } ) }
2		vex	⊢ 𝑥 ∈ V
3	2	eldm	⊢ ( 𝑥 ∈ dom 𝑅 ↔ ∃ 𝑦 𝑥 𝑅 𝑦 )
4		imasng	⊢ ( 𝑥 ∈ V → ( 𝑅 “ { 𝑥 } ) = { 𝑦 ∣ 𝑥 𝑅 𝑦 } )
5	4	elv	⊢ ( 𝑅 “ { 𝑥 } ) = { 𝑦 ∣ 𝑥 𝑅 𝑦 }
6	5	neeq1i	⊢ ( ( 𝑅 “ { 𝑥 } ) ≠ { 𝑍 } ↔ { 𝑦 ∣ 𝑥 𝑅 𝑦 } ≠ { 𝑍 } )
7		df-sn	⊢ { 𝑍 } = { 𝑦 ∣ 𝑦 = 𝑍 }
8	7	neeq2i	⊢ ( { 𝑦 ∣ 𝑥 𝑅 𝑦 } ≠ { 𝑍 } ↔ { 𝑦 ∣ 𝑥 𝑅 𝑦 } ≠ { 𝑦 ∣ 𝑦 = 𝑍 } )
9		nabbib	⊢ ( { 𝑦 ∣ 𝑥 𝑅 𝑦 } ≠ { 𝑦 ∣ 𝑦 = 𝑍 } ↔ ∃ 𝑦 ( 𝑥 𝑅 𝑦 ↔ ¬ 𝑦 = 𝑍 ) )
10	6 8 9	3bitri	⊢ ( ( 𝑅 “ { 𝑥 } ) ≠ { 𝑍 } ↔ ∃ 𝑦 ( 𝑥 𝑅 𝑦 ↔ ¬ 𝑦 = 𝑍 ) )
11	3 10	anbi12i	⊢ ( ( 𝑥 ∈ dom 𝑅 ∧ ( 𝑅 “ { 𝑥 } ) ≠ { 𝑍 } ) ↔ ( ∃ 𝑦 𝑥 𝑅 𝑦 ∧ ∃ 𝑦 ( 𝑥 𝑅 𝑦 ↔ ¬ 𝑦 = 𝑍 ) ) )
12	11	abbii	⊢ { 𝑥 ∣ ( 𝑥 ∈ dom 𝑅 ∧ ( 𝑅 “ { 𝑥 } ) ≠ { 𝑍 } ) } = { 𝑥 ∣ ( ∃ 𝑦 𝑥 𝑅 𝑦 ∧ ∃ 𝑦 ( 𝑥 𝑅 𝑦 ↔ ¬ 𝑦 = 𝑍 ) ) }
13	1 12	eqtr2i	⊢ { 𝑥 ∣ ( ∃ 𝑦 𝑥 𝑅 𝑦 ∧ ∃ 𝑦 ( 𝑥 𝑅 𝑦 ↔ ¬ 𝑦 = 𝑍 ) ) } = { 𝑥 ∈ dom 𝑅 ∣ ( 𝑅 “ { 𝑥 } ) ≠ { 𝑍 } }
14	13	a1i	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → { 𝑥 ∣ ( ∃ 𝑦 𝑥 𝑅 𝑦 ∧ ∃ 𝑦 ( 𝑥 𝑅 𝑦 ↔ ¬ 𝑦 = 𝑍 ) ) } = { 𝑥 ∈ dom 𝑅 ∣ ( 𝑅 “ { 𝑥 } ) ≠ { 𝑍 } } )
15		df-ne	⊢ ( 𝑦 ≠ 𝑍 ↔ ¬ 𝑦 = 𝑍 )
16	15	bibi2i	⊢ ( ( 𝑥 𝑅 𝑦 ↔ 𝑦 ≠ 𝑍 ) ↔ ( 𝑥 𝑅 𝑦 ↔ ¬ 𝑦 = 𝑍 ) )
17	16	exbii	⊢ ( ∃ 𝑦 ( 𝑥 𝑅 𝑦 ↔ 𝑦 ≠ 𝑍 ) ↔ ∃ 𝑦 ( 𝑥 𝑅 𝑦 ↔ ¬ 𝑦 = 𝑍 ) )
18	17	anbi2i	⊢ ( ( ∃ 𝑦 𝑥 𝑅 𝑦 ∧ ∃ 𝑦 ( 𝑥 𝑅 𝑦 ↔ 𝑦 ≠ 𝑍 ) ) ↔ ( ∃ 𝑦 𝑥 𝑅 𝑦 ∧ ∃ 𝑦 ( 𝑥 𝑅 𝑦 ↔ ¬ 𝑦 = 𝑍 ) ) )
19	18	abbii	⊢ { 𝑥 ∣ ( ∃ 𝑦 𝑥 𝑅 𝑦 ∧ ∃ 𝑦 ( 𝑥 𝑅 𝑦 ↔ 𝑦 ≠ 𝑍 ) ) } = { 𝑥 ∣ ( ∃ 𝑦 𝑥 𝑅 𝑦 ∧ ∃ 𝑦 ( 𝑥 𝑅 𝑦 ↔ ¬ 𝑦 = 𝑍 ) ) }
20	19	a1i	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → { 𝑥 ∣ ( ∃ 𝑦 𝑥 𝑅 𝑦 ∧ ∃ 𝑦 ( 𝑥 𝑅 𝑦 ↔ 𝑦 ≠ 𝑍 ) ) } = { 𝑥 ∣ ( ∃ 𝑦 𝑥 𝑅 𝑦 ∧ ∃ 𝑦 ( 𝑥 𝑅 𝑦 ↔ ¬ 𝑦 = 𝑍 ) ) } )
21		suppval	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝑅 supp 𝑍 ) = { 𝑥 ∈ dom 𝑅 ∣ ( 𝑅 “ { 𝑥 } ) ≠ { 𝑍 } } )
22	14 20 21	3eqtr4rd	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝑅 supp 𝑍 ) = { 𝑥 ∣ ( ∃ 𝑦 𝑥 𝑅 𝑦 ∧ ∃ 𝑦 ( 𝑥 𝑅 𝑦 ↔ 𝑦 ≠ 𝑍 ) ) } )