Theorem intimass

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	intimass	$$⊢\bigcap A\left[B\right]\subseteq \bigcap \left\{x|\exists a\in Ax=a\left[B\right]\right\}$$

Proof

Step	Hyp	Ref	Expression
1		r19.12	$$⊢\exists b\in B\forall a\in A⟨b,y⟩\in a\to \forall a\in A\exists b\in B⟨b,y⟩\in a$$
2		elimaint	$$⊢y\in \bigcap A\left[B\right]\leftrightarrow \exists b\in B\forall a\in A⟨b,y⟩\in a$$
3		elintima	$$⊢y\in \bigcap \left\{x|\exists a\in Ax=a\left[B\right]\right\}\leftrightarrow \forall a\in A\exists b\in B⟨b,y⟩\in a$$
4	1 2 3	3imtr4i	$$⊢y\in \bigcap A\left[B\right]\to y\in \bigcap \left\{x|\exists a\in Ax=a\left[B\right]\right\}$$
5	4	ssriv	$$⊢\bigcap A\left[B\right]\subseteq \bigcap \left\{x|\exists a\in Ax=a\left[B\right]\right\}$$