Metamath Proof Explorer

Theorem dfiso2

Description: Alternate definition of an isomorphism of a category, according to definition 3.8 in Adamek p. 28. (Contributed by AV, 10-Apr-2020)

Ref Expression
Hypotheses dfiso2.b 
|- B = ( Base ` C )
dfiso2.h 
|- H = ( Hom ` C )
dfiso2.c 
|- ( ph -> C e. Cat )
dfiso2.i 
|- I = ( Iso ` C )
dfiso2.x 
|- ( ph -> X e. B )
dfiso2.y 
|- ( ph -> Y e. B )
dfiso2.f 
|- ( ph -> F e. ( X H Y ) )
dfiso2.1 
|- .1. = ( Id ` C )
dfiso2.o 
|- .o. = ( <. X , Y >. ( comp ` C ) X )
dfiso2.p 
|- .* = ( <. Y , X >. ( comp ` C ) Y )
Assertion dfiso2 
|- ( ph -> ( F e. ( X I Y ) <-> E. g e. ( Y H X ) ( ( g .o. F ) = ( .1. ` X ) /\ ( F .* g ) = ( .1. ` Y ) ) ) )

Proof

Step Hyp Ref Expression
1 dfiso2.b 
 |-  B = ( Base ` C )
2 dfiso2.h 
 |-  H = ( Hom ` C )
3 dfiso2.c 
 |-  ( ph -> C e. Cat )
4 dfiso2.i 
 |-  I = ( Iso ` C )
5 dfiso2.x 
 |-  ( ph -> X e. B )
6 dfiso2.y 
 |-  ( ph -> Y e. B )
7 dfiso2.f 
 |-  ( ph -> F e. ( X H Y ) )
8 dfiso2.1 
 |-  .1. = ( Id ` C )
9 dfiso2.o 
 |-  .o. = ( <. X , Y >. ( comp ` C ) X )
10 dfiso2.p 
 |-  .* = ( <. Y , X >. ( comp ` C ) Y )
11 eqid 
 |-  ( Inv ` C ) = ( Inv ` C )
12 1 11 3 5 6 4 isoval 
 |-  ( ph -> ( X I Y ) = dom ( X ( Inv ` C ) Y ) )
13 12 eleq2d 
 |-  ( ph -> ( F e. ( X I Y ) <-> F e. dom ( X ( Inv ` C ) Y ) ) )
14 eqid 
 |-  ( Sect ` C ) = ( Sect ` C )
15 1 11 3 5 6 14 invfval 
 |-  ( ph -> ( X ( Inv ` C ) Y ) = ( ( X ( Sect ` C ) Y ) i^i `' ( Y ( Sect ` C ) X ) ) )
16 15 dmeqd 
 |-  ( ph -> dom ( X ( Inv ` C ) Y ) = dom ( ( X ( Sect ` C ) Y ) i^i `' ( Y ( Sect ` C ) X ) ) )
17 16 eleq2d 
 |-  ( ph -> ( F e. dom ( X ( Inv ` C ) Y ) <-> F e. dom ( ( X ( Sect ` C ) Y ) i^i `' ( Y ( Sect ` C ) X ) ) ) )
18 eqid 
 |-  ( comp ` C ) = ( comp ` C )
19 1 2 18 8 14 3 5 6 sectfval 
 |-  ( ph -> ( X ( Sect ` C ) Y ) = { <. f , g >. | ( ( f e. ( X H Y ) /\ g e. ( Y H X ) ) /\ ( g ( <. X , Y >. ( comp ` C ) X ) f ) = ( .1. ` X ) ) } )
20 1 2 18 8 14 3 6 5 sectfval 
 |-  ( ph -> ( Y ( Sect ` C ) X ) = { <. g , f >. | ( ( g e. ( Y H X ) /\ f e. ( X H Y ) ) /\ ( f ( <. Y , X >. ( comp ` C ) Y ) g ) = ( .1. ` Y ) ) } )
21 20 cnveqd 
 |-  ( ph -> `' ( Y ( Sect ` C ) X ) = `' { <. g , f >. | ( ( g e. ( Y H X ) /\ f e. ( X H Y ) ) /\ ( f ( <. Y , X >. ( comp ` C ) Y ) g ) = ( .1. ` Y ) ) } )
22 cnvopab 
 |-  `' { <. g , f >. | ( ( g e. ( Y H X ) /\ f e. ( X H Y ) ) /\ ( f ( <. Y , X >. ( comp ` C ) Y ) g ) = ( .1. ` Y ) ) } = { <. f , g >. | ( ( g e. ( Y H X ) /\ f e. ( X H Y ) ) /\ ( f ( <. Y , X >. ( comp ` C ) Y ) g ) = ( .1. ` Y ) ) }
23 21 22 eqtrdi 
 |-  ( ph -> `' ( Y ( Sect ` C ) X ) = { <. f , g >. | ( ( g e. ( Y H X ) /\ f e. ( X H Y ) ) /\ ( f ( <. Y , X >. ( comp ` C ) Y ) g ) = ( .1. ` Y ) ) } )
24 19 23 ineq12d 
 |-  ( ph -> ( ( X ( Sect ` C ) Y ) i^i `' ( Y ( Sect ` C ) X ) ) = ( { <. f , g >. | ( ( f e. ( X H Y ) /\ g e. ( Y H X ) ) /\ ( g ( <. X , Y >. ( comp ` C ) X ) f ) = ( .1. ` X ) ) } i^i { <. f , g >. | ( ( g e. ( Y H X ) /\ f e. ( X H Y ) ) /\ ( f ( <. Y , X >. ( comp ` C ) Y ) g ) = ( .1. ` Y ) ) } ) )
25 inopab 
 |-  ( { <. f , g >. | ( ( f e. ( X H Y ) /\ g e. ( Y H X ) ) /\ ( g ( <. X , Y >. ( comp ` C ) X ) f ) = ( .1. ` X ) ) } i^i { <. f , g >. | ( ( g e. ( Y H X ) /\ f e. ( X H Y ) ) /\ ( f ( <. Y , X >. ( comp ` C ) Y ) g ) = ( .1. ` Y ) ) } ) = { <. f , g >. | ( ( ( f e. ( X H Y ) /\ g e. ( Y H X ) ) /\ ( g ( <. X , Y >. ( comp ` C ) X ) f ) = ( .1. ` X ) ) /\ ( ( g e. ( Y H X ) /\ f e. ( X H Y ) ) /\ ( f ( <. Y , X >. ( comp ` C ) Y ) g ) = ( .1. ` Y ) ) ) }
26 an4 
 |-  ( ( ( ( f e. ( X H Y ) /\ g e. ( Y H X ) ) /\ ( g ( <. X , Y >. ( comp ` C ) X ) f ) = ( .1. ` X ) ) /\ ( ( g e. ( Y H X ) /\ f e. ( X H Y ) ) /\ ( f ( <. Y , X >. ( comp ` C ) Y ) g ) = ( .1. ` Y ) ) ) <-> ( ( ( f e. ( X H Y ) /\ g e. ( Y H X ) ) /\ ( g e. ( Y H X ) /\ f e. ( X H Y ) ) ) /\ ( ( g ( <. X , Y >. ( comp ` C ) X ) f ) = ( .1. ` X ) /\ ( f ( <. Y , X >. ( comp ` C ) Y ) g ) = ( .1. ` Y ) ) ) )
27 an42 
 |-  ( ( ( f e. ( X H Y ) /\ g e. ( Y H X ) ) /\ ( g e. ( Y H X ) /\ f e. ( X H Y ) ) ) <-> ( ( f e. ( X H Y ) /\ g e. ( Y H X ) ) /\ ( f e. ( X H Y ) /\ g e. ( Y H X ) ) ) )
28 anidm 
 |-  ( ( ( f e. ( X H Y ) /\ g e. ( Y H X ) ) /\ ( f e. ( X H Y ) /\ g e. ( Y H X ) ) ) <-> ( f e. ( X H Y ) /\ g e. ( Y H X ) ) )
29 27 28 bitri 
 |-  ( ( ( f e. ( X H Y ) /\ g e. ( Y H X ) ) /\ ( g e. ( Y H X ) /\ f e. ( X H Y ) ) ) <-> ( f e. ( X H Y ) /\ g e. ( Y H X ) ) )
30 29 anbi1i 
 |-  ( ( ( ( f e. ( X H Y ) /\ g e. ( Y H X ) ) /\ ( g e. ( Y H X ) /\ f e. ( X H Y ) ) ) /\ ( ( g ( <. X , Y >. ( comp ` C ) X ) f ) = ( .1. ` X ) /\ ( f ( <. Y , X >. ( comp ` C ) Y ) g ) = ( .1. ` Y ) ) ) <-> ( ( f e. ( X H Y ) /\ g e. ( Y H X ) ) /\ ( ( g ( <. X , Y >. ( comp ` C ) X ) f ) = ( .1. ` X ) /\ ( f ( <. Y , X >. ( comp ` C ) Y ) g ) = ( .1. ` Y ) ) ) )
31 26 30 bitri 
 |-  ( ( ( ( f e. ( X H Y ) /\ g e. ( Y H X ) ) /\ ( g ( <. X , Y >. ( comp ` C ) X ) f ) = ( .1. ` X ) ) /\ ( ( g e. ( Y H X ) /\ f e. ( X H Y ) ) /\ ( f ( <. Y , X >. ( comp ` C ) Y ) g ) = ( .1. ` Y ) ) ) <-> ( ( f e. ( X H Y ) /\ g e. ( Y H X ) ) /\ ( ( g ( <. X , Y >. ( comp ` C ) X ) f ) = ( .1. ` X ) /\ ( f ( <. Y , X >. ( comp ` C ) Y ) g ) = ( .1. ` Y ) ) ) )
32 31 opabbii 
 |-  { <. f , g >. | ( ( ( f e. ( X H Y ) /\ g e. ( Y H X ) ) /\ ( g ( <. X , Y >. ( comp ` C ) X ) f ) = ( .1. ` X ) ) /\ ( ( g e. ( Y H X ) /\ f e. ( X H Y ) ) /\ ( f ( <. Y , X >. ( comp ` C ) Y ) g ) = ( .1. ` Y ) ) ) } = { <. f , g >. | ( ( f e. ( X H Y ) /\ g e. ( Y H X ) ) /\ ( ( g ( <. X , Y >. ( comp ` C ) X ) f ) = ( .1. ` X ) /\ ( f ( <. Y , X >. ( comp ` C ) Y ) g ) = ( .1. ` Y ) ) ) }
33 25 32 eqtri 
 |-  ( { <. f , g >. | ( ( f e. ( X H Y ) /\ g e. ( Y H X ) ) /\ ( g ( <. X , Y >. ( comp ` C ) X ) f ) = ( .1. ` X ) ) } i^i { <. f , g >. | ( ( g e. ( Y H X ) /\ f e. ( X H Y ) ) /\ ( f ( <. Y , X >. ( comp ` C ) Y ) g ) = ( .1. ` Y ) ) } ) = { <. f , g >. | ( ( f e. ( X H Y ) /\ g e. ( Y H X ) ) /\ ( ( g ( <. X , Y >. ( comp ` C ) X ) f ) = ( .1. ` X ) /\ ( f ( <. Y , X >. ( comp ` C ) Y ) g ) = ( .1. ` Y ) ) ) }
34 24 33 eqtrdi 
 |-  ( ph -> ( ( X ( Sect ` C ) Y ) i^i `' ( Y ( Sect ` C ) X ) ) = { <. f , g >. | ( ( f e. ( X H Y ) /\ g e. ( Y H X ) ) /\ ( ( g ( <. X , Y >. ( comp ` C ) X ) f ) = ( .1. ` X ) /\ ( f ( <. Y , X >. ( comp ` C ) Y ) g ) = ( .1. ` Y ) ) ) } )
35 34 dmeqd 
 |-  ( ph -> dom ( ( X ( Sect ` C ) Y ) i^i `' ( Y ( Sect ` C ) X ) ) = dom { <. f , g >. | ( ( f e. ( X H Y ) /\ g e. ( Y H X ) ) /\ ( ( g ( <. X , Y >. ( comp ` C ) X ) f ) = ( .1. ` X ) /\ ( f ( <. Y , X >. ( comp ` C ) Y ) g ) = ( .1. ` Y ) ) ) } )
36 dmopab 
 |-  dom { <. f , g >. | ( ( f e. ( X H Y ) /\ g e. ( Y H X ) ) /\ ( ( g ( <. X , Y >. ( comp ` C ) X ) f ) = ( .1. ` X ) /\ ( f ( <. Y , X >. ( comp ` C ) Y ) g ) = ( .1. ` Y ) ) ) } = { f | E. g ( ( f e. ( X H Y ) /\ g e. ( Y H X ) ) /\ ( ( g ( <. X , Y >. ( comp ` C ) X ) f ) = ( .1. ` X ) /\ ( f ( <. Y , X >. ( comp ` C ) Y ) g ) = ( .1. ` Y ) ) ) }
37 35 36 eqtrdi 
 |-  ( ph -> dom ( ( X ( Sect ` C ) Y ) i^i `' ( Y ( Sect ` C ) X ) ) = { f | E. g ( ( f e. ( X H Y ) /\ g e. ( Y H X ) ) /\ ( ( g ( <. X , Y >. ( comp ` C ) X ) f ) = ( .1. ` X ) /\ ( f ( <. Y , X >. ( comp ` C ) Y ) g ) = ( .1. ` Y ) ) ) } )
38 37 eleq2d 
 |-  ( ph -> ( F e. dom ( ( X ( Sect ` C ) Y ) i^i `' ( Y ( Sect ` C ) X ) ) <-> F e. { f | E. g ( ( f e. ( X H Y ) /\ g e. ( Y H X ) ) /\ ( ( g ( <. X , Y >. ( comp ` C ) X ) f ) = ( .1. ` X ) /\ ( f ( <. Y , X >. ( comp ` C ) Y ) g ) = ( .1. ` Y ) ) ) } ) )
39 eleq1 
 |-  ( f = F -> ( f e. ( X H Y ) <-> F e. ( X H Y ) ) )
40 39 anbi1d 
 |-  ( f = F -> ( ( f e. ( X H Y ) /\ g e. ( Y H X ) ) <-> ( F e. ( X H Y ) /\ g e. ( Y H X ) ) ) )
41 oveq2 
 |-  ( f = F -> ( g ( <. X , Y >. ( comp ` C ) X ) f ) = ( g ( <. X , Y >. ( comp ` C ) X ) F ) )
42 41 eqeq1d 
 |-  ( f = F -> ( ( g ( <. X , Y >. ( comp ` C ) X ) f ) = ( .1. ` X ) <-> ( g ( <. X , Y >. ( comp ` C ) X ) F ) = ( .1. ` X ) ) )
43 oveq1 
 |-  ( f = F -> ( f ( <. Y , X >. ( comp ` C ) Y ) g ) = ( F ( <. Y , X >. ( comp ` C ) Y ) g ) )
44 43 eqeq1d 
 |-  ( f = F -> ( ( f ( <. Y , X >. ( comp ` C ) Y ) g ) = ( .1. ` Y ) <-> ( F ( <. Y , X >. ( comp ` C ) Y ) g ) = ( .1. ` Y ) ) )
45 42 44 anbi12d 
 |-  ( f = F -> ( ( ( g ( <. X , Y >. ( comp ` C ) X ) f ) = ( .1. ` X ) /\ ( f ( <. Y , X >. ( comp ` C ) Y ) g ) = ( .1. ` Y ) ) <-> ( ( g ( <. X , Y >. ( comp ` C ) X ) F ) = ( .1. ` X ) /\ ( F ( <. Y , X >. ( comp ` C ) Y ) g ) = ( .1. ` Y ) ) ) )
46 40 45 anbi12d 
 |-  ( f = F -> ( ( ( f e. ( X H Y ) /\ g e. ( Y H X ) ) /\ ( ( g ( <. X , Y >. ( comp ` C ) X ) f ) = ( .1. ` X ) /\ ( f ( <. Y , X >. ( comp ` C ) Y ) g ) = ( .1. ` Y ) ) ) <-> ( ( F e. ( X H Y ) /\ g e. ( Y H X ) ) /\ ( ( g ( <. X , Y >. ( comp ` C ) X ) F ) = ( .1. ` X ) /\ ( F ( <. Y , X >. ( comp ` C ) Y ) g ) = ( .1. ` Y ) ) ) ) )
47 46 exbidv 
 |-  ( f = F -> ( E. g ( ( f e. ( X H Y ) /\ g e. ( Y H X ) ) /\ ( ( g ( <. X , Y >. ( comp ` C ) X ) f ) = ( .1. ` X ) /\ ( f ( <. Y , X >. ( comp ` C ) Y ) g ) = ( .1. ` Y ) ) ) <-> E. g ( ( F e. ( X H Y ) /\ g e. ( Y H X ) ) /\ ( ( g ( <. X , Y >. ( comp ` C ) X ) F ) = ( .1. ` X ) /\ ( F ( <. Y , X >. ( comp ` C ) Y ) g ) = ( .1. ` Y ) ) ) ) )
48 47 elabg 
 |-  ( F e. ( X H Y ) -> ( F e. { f | E. g ( ( f e. ( X H Y ) /\ g e. ( Y H X ) ) /\ ( ( g ( <. X , Y >. ( comp ` C ) X ) f ) = ( .1. ` X ) /\ ( f ( <. Y , X >. ( comp ` C ) Y ) g ) = ( .1. ` Y ) ) ) } <-> E. g ( ( F e. ( X H Y ) /\ g e. ( Y H X ) ) /\ ( ( g ( <. X , Y >. ( comp ` C ) X ) F ) = ( .1. ` X ) /\ ( F ( <. Y , X >. ( comp ` C ) Y ) g ) = ( .1. ` Y ) ) ) ) )
49 7 48 syl 
 |-  ( ph -> ( F e. { f | E. g ( ( f e. ( X H Y ) /\ g e. ( Y H X ) ) /\ ( ( g ( <. X , Y >. ( comp ` C ) X ) f ) = ( .1. ` X ) /\ ( f ( <. Y , X >. ( comp ` C ) Y ) g ) = ( .1. ` Y ) ) ) } <-> E. g ( ( F e. ( X H Y ) /\ g e. ( Y H X ) ) /\ ( ( g ( <. X , Y >. ( comp ` C ) X ) F ) = ( .1. ` X ) /\ ( F ( <. Y , X >. ( comp ` C ) Y ) g ) = ( .1. ` Y ) ) ) ) )
50 7 biantrurd 
 |-  ( ph -> ( g e. ( Y H X ) <-> ( F e. ( X H Y ) /\ g e. ( Y H X ) ) ) )
51 50 bicomd 
 |-  ( ph -> ( ( F e. ( X H Y ) /\ g e. ( Y H X ) ) <-> g e. ( Y H X ) ) )
52 9 a1i 
 |-  ( ph -> .o. = ( <. X , Y >. ( comp ` C ) X ) )
53 52 eqcomd 
 |-  ( ph -> ( <. X , Y >. ( comp ` C ) X ) = .o. )
54 53 oveqd 
 |-  ( ph -> ( g ( <. X , Y >. ( comp ` C ) X ) F ) = ( g .o. F ) )
55 54 eqeq1d 
 |-  ( ph -> ( ( g ( <. X , Y >. ( comp ` C ) X ) F ) = ( .1. ` X ) <-> ( g .o. F ) = ( .1. ` X ) ) )
56 10 a1i 
 |-  ( ph -> .* = ( <. Y , X >. ( comp ` C ) Y ) )
57 56 eqcomd 
 |-  ( ph -> ( <. Y , X >. ( comp ` C ) Y ) = .* )
58 57 oveqd 
 |-  ( ph -> ( F ( <. Y , X >. ( comp ` C ) Y ) g ) = ( F .* g ) )
59 58 eqeq1d 
 |-  ( ph -> ( ( F ( <. Y , X >. ( comp ` C ) Y ) g ) = ( .1. ` Y ) <-> ( F .* g ) = ( .1. ` Y ) ) )
60 55 59 anbi12d 
 |-  ( ph -> ( ( ( g ( <. X , Y >. ( comp ` C ) X ) F ) = ( .1. ` X ) /\ ( F ( <. Y , X >. ( comp ` C ) Y ) g ) = ( .1. ` Y ) ) <-> ( ( g .o. F ) = ( .1. ` X ) /\ ( F .* g ) = ( .1. ` Y ) ) ) )
61 51 60 anbi12d 
 |-  ( ph -> ( ( ( F e. ( X H Y ) /\ g e. ( Y H X ) ) /\ ( ( g ( <. X , Y >. ( comp ` C ) X ) F ) = ( .1. ` X ) /\ ( F ( <. Y , X >. ( comp ` C ) Y ) g ) = ( .1. ` Y ) ) ) <-> ( g e. ( Y H X ) /\ ( ( g .o. F ) = ( .1. ` X ) /\ ( F .* g ) = ( .1. ` Y ) ) ) ) )
62 61 exbidv 
 |-  ( ph -> ( E. g ( ( F e. ( X H Y ) /\ g e. ( Y H X ) ) /\ ( ( g ( <. X , Y >. ( comp ` C ) X ) F ) = ( .1. ` X ) /\ ( F ( <. Y , X >. ( comp ` C ) Y ) g ) = ( .1. ` Y ) ) ) <-> E. g ( g e. ( Y H X ) /\ ( ( g .o. F ) = ( .1. ` X ) /\ ( F .* g ) = ( .1. ` Y ) ) ) ) )
63 df-rex 
 |-  ( E. g e. ( Y H X ) ( ( g .o. F ) = ( .1. ` X ) /\ ( F .* g ) = ( .1. ` Y ) ) <-> E. g ( g e. ( Y H X ) /\ ( ( g .o. F ) = ( .1. ` X ) /\ ( F .* g ) = ( .1. ` Y ) ) ) )
64 62 63 bitr4di 
 |-  ( ph -> ( E. g ( ( F e. ( X H Y ) /\ g e. ( Y H X ) ) /\ ( ( g ( <. X , Y >. ( comp ` C ) X ) F ) = ( .1. ` X ) /\ ( F ( <. Y , X >. ( comp ` C ) Y ) g ) = ( .1. ` Y ) ) ) <-> E. g e. ( Y H X ) ( ( g .o. F ) = ( .1. ` X ) /\ ( F .* g ) = ( .1. ` Y ) ) ) )
65 38 49 64 3bitrd 
 |-  ( ph -> ( F e. dom ( ( X ( Sect ` C ) Y ) i^i `' ( Y ( Sect ` C ) X ) ) <-> E. g e. ( Y H X ) ( ( g .o. F ) = ( .1. ` X ) /\ ( F .* g ) = ( .1. ` Y ) ) ) )
66 13 17 65 3bitrd 
 |-  ( ph -> ( F e. ( X I Y ) <-> E. g e. ( Y H X ) ( ( g .o. F ) = ( .1. ` X ) /\ ( F .* g ) = ( .1. ` Y ) ) ) )