Theorem imaiinfv

Description: Indexed intersection of an image. (Contributed by Stefan O'Rear, 22-Feb-2015)

	Ref	Expression
Assertion	imaiinfv	$$⊢\left(FFnA\wedge B\subseteq A\right)\to \bigcap _{x\in B}F\left(x\right)=\bigcap F\left[B\right]$$

Proof

Step	Hyp	Ref	Expression
1		fnssres	$$⊢\left(FFnA\wedge B\subseteq A\right)\to \left({F\upharpoonright }_B\right)FnB$$
2		fniinfv	$$⊢\left({F\upharpoonright }_B\right)FnB\to \bigcap _{x\in B}\left({F\upharpoonright }_B\right)\left(x\right)=\bigcap \mathrm{ran}\left({F\upharpoonright }_B\right)$$
3	1 2	syl	$$⊢\left(FFnA\wedge B\subseteq A\right)\to \bigcap _{x\in B}\left({F\upharpoonright }_B\right)\left(x\right)=\bigcap \mathrm{ran}\left({F\upharpoonright }_B\right)$$
4		fvres	$$⊢x\in B\to \left({F\upharpoonright }_B\right)\left(x\right)=F\left(x\right)$$
5	4	iineq2i	$$⊢\bigcap _{x\in B}\left({F\upharpoonright }_B\right)\left(x\right)=\bigcap _{x\in B}F\left(x\right)$$
6	5	eqcomi	$$⊢\bigcap _{x\in B}F\left(x\right)=\bigcap _{x\in B}\left({F\upharpoonright }_B\right)\left(x\right)$$
7		df-ima	$$⊢F\left[B\right]=\mathrm{ran}\left({F\upharpoonright }_B\right)$$
8	7	inteqi	$$⊢\bigcap F\left[B\right]=\bigcap \mathrm{ran}\left({F\upharpoonright }_B\right)$$
9	3 6 8	3eqtr4g	$$⊢\left(FFnA\wedge B\subseteq A\right)\to \bigcap _{x\in B}F\left(x\right)=\bigcap F\left[B\right]$$