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
|
ffvelrnd |
|- ( ( ( 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
|
ffvelrnd |
|- ( ( ( 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 } ) ) |