Theorem rnin

Description: The range of an intersection belongs the intersection of ranges. Theorem 9 of Suppes p. 60. (Contributed by NM, 15-Sep-2004)

	Ref	Expression
Assertion	rnin	|- ran ( A i^i B ) C_ ( ran A i^i ran B )

Proof

Step	Hyp	Ref	Expression
1		cnvin	|- `' ( A i^i B ) = ( `' A i^i `' B )
2	1	dmeqi	|- dom `' ( A i^i B ) = dom ( `' A i^i `' B )
3		dmin	|- dom ( `' A i^i `' B ) C_ ( dom `' A i^i dom `' B )
4	2 3	eqsstri	|- dom `' ( A i^i B ) C_ ( dom `' A i^i dom `' B )
5		df-rn	|- ran ( A i^i B ) = dom `' ( A i^i B )
6		df-rn	|- ran A = dom `' A
7		df-rn	|- ran B = dom `' B
8	6 7	ineq12i	|- ( ran A i^i ran B ) = ( dom `' A i^i dom `' B )
9	4 5 8	3sstr4i	|- ran ( A i^i B ) C_ ( ran A i^i ran B )