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

Metamath Proof Explorer

Theorem cnvimadfsn

Description: The support of functions "defined" by inverse images expressed by binary relations. (Contributed by AV, 7-Apr-2019)

Ref Expression
Assertion cnvimadfsn ( ◡ 𝑅 “ ( V ∖ { 𝑍 } ) ) = { 𝑥 ∣ ∃ 𝑦 ( 𝑥 𝑅 𝑦 ∧ 𝑦 ≠ 𝑍 ) }

Proof

Step Hyp Ref Expression
1 dfima3 ⊢ ( ◡ 𝑅 “ ( V ∖ { 𝑍 } ) ) = { 𝑥 ∣ ∃ 𝑦 ( 𝑦 ∈ ( V ∖ { 𝑍 } ) ∧ ⟨ 𝑦 , 𝑥 ⟩ ∈ ◡ 𝑅 ) }
2 eldifvsn ⊢ ( 𝑦 ∈ V → ( 𝑦 ∈ ( V ∖ { 𝑍 } ) ↔ 𝑦 ≠ 𝑍 ) )
3 2 elv ⊢ ( 𝑦 ∈ ( V ∖ { 𝑍 } ) ↔ 𝑦 ≠ 𝑍 )
4 vex ⊢ 𝑦 ∈ V
5 vex ⊢ 𝑥 ∈ V
6 4 5 opelcnv ⊢ ( ⟨ 𝑦 , 𝑥 ⟩ ∈ ◡ 𝑅 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 )
7 df-br ⊢ ( 𝑥 𝑅 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 )
8 6 7 bitr4i ⊢ ( ⟨ 𝑦 , 𝑥 ⟩ ∈ ◡ 𝑅 ↔ 𝑥 𝑅 𝑦 )
9 3 8 anbi12ci ⊢ ( ( 𝑦 ∈ ( V ∖ { 𝑍 } ) ∧ ⟨ 𝑦 , 𝑥 ⟩ ∈ ◡ 𝑅 ) ↔ ( 𝑥 𝑅 𝑦 ∧ 𝑦 ≠ 𝑍 ) )
10 9 exbii ⊢ ( ∃ 𝑦 ( 𝑦 ∈ ( V ∖ { 𝑍 } ) ∧ ⟨ 𝑦 , 𝑥 ⟩ ∈ ◡ 𝑅 ) ↔ ∃ 𝑦 ( 𝑥 𝑅 𝑦 ∧ 𝑦 ≠ 𝑍 ) )
11 10 abbii ⊢ { 𝑥 ∣ ∃ 𝑦 ( 𝑦 ∈ ( V ∖ { 𝑍 } ) ∧ ⟨ 𝑦 , 𝑥 ⟩ ∈ ◡ 𝑅 ) } = { 𝑥 ∣ ∃ 𝑦 ( 𝑥 𝑅 𝑦 ∧ 𝑦 ≠ 𝑍 ) }
12 1 11 eqtri ⊢ ( ◡ 𝑅 “ ( V ∖ { 𝑍 } ) ) = { 𝑥 ∣ ∃ 𝑦 ( 𝑥 𝑅 𝑦 ∧ 𝑦 ≠ 𝑍 ) }