This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 eqabri 
 |-  ( 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 biimtrid 
 |-  ( 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 )