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

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) (Proof shortened by AV, 30-Oct-2025)

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 simp1l 
 |-  ( ( ( E : D -1-1-> R /\ F : C -1-1-> D ) /\ ( A e. C /\ B e. C ) /\ A =/= B ) -> E : D -1-1-> R )
2 f1f 
 |-  ( F : C -1-1-> D -> F : C --> D )
3 2 adantl 
 |-  ( ( E : D -1-1-> R /\ F : C -1-1-> D ) -> F : C --> D )
4 3 adantr 
 |-  ( ( ( E : D -1-1-> R /\ F : C -1-1-> D ) /\ ( A e. C /\ B e. C ) ) -> F : C --> D )
5 simpl 
 |-  ( ( A e. C /\ B e. C ) -> A e. C )
6 5 adantl 
 |-  ( ( ( E : D -1-1-> R /\ F : C -1-1-> D ) /\ ( A e. C /\ B e. C ) ) -> A e. C )
7 4 6 ffvelcdmd 
 |-  ( ( ( E : D -1-1-> R /\ F : C -1-1-> D ) /\ ( A e. C /\ B e. C ) ) -> ( F ` A ) e. D )
8 7 3adant3 
 |-  ( ( ( E : D -1-1-> R /\ F : C -1-1-> D ) /\ ( A e. C /\ B e. C ) /\ A =/= B ) -> ( F ` A ) e. D )
9 simpr 
 |-  ( ( A e. C /\ B e. C ) -> B e. C )
10 9 adantl 
 |-  ( ( ( E : D -1-1-> R /\ F : C -1-1-> D ) /\ ( A e. C /\ B e. C ) ) -> B e. C )
11 4 10 ffvelcdmd 
 |-  ( ( ( E : D -1-1-> R /\ F : C -1-1-> D ) /\ ( A e. C /\ B e. C ) ) -> ( F ` B ) e. D )
12 11 3adant3 
 |-  ( ( ( E : D -1-1-> R /\ F : C -1-1-> D ) /\ ( A e. C /\ B e. C ) /\ A =/= B ) -> ( F ` B ) e. D )
13 simpr 
 |-  ( ( E : D -1-1-> R /\ F : C -1-1-> D ) -> F : C -1-1-> D )
14 df-3an 
 |-  ( ( A e. C /\ B e. C /\ A =/= B ) <-> ( ( A e. C /\ B e. C ) /\ A =/= B ) )
15 14 biimpri 
 |-  ( ( ( A e. C /\ B e. C ) /\ A =/= B ) -> ( A e. C /\ B e. C /\ A =/= B ) )
16 dff14i 
 |-  ( ( F : C -1-1-> D /\ ( A e. C /\ B e. C /\ A =/= B ) ) -> ( F ` A ) =/= ( F ` B ) )
17 13 15 16 syl3an132 
 |-  ( ( ( E : D -1-1-> R /\ F : C -1-1-> D ) /\ ( A e. C /\ B e. C ) /\ A =/= B ) -> ( F ` A ) =/= ( F ` B ) )
18 dff14i 
 |-  ( ( E : D -1-1-> R /\ ( ( F ` A ) e. D /\ ( F ` B ) e. D /\ ( F ` A ) =/= ( F ` B ) ) ) -> ( E ` ( F ` A ) ) =/= ( E ` ( F ` B ) ) )
19 1 8 12 17 18 syl13anc 
 |-  ( ( ( E : D -1-1-> R /\ F : C -1-1-> D ) /\ ( A e. C /\ B e. C ) /\ A =/= B ) -> ( E ` ( F ` A ) ) =/= ( E ` ( F ` B ) ) )
20 simpl 
 |-  ( ( ( E ` ( F ` A ) ) = X /\ ( E ` ( F ` B ) ) = Y ) -> ( E ` ( F ` A ) ) = X )
21 simpr 
 |-  ( ( ( E ` ( F ` A ) ) = X /\ ( E ` ( F ` B ) ) = Y ) -> ( E ` ( F ` B ) ) = Y )
22 20 21 neeq12d 
 |-  ( ( ( E ` ( F ` A ) ) = X /\ ( E ` ( F ` B ) ) = Y ) -> ( ( E ` ( F ` A ) ) =/= ( E ` ( F ` B ) ) <-> X =/= Y ) )
23 19 22 syl5ibcom 
 |-  ( ( ( 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 ) )