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

Metamath Proof Explorer

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 𝑍 ) = { 𝑥 ∣ ( ∃ 𝑦 𝑥 𝑅 𝑦 ∧ ∃ 𝑦 ( 𝑥 𝑅 𝑦 ↔ 𝑦 ≠ 𝑍 ) ) } )