Theorem rnmposs

Description: The range of an operation given by the maps-to notation as a subset. (Contributed by Thierry Arnoux, 23-May-2017)

	Ref	Expression
Hypothesis	rnmposs.1	|- F = ( x e. A , y e. B |-> C )
Assertion	rnmposs	|- ( A. x e. A A. y e. B C e. D -> ran F C_ D )

Proof

Step	Hyp	Ref	Expression
1		rnmposs.1	|- F = ( x e. A , y e. B |-> C )
2	1	rnmpo	|- ran F = { z | E. x e. A E. y e. B z = C }
3	2	abeq2i	|- ( z e. ran F <-> E. x e. A E. y e. B z = C )
4		2r19.29	|- ( ( A. x e. A A. y e. B C e. D /\ E. x e. A E. y e. B z = C ) -> E. x e. A E. y e. B ( C e. D /\ z = C ) )
5		eleq1	|- ( z = C -> ( z e. D <-> C e. D ) )
6	5	biimparc	|- ( ( C e. D /\ z = C ) -> z e. D )
7	6	a1i	|- ( ( x e. A /\ y e. B ) -> ( ( C e. D /\ z = C ) -> z e. D ) )
8	7	rexlimivv	|- ( E. x e. A E. y e. B ( C e. D /\ z = C ) -> z e. D )
9	4 8	syl	|- ( ( A. x e. A A. y e. B C e. D /\ E. x e. A E. y e. B z = C ) -> z e. D )
10	9	ex	|- ( A. x e. A A. y e. B C e. D -> ( E. x e. A E. y e. B z = C -> z e. D ) )
11	3 10	syl5bi	|- ( A. x e. A A. y e. B C e. D -> ( z e. ran F -> z e. D ) )
12	11	ssrdv	|- ( A. x e. A A. y e. B C e. D -> ran F C_ D )