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

Metamath Proof Explorer

Theorem suppimacnvss

Description: The support of functions "defined" by inverse images is a subset of the support defined by df-supp . (Contributed by AV, 7-Apr-2019)

Ref Expression
Assertion suppimacnvss ( ( 𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( ◡ 𝑅 “ ( V ∖ { 𝑍 } ) ) ⊆ ( 𝑅 supp 𝑍 ) )

Proof

Step Hyp Ref Expression
1 exsimpl ⊢ ( ∃ 𝑦 ( 𝑥 𝑅 𝑦 ∧ 𝑦 ≠ 𝑍 ) → ∃ 𝑦 𝑥 𝑅 𝑦 )
2 pm5.1 ⊢ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 ≠ 𝑍 ) → ( 𝑥 𝑅 𝑦 ↔ 𝑦 ≠ 𝑍 ) )
3 2 eximi ⊢ ( ∃ 𝑦 ( 𝑥 𝑅 𝑦 ∧ 𝑦 ≠ 𝑍 ) → ∃ 𝑦 ( 𝑥 𝑅 𝑦 ↔ 𝑦 ≠ 𝑍 ) )
4 1 3 jca ⊢ ( ∃ 𝑦 ( 𝑥 𝑅 𝑦 ∧ 𝑦 ≠ 𝑍 ) → ( ∃ 𝑦 𝑥 𝑅 𝑦 ∧ ∃ 𝑦 ( 𝑥 𝑅 𝑦 ↔ 𝑦 ≠ 𝑍 ) ) )
5 4 a1i ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( ∃ 𝑦 ( 𝑥 𝑅 𝑦 ∧ 𝑦 ≠ 𝑍 ) → ( ∃ 𝑦 𝑥 𝑅 𝑦 ∧ ∃ 𝑦 ( 𝑥 𝑅 𝑦 ↔ 𝑦 ≠ 𝑍 ) ) ) )
6 5 ss2abdv ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → { 𝑥 ∣ ∃ 𝑦 ( 𝑥 𝑅 𝑦 ∧ 𝑦 ≠ 𝑍 ) } ⊆ { 𝑥 ∣ ( ∃ 𝑦 𝑥 𝑅 𝑦 ∧ ∃ 𝑦 ( 𝑥 𝑅 𝑦 ↔ 𝑦 ≠ 𝑍 ) ) } )
7 cnvimadfsn ⊢ ( ◡ 𝑅 “ ( V ∖ { 𝑍 } ) ) = { 𝑥 ∣ ∃ 𝑦 ( 𝑥 𝑅 𝑦 ∧ 𝑦 ≠ 𝑍 ) }
8 7 a1i ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( ◡ 𝑅 “ ( V ∖ { 𝑍 } ) ) = { 𝑥 ∣ ∃ 𝑦 ( 𝑥 𝑅 𝑦 ∧ 𝑦 ≠ 𝑍 ) } )
9 suppvalbr ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝑅 supp 𝑍 ) = { 𝑥 ∣ ( ∃ 𝑦 𝑥 𝑅 𝑦 ∧ ∃ 𝑦 ( 𝑥 𝑅 𝑦 ↔ 𝑦 ≠ 𝑍 ) ) } )
10 6 8 9 3sstr4d ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( ◡ 𝑅 “ ( V ∖ { 𝑍 } ) ) ⊆ ( 𝑅 supp 𝑍 ) )