Metamath Proof Explorer

Theorem invfun

Description: The inverse relation is a function, which is to say that every morphism has at most one inverse. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Hypotheses invfval.b 
|- B = ( Base ` C )
invfval.n 
|- N = ( Inv ` C )
invfval.c 
|- ( ph -> C e. Cat )
invfval.x 
|- ( ph -> X e. B )
invfval.y 
|- ( ph -> Y e. B )
Assertion invfun 
|- ( ph -> Fun ( X N Y ) )

Proof

Step Hyp Ref Expression
1 invfval.b 
 |-  B = ( Base ` C )
2 invfval.n 
 |-  N = ( Inv ` C )
3 invfval.c 
 |-  ( ph -> C e. Cat )
4 invfval.x 
 |-  ( ph -> X e. B )
5 invfval.y 
 |-  ( ph -> Y e. B )
6 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
7 1 2 3 4 5 6 invss 
 |-  ( ph -> ( X N Y ) C_ ( ( X ( Hom ` C ) Y ) X. ( Y ( Hom ` C ) X ) ) )
8 relxp 
 |-  Rel ( ( X ( Hom ` C ) Y ) X. ( Y ( Hom ` C ) X ) )
9 relss 
 |-  ( ( X N Y ) C_ ( ( X ( Hom ` C ) Y ) X. ( Y ( Hom ` C ) X ) ) -> ( Rel ( ( X ( Hom ` C ) Y ) X. ( Y ( Hom ` C ) X ) ) -> Rel ( X N Y ) ) )
10 7 8 9 mpisyl 
 |-  ( ph -> Rel ( X N Y ) )
11 eqid 
 |-  ( Sect ` C ) = ( Sect ` C )
12 3 adantr 
 |-  ( ( ph /\ ( f ( X N Y ) g /\ f ( X N Y ) h ) ) -> C e. Cat )
13 5 adantr 
 |-  ( ( ph /\ ( f ( X N Y ) g /\ f ( X N Y ) h ) ) -> Y e. B )
14 4 adantr 
 |-  ( ( ph /\ ( f ( X N Y ) g /\ f ( X N Y ) h ) ) -> X e. B )
15 1 2 3 4 5 11 isinv 
 |-  ( ph -> ( f ( X N Y ) g <-> ( f ( X ( Sect ` C ) Y ) g /\ g ( Y ( Sect ` C ) X ) f ) ) )
16 15 simplbda 
 |-  ( ( ph /\ f ( X N Y ) g ) -> g ( Y ( Sect ` C ) X ) f )
17 16 adantrr 
 |-  ( ( ph /\ ( f ( X N Y ) g /\ f ( X N Y ) h ) ) -> g ( Y ( Sect ` C ) X ) f )
18 1 2 3 4 5 11 isinv 
 |-  ( ph -> ( f ( X N Y ) h <-> ( f ( X ( Sect ` C ) Y ) h /\ h ( Y ( Sect ` C ) X ) f ) ) )
19 18 simprbda 
 |-  ( ( ph /\ f ( X N Y ) h ) -> f ( X ( Sect ` C ) Y ) h )
20 19 adantrl 
 |-  ( ( ph /\ ( f ( X N Y ) g /\ f ( X N Y ) h ) ) -> f ( X ( Sect ` C ) Y ) h )
21 1 11 12 13 14 17 20 sectcan 
 |-  ( ( ph /\ ( f ( X N Y ) g /\ f ( X N Y ) h ) ) -> g = h )
22 21 ex 
 |-  ( ph -> ( ( f ( X N Y ) g /\ f ( X N Y ) h ) -> g = h ) )
23 22 alrimiv 
 |-  ( ph -> A. h ( ( f ( X N Y ) g /\ f ( X N Y ) h ) -> g = h ) )
24 23 alrimivv 
 |-  ( ph -> A. f A. g A. h ( ( f ( X N Y ) g /\ f ( X N Y ) h ) -> g = h ) )
25 dffun2 
 |-  ( Fun ( X N Y ) <-> ( Rel ( X N Y ) /\ A. f A. g A. h ( ( f ( X N Y ) g /\ f ( X N Y ) h ) -> g = h ) ) )
26 10 24 25 sylanbrc 
 |-  ( ph -> Fun ( X N Y ) )