Metamath Proof Explorer

Theorem f1cofveqaeq

Description: If the values of a composition of one-to-one functions for two arguments are equal, the arguments themselves must be equal. (Contributed by AV, 3-Feb-2021)

Ref Expression
Assertion f1cofveqaeq 
|- ( ( ( F : B -1-1-> C /\ G : A -1-1-> B ) /\ ( X e. A /\ Y e. A ) ) -> ( ( F ` ( G ` X ) ) = ( F ` ( G ` Y ) ) -> X = Y ) )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( F : B -1-1-> C /\ G : A -1-1-> B ) -> F : B -1-1-> C )
2 f1f 
 |-  ( G : A -1-1-> B -> G : A --> B )
3 ffvelrn 
 |-  ( ( G : A --> B /\ X e. A ) -> ( G ` X ) e. B )
4 3 ex 
 |-  ( G : A --> B -> ( X e. A -> ( G ` X ) e. B ) )
5 ffvelrn 
 |-  ( ( G : A --> B /\ Y e. A ) -> ( G ` Y ) e. B )
6 5 ex 
 |-  ( G : A --> B -> ( Y e. A -> ( G ` Y ) e. B ) )
7 4 6 anim12d 
 |-  ( G : A --> B -> ( ( X e. A /\ Y e. A ) -> ( ( G ` X ) e. B /\ ( G ` Y ) e. B ) ) )
8 2 7 syl 
 |-  ( G : A -1-1-> B -> ( ( X e. A /\ Y e. A ) -> ( ( G ` X ) e. B /\ ( G ` Y ) e. B ) ) )
9 8 adantl 
 |-  ( ( F : B -1-1-> C /\ G : A -1-1-> B ) -> ( ( X e. A /\ Y e. A ) -> ( ( G ` X ) e. B /\ ( G ` Y ) e. B ) ) )
10 9 imp 
 |-  ( ( ( F : B -1-1-> C /\ G : A -1-1-> B ) /\ ( X e. A /\ Y e. A ) ) -> ( ( G ` X ) e. B /\ ( G ` Y ) e. B ) )
11 f1veqaeq 
 |-  ( ( F : B -1-1-> C /\ ( ( G ` X ) e. B /\ ( G ` Y ) e. B ) ) -> ( ( F ` ( G ` X ) ) = ( F ` ( G ` Y ) ) -> ( G ` X ) = ( G ` Y ) ) )
12 1 10 11 syl2an2r 
 |-  ( ( ( F : B -1-1-> C /\ G : A -1-1-> B ) /\ ( X e. A /\ Y e. A ) ) -> ( ( F ` ( G ` X ) ) = ( F ` ( G ` Y ) ) -> ( G ` X ) = ( G ` Y ) ) )
13 f1veqaeq 
 |-  ( ( G : A -1-1-> B /\ ( X e. A /\ Y e. A ) ) -> ( ( G ` X ) = ( G ` Y ) -> X = Y ) )
14 13 adantll 
 |-  ( ( ( F : B -1-1-> C /\ G : A -1-1-> B ) /\ ( X e. A /\ Y e. A ) ) -> ( ( G ` X ) = ( G ` Y ) -> X = Y ) )
15 12 14 syld 
 |-  ( ( ( F : B -1-1-> C /\ G : A -1-1-> B ) /\ ( X e. A /\ Y e. A ) ) -> ( ( F ` ( G ` X ) ) = ( F ` ( G ` Y ) ) -> X = Y ) )