Metamath Proof Explorer

Theorem f1cofveqaeqALT

Description: Alternate proof of f1cofveqaeq , 1 essential step shorter, but having more bytes (305 versus 282). (Contributed by AV, 3-Feb-2021) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Assertion f1cofveqaeqALT 
|- ( ( ( 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 f1f 
 |-  ( G : A -1-1-> B -> G : A --> B )
2 fvco3 
 |-  ( ( G : A --> B /\ X e. A ) -> ( ( F o. G ) ` X ) = ( F ` ( G ` X ) ) )
3 2 adantrr 
 |-  ( ( G : A --> B /\ ( X e. A /\ Y e. A ) ) -> ( ( F o. G ) ` X ) = ( F ` ( G ` X ) ) )
4 fvco3 
 |-  ( ( G : A --> B /\ Y e. A ) -> ( ( F o. G ) ` Y ) = ( F ` ( G ` Y ) ) )
5 4 adantrl 
 |-  ( ( G : A --> B /\ ( X e. A /\ Y e. A ) ) -> ( ( F o. G ) ` Y ) = ( F ` ( G ` Y ) ) )
6 3 5 eqeq12d 
 |-  ( ( G : A --> B /\ ( X e. A /\ Y e. A ) ) -> ( ( ( F o. G ) ` X ) = ( ( F o. G ) ` Y ) <-> ( F ` ( G ` X ) ) = ( F ` ( G ` Y ) ) ) )
7 6 ex 
 |-  ( G : A --> B -> ( ( X e. A /\ Y e. A ) -> ( ( ( F o. G ) ` X ) = ( ( F o. G ) ` Y ) <-> ( F ` ( G ` X ) ) = ( F ` ( G ` Y ) ) ) ) )
8 1 7 syl 
 |-  ( G : A -1-1-> B -> ( ( X e. A /\ Y e. A ) -> ( ( ( F o. G ) ` X ) = ( ( F o. G ) ` Y ) <-> ( F ` ( G ` X ) ) = ( F ` ( G ` Y ) ) ) ) )
9 8 adantl 
 |-  ( ( F : B -1-1-> C /\ G : A -1-1-> B ) -> ( ( X e. A /\ Y e. A ) -> ( ( ( F o. G ) ` X ) = ( ( F o. G ) ` Y ) <-> ( F ` ( G ` X ) ) = ( F ` ( G ` Y ) ) ) ) )
10 9 imp 
 |-  ( ( ( F : B -1-1-> C /\ G : A -1-1-> B ) /\ ( X e. A /\ Y e. A ) ) -> ( ( ( F o. G ) ` X ) = ( ( F o. G ) ` Y ) <-> ( F ` ( G ` X ) ) = ( F ` ( G ` Y ) ) ) )
11 f1co 
 |-  ( ( F : B -1-1-> C /\ G : A -1-1-> B ) -> ( F o. G ) : A -1-1-> C )
12 f1veqaeq 
 |-  ( ( ( F o. G ) : A -1-1-> C /\ ( X e. A /\ Y e. A ) ) -> ( ( ( F o. G ) ` X ) = ( ( F o. G ) ` Y ) -> X = Y ) )
13 11 12 sylan 
 |-  ( ( ( F : B -1-1-> C /\ G : A -1-1-> B ) /\ ( X e. A /\ Y e. A ) ) -> ( ( ( F o. G ) ` X ) = ( ( F o. G ) ` Y ) -> X = Y ) )
14 10 13 sylbird 
 |-  ( ( ( F : B -1-1-> C /\ G : A -1-1-> B ) /\ ( X e. A /\ Y e. A ) ) -> ( ( F ` ( G ` X ) ) = ( F ` ( G ` Y ) ) -> X = Y ) )