Metamath Proof Explorer

Theorem imarnf1pr

Description: The image of the range of a function F under a function E if F is a function from a pair into the domain of E . (Contributed by Alexander van der Vekens, 2-Feb-2018)

Ref Expression
Assertion imarnf1pr 
|- ( ( X e. V /\ Y e. W ) -> ( ( ( F : { X , Y } --> dom E /\ E : dom E --> R ) /\ ( ( E ` ( F ` X ) ) = A /\ ( E ` ( F ` Y ) ) = B ) ) -> ( E " ran F ) = { A , B } ) )

Proof

Step Hyp Ref Expression
1 ffn 
 |-  ( E : dom E --> R -> E Fn dom E )
2 1 adantl 
 |-  ( ( F : { X , Y } --> dom E /\ E : dom E --> R ) -> E Fn dom E )
3 2 adantr 
 |-  ( ( ( F : { X , Y } --> dom E /\ E : dom E --> R ) /\ ( X e. V /\ Y e. W ) ) -> E Fn dom E )
4 simpll 
 |-  ( ( ( F : { X , Y } --> dom E /\ E : dom E --> R ) /\ ( X e. V /\ Y e. W ) ) -> F : { X , Y } --> dom E )
5 prid1g 
 |-  ( X e. V -> X e. { X , Y } )
6 5 adantr 
 |-  ( ( X e. V /\ Y e. W ) -> X e. { X , Y } )
7 6 adantl 
 |-  ( ( ( F : { X , Y } --> dom E /\ E : dom E --> R ) /\ ( X e. V /\ Y e. W ) ) -> X e. { X , Y } )
8 4 7 ffvelcdmd 
 |-  ( ( ( F : { X , Y } --> dom E /\ E : dom E --> R ) /\ ( X e. V /\ Y e. W ) ) -> ( F ` X ) e. dom E )
9 prid2g 
 |-  ( Y e. W -> Y e. { X , Y } )
10 9 ad2antll 
 |-  ( ( ( F : { X , Y } --> dom E /\ E : dom E --> R ) /\ ( X e. V /\ Y e. W ) ) -> Y e. { X , Y } )
11 4 10 ffvelcdmd 
 |-  ( ( ( F : { X , Y } --> dom E /\ E : dom E --> R ) /\ ( X e. V /\ Y e. W ) ) -> ( F ` Y ) e. dom E )
12 fnimapr 
 |-  ( ( E Fn dom E /\ ( F ` X ) e. dom E /\ ( F ` Y ) e. dom E ) -> ( E " { ( F ` X ) , ( F ` Y ) } ) = { ( E ` ( F ` X ) ) , ( E ` ( F ` Y ) ) } )
13 3 8 11 12 syl3anc 
 |-  ( ( ( F : { X , Y } --> dom E /\ E : dom E --> R ) /\ ( X e. V /\ Y e. W ) ) -> ( E " { ( F ` X ) , ( F ` Y ) } ) = { ( E ` ( F ` X ) ) , ( E ` ( F ` Y ) ) } )
14 13 ex 
 |-  ( ( F : { X , Y } --> dom E /\ E : dom E --> R ) -> ( ( X e. V /\ Y e. W ) -> ( E " { ( F ` X ) , ( F ` Y ) } ) = { ( E ` ( F ` X ) ) , ( E ` ( F ` Y ) ) } ) )
15 14 adantr 
 |-  ( ( ( F : { X , Y } --> dom E /\ E : dom E --> R ) /\ ( ( E ` ( F ` X ) ) = A /\ ( E ` ( F ` Y ) ) = B ) ) -> ( ( X e. V /\ Y e. W ) -> ( E " { ( F ` X ) , ( F ` Y ) } ) = { ( E ` ( F ` X ) ) , ( E ` ( F ` Y ) ) } ) )
16 15 impcom 
 |-  ( ( ( X e. V /\ Y e. W ) /\ ( ( F : { X , Y } --> dom E /\ E : dom E --> R ) /\ ( ( E ` ( F ` X ) ) = A /\ ( E ` ( F ` Y ) ) = B ) ) ) -> ( E " { ( F ` X ) , ( F ` Y ) } ) = { ( E ` ( F ` X ) ) , ( E ` ( F ` Y ) ) } )
17 ffn 
 |-  ( F : { X , Y } --> dom E -> F Fn { X , Y } )
18 rnfdmpr 
 |-  ( ( X e. V /\ Y e. W ) -> ( F Fn { X , Y } -> ran F = { ( F ` X ) , ( F ` Y ) } ) )
19 17 18 syl5com 
 |-  ( F : { X , Y } --> dom E -> ( ( X e. V /\ Y e. W ) -> ran F = { ( F ` X ) , ( F ` Y ) } ) )
20 19 adantr 
 |-  ( ( F : { X , Y } --> dom E /\ E : dom E --> R ) -> ( ( X e. V /\ Y e. W ) -> ran F = { ( F ` X ) , ( F ` Y ) } ) )
21 20 adantr 
 |-  ( ( ( F : { X , Y } --> dom E /\ E : dom E --> R ) /\ ( ( E ` ( F ` X ) ) = A /\ ( E ` ( F ` Y ) ) = B ) ) -> ( ( X e. V /\ Y e. W ) -> ran F = { ( F ` X ) , ( F ` Y ) } ) )
22 21 impcom 
 |-  ( ( ( X e. V /\ Y e. W ) /\ ( ( F : { X , Y } --> dom E /\ E : dom E --> R ) /\ ( ( E ` ( F ` X ) ) = A /\ ( E ` ( F ` Y ) ) = B ) ) ) -> ran F = { ( F ` X ) , ( F ` Y ) } )
23 22 eqcomd 
 |-  ( ( ( X e. V /\ Y e. W ) /\ ( ( F : { X , Y } --> dom E /\ E : dom E --> R ) /\ ( ( E ` ( F ` X ) ) = A /\ ( E ` ( F ` Y ) ) = B ) ) ) -> { ( F ` X ) , ( F ` Y ) } = ran F )
24 23 imaeq2d 
 |-  ( ( ( X e. V /\ Y e. W ) /\ ( ( F : { X , Y } --> dom E /\ E : dom E --> R ) /\ ( ( E ` ( F ` X ) ) = A /\ ( E ` ( F ` Y ) ) = B ) ) ) -> ( E " { ( F ` X ) , ( F ` Y ) } ) = ( E " ran F ) )
25 preq12 
 |-  ( ( ( E ` ( F ` X ) ) = A /\ ( E ` ( F ` Y ) ) = B ) -> { ( E ` ( F ` X ) ) , ( E ` ( F ` Y ) ) } = { A , B } )
26 25 ad2antll 
 |-  ( ( ( X e. V /\ Y e. W ) /\ ( ( F : { X , Y } --> dom E /\ E : dom E --> R ) /\ ( ( E ` ( F ` X ) ) = A /\ ( E ` ( F ` Y ) ) = B ) ) ) -> { ( E ` ( F ` X ) ) , ( E ` ( F ` Y ) ) } = { A , B } )
27 16 24 26 3eqtr3d 
 |-  ( ( ( X e. V /\ Y e. W ) /\ ( ( F : { X , Y } --> dom E /\ E : dom E --> R ) /\ ( ( E ` ( F ` X ) ) = A /\ ( E ` ( F ` Y ) ) = B ) ) ) -> ( E " ran F ) = { A , B } )
28 27 ex 
 |-  ( ( X e. V /\ Y e. W ) -> ( ( ( F : { X , Y } --> dom E /\ E : dom E --> R ) /\ ( ( E ` ( F ` X ) ) = A /\ ( E ` ( F ` Y ) ) = B ) ) -> ( E " ran F ) = { A , B } ) )