Metamath Proof Explorer


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 )