Theorem intimass2

Description: The image under the intersection of relations is a subset of the intersection of the images. (Contributed by RP, 13-Apr-2020)

	Ref	Expression
Assertion	intimass2	⊢ ( ∩ 𝐴 “ 𝐵 ) ⊆ ∩ 𝑥 ∈ 𝐴 ( 𝑥 “ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		intimass	⊢ ( ∩ 𝐴 “ 𝐵 ) ⊆ ∩ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝑥 “ 𝐵 ) }
2		intima0	⊢ ∩ 𝑥 ∈ 𝐴 ( 𝑥 “ 𝐵 ) = ∩ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝑥 “ 𝐵 ) }
3	1 2	sseqtrri	⊢ ( ∩ 𝐴 “ 𝐵 ) ⊆ ∩ 𝑥 ∈ 𝐴 ( 𝑥 “ 𝐵 )