Metamath Proof Explorer

Theorem 2f1fvneq

Description: If two one-to-one functions are applied on different arguments, also the values are different. (Contributed by Alexander van der Vekens, 25-Jan-2018)

Ref Expression
Assertion 2f1fvneq 
|- ( ( ( E : D -1-1-> R /\ F : C -1-1-> D ) /\ ( A e. C /\ B e. C ) /\ A =/= B ) -> ( ( ( E ` ( F ` A ) ) = X /\ ( E ` ( F ` B ) ) = Y ) -> X =/= Y ) )

Proof

Step Hyp Ref Expression
1 f1veqaeq 
 |-  ( ( F : C -1-1-> D /\ ( A e. C /\ B e. C ) ) -> ( ( F ` A ) = ( F ` B ) -> A = B ) )
2 1 adantll 
 |-  ( ( ( E : D -1-1-> R /\ F : C -1-1-> D ) /\ ( A e. C /\ B e. C ) ) -> ( ( F ` A ) = ( F ` B ) -> A = B ) )
3 2 necon3ad 
 |-  ( ( ( E : D -1-1-> R /\ F : C -1-1-> D ) /\ ( A e. C /\ B e. C ) ) -> ( A =/= B -> -. ( F ` A ) = ( F ` B ) ) )
4 3 3impia 
 |-  ( ( ( E : D -1-1-> R /\ F : C -1-1-> D ) /\ ( A e. C /\ B e. C ) /\ A =/= B ) -> -. ( F ` A ) = ( F ` B ) )
5 simpll 
 |-  ( ( ( E : D -1-1-> R /\ F : C -1-1-> D ) /\ ( A e. C /\ B e. C ) ) -> E : D -1-1-> R )
6 f1f 
 |-  ( F : C -1-1-> D -> F : C --> D )
7 ffvelrn 
 |-  ( ( F : C --> D /\ A e. C ) -> ( F ` A ) e. D )
8 ffvelrn 
 |-  ( ( F : C --> D /\ B e. C ) -> ( F ` B ) e. D )
9 7 8 anim12dan 
 |-  ( ( F : C --> D /\ ( A e. C /\ B e. C ) ) -> ( ( F ` A ) e. D /\ ( F ` B ) e. D ) )
10 9 ex 
 |-  ( F : C --> D -> ( ( A e. C /\ B e. C ) -> ( ( F ` A ) e. D /\ ( F ` B ) e. D ) ) )
11 6 10 syl 
 |-  ( F : C -1-1-> D -> ( ( A e. C /\ B e. C ) -> ( ( F ` A ) e. D /\ ( F ` B ) e. D ) ) )
12 11 adantl 
 |-  ( ( E : D -1-1-> R /\ F : C -1-1-> D ) -> ( ( A e. C /\ B e. C ) -> ( ( F ` A ) e. D /\ ( F ` B ) e. D ) ) )
13 12 imp 
 |-  ( ( ( E : D -1-1-> R /\ F : C -1-1-> D ) /\ ( A e. C /\ B e. C ) ) -> ( ( F ` A ) e. D /\ ( F ` B ) e. D ) )
14 f1veqaeq 
 |-  ( ( E : D -1-1-> R /\ ( ( F ` A ) e. D /\ ( F ` B ) e. D ) ) -> ( ( E ` ( F ` A ) ) = ( E ` ( F ` B ) ) -> ( F ` A ) = ( F ` B ) ) )
15 5 13 14 syl2anc 
 |-  ( ( ( E : D -1-1-> R /\ F : C -1-1-> D ) /\ ( A e. C /\ B e. C ) ) -> ( ( E ` ( F ` A ) ) = ( E ` ( F ` B ) ) -> ( F ` A ) = ( F ` B ) ) )
16 15 con3dimp 
 |-  ( ( ( ( E : D -1-1-> R /\ F : C -1-1-> D ) /\ ( A e. C /\ B e. C ) ) /\ -. ( F ` A ) = ( F ` B ) ) -> -. ( E ` ( F ` A ) ) = ( E ` ( F ` B ) ) )
17 eqeq12 
 |-  ( ( ( E ` ( F ` A ) ) = X /\ ( E ` ( F ` B ) ) = Y ) -> ( ( E ` ( F ` A ) ) = ( E ` ( F ` B ) ) <-> X = Y ) )
18 17 notbid 
 |-  ( ( ( E ` ( F ` A ) ) = X /\ ( E ` ( F ` B ) ) = Y ) -> ( -. ( E ` ( F ` A ) ) = ( E ` ( F ` B ) ) <-> -. X = Y ) )
19 neqne 
 |-  ( -. X = Y -> X =/= Y )
20 18 19 syl6bi 
 |-  ( ( ( E ` ( F ` A ) ) = X /\ ( E ` ( F ` B ) ) = Y ) -> ( -. ( E ` ( F ` A ) ) = ( E ` ( F ` B ) ) -> X =/= Y ) )
21 16 20 syl5com 
 |-  ( ( ( ( E : D -1-1-> R /\ F : C -1-1-> D ) /\ ( A e. C /\ B e. C ) ) /\ -. ( F ` A ) = ( F ` B ) ) -> ( ( ( E ` ( F ` A ) ) = X /\ ( E ` ( F ` B ) ) = Y ) -> X =/= Y ) )
22 21 ex 
 |-  ( ( ( E : D -1-1-> R /\ F : C -1-1-> D ) /\ ( A e. C /\ B e. C ) ) -> ( -. ( F ` A ) = ( F ` B ) -> ( ( ( E ` ( F ` A ) ) = X /\ ( E ` ( F ` B ) ) = Y ) -> X =/= Y ) ) )
23 22 3adant3 
 |-  ( ( ( E : D -1-1-> R /\ F : C -1-1-> D ) /\ ( A e. C /\ B e. C ) /\ A =/= B ) -> ( -. ( F ` A ) = ( F ` B ) -> ( ( ( E ` ( F ` A ) ) = X /\ ( E ` ( F ` B ) ) = Y ) -> X =/= Y ) ) )
24 4 23 mpd 
 |-  ( ( ( E : D -1-1-> R /\ F : C -1-1-> D ) /\ ( A e. C /\ B e. C ) /\ A =/= B ) -> ( ( ( E ` ( F ` A ) ) = X /\ ( E ` ( F ` B ) ) = Y ) -> X =/= Y ) )