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 𝑍 ) )