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		suppval	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝑅 supp 𝑍 ) = { 𝑥 ∈ dom 𝑅 ∣ ( 𝑅 “ { 𝑥 } ) ≠ { 𝑍 } } )
2		df-rab	⊢ { 𝑥 ∈ dom 𝑅 ∣ ( 𝑅 “ { 𝑥 } ) ≠ { 𝑍 } } = { 𝑥 ∣ ( 𝑥 ∈ dom 𝑅 ∧ ( 𝑅 “ { 𝑥 } ) ≠ { 𝑍 } ) }
3		vex	⊢ 𝑥 ∈ V
4	3	eldm	⊢ ( 𝑥 ∈ dom 𝑅 ↔ ∃ 𝑦 𝑥 𝑅 𝑦 )
5		df-sn	⊢ { 𝑍 } = { 𝑦 ∣ 𝑦 = 𝑍 }
6	5	neeq2i	⊢ ( { 𝑦 ∣ 𝑥 𝑅 𝑦 } ≠ { 𝑍 } ↔ { 𝑦 ∣ 𝑥 𝑅 𝑦 } ≠ { 𝑦 ∣ 𝑦 = 𝑍 } )
7		imasng	⊢ ( 𝑥 ∈ V → ( 𝑅 “ { 𝑥 } ) = { 𝑦 ∣ 𝑥 𝑅 𝑦 } )
8	7	elv	⊢ ( 𝑅 “ { 𝑥 } ) = { 𝑦 ∣ 𝑥 𝑅 𝑦 }
9	8	neeq1i	⊢ ( ( 𝑅 “ { 𝑥 } ) ≠ { 𝑍 } ↔ { 𝑦 ∣ 𝑥 𝑅 𝑦 } ≠ { 𝑍 } )
10		nabbi	⊢ ( ∃ 𝑦 ( 𝑥 𝑅 𝑦 ↔ ¬ 𝑦 = 𝑍 ) ↔ { 𝑦 ∣ 𝑥 𝑅 𝑦 } ≠ { 𝑦 ∣ 𝑦 = 𝑍 } )
11	6 9 10	3bitr4i	⊢ ( ( 𝑅 “ { 𝑥 } ) ≠ { 𝑍 } ↔ ∃ 𝑦 ( 𝑥 𝑅 𝑦 ↔ ¬ 𝑦 = 𝑍 ) )
12	4 11	anbi12i	⊢ ( ( 𝑥 ∈ dom 𝑅 ∧ ( 𝑅 “ { 𝑥 } ) ≠ { 𝑍 } ) ↔ ( ∃ 𝑦 𝑥 𝑅 𝑦 ∧ ∃ 𝑦 ( 𝑥 𝑅 𝑦 ↔ ¬ 𝑦 = 𝑍 ) ) )
13	12	abbii	⊢ { 𝑥 ∣ ( 𝑥 ∈ dom 𝑅 ∧ ( 𝑅 “ { 𝑥 } ) ≠ { 𝑍 } ) } = { 𝑥 ∣ ( ∃ 𝑦 𝑥 𝑅 𝑦 ∧ ∃ 𝑦 ( 𝑥 𝑅 𝑦 ↔ ¬ 𝑦 = 𝑍 ) ) }
14	2 13	eqtri	⊢ { 𝑥 ∈ dom 𝑅 ∣ ( 𝑅 “ { 𝑥 } ) ≠ { 𝑍 } } = { 𝑥 ∣ ( ∃ 𝑦 𝑥 𝑅 𝑦 ∧ ∃ 𝑦 ( 𝑥 𝑅 𝑦 ↔ ¬ 𝑦 = 𝑍 ) ) }
15	14	a1i	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → { 𝑥 ∈ dom 𝑅 ∣ ( 𝑅 “ { 𝑥 } ) ≠ { 𝑍 } } = { 𝑥 ∣ ( ∃ 𝑦 𝑥 𝑅 𝑦 ∧ ∃ 𝑦 ( 𝑥 𝑅 𝑦 ↔ ¬ 𝑦 = 𝑍 ) ) } )
16		df-ne	⊢ ( 𝑦 ≠ 𝑍 ↔ ¬ 𝑦 = 𝑍 )
17	16	bicomi	⊢ ( ¬ 𝑦 = 𝑍 ↔ 𝑦 ≠ 𝑍 )
18	17	bibi2i	⊢ ( ( 𝑥 𝑅 𝑦 ↔ ¬ 𝑦 = 𝑍 ) ↔ ( 𝑥 𝑅 𝑦 ↔ 𝑦 ≠ 𝑍 ) )
19	18	exbii	⊢ ( ∃ 𝑦 ( 𝑥 𝑅 𝑦 ↔ ¬ 𝑦 = 𝑍 ) ↔ ∃ 𝑦 ( 𝑥 𝑅 𝑦 ↔ 𝑦 ≠ 𝑍 ) )
20	19	anbi2i	⊢ ( ( ∃ 𝑦 𝑥 𝑅 𝑦 ∧ ∃ 𝑦 ( 𝑥 𝑅 𝑦 ↔ ¬ 𝑦 = 𝑍 ) ) ↔ ( ∃ 𝑦 𝑥 𝑅 𝑦 ∧ ∃ 𝑦 ( 𝑥 𝑅 𝑦 ↔ 𝑦 ≠ 𝑍 ) ) )
21	20	abbii	⊢ { 𝑥 ∣ ( ∃ 𝑦 𝑥 𝑅 𝑦 ∧ ∃ 𝑦 ( 𝑥 𝑅 𝑦 ↔ ¬ 𝑦 = 𝑍 ) ) } = { 𝑥 ∣ ( ∃ 𝑦 𝑥 𝑅 𝑦 ∧ ∃ 𝑦 ( 𝑥 𝑅 𝑦 ↔ 𝑦 ≠ 𝑍 ) ) }
22	21	a1i	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → { 𝑥 ∣ ( ∃ 𝑦 𝑥 𝑅 𝑦 ∧ ∃ 𝑦 ( 𝑥 𝑅 𝑦 ↔ ¬ 𝑦 = 𝑍 ) ) } = { 𝑥 ∣ ( ∃ 𝑦 𝑥 𝑅 𝑦 ∧ ∃ 𝑦 ( 𝑥 𝑅 𝑦 ↔ 𝑦 ≠ 𝑍 ) ) } )
23	1 15 22	3eqtrd	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝑅 supp 𝑍 ) = { 𝑥 ∣ ( ∃ 𝑦 𝑥 𝑅 𝑦 ∧ ∃ 𝑦 ( 𝑥 𝑅 𝑦 ↔ 𝑦 ≠ 𝑍 ) ) } )