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 φ C Cat
dfiso2.i I = Iso C
dfiso2.x φ X B
dfiso2.y φ Y B
dfiso2.f φ F X H Y
dfiso2.1 1 ˙ = Id C
dfiso2.o No typesetting found for |- .o. = ( <. X , Y >. ( comp ` C ) X ) with typecode |-
dfiso2.p ˙ = Y X comp C Y
Assertion dfiso2 Could not format assertion : No typesetting found for |- ( ph -> ( F e. ( X I Y ) <-> E. g e. ( Y H X ) ( ( g .o. F ) = ( .1. ` X ) /\ ( F .* g ) = ( .1. ` Y ) ) ) ) with typecode |-

Proof

Step Hyp Ref Expression
1 dfiso2.b B = Base C
2 dfiso2.h H = Hom C
3 dfiso2.c φ C Cat
4 dfiso2.i I = Iso C
5 dfiso2.x φ X B
6 dfiso2.y φ Y B
7 dfiso2.f φ F X H Y
8 dfiso2.1 1 ˙ = Id C
9 dfiso2.o Could not format .o. = ( <. X , Y >. ( comp ` C ) X ) : No typesetting found for |- .o. = ( <. X , Y >. ( comp ` C ) X ) with typecode |-
10 dfiso2.p ˙ = Y X comp C Y
11 eqid Inv C = Inv C
12 1 11 3 5 6 4 isoval φ X I Y = dom X Inv C Y
13 12 eleq2d φ F X I Y F dom X Inv C Y
14 eqid Sect C = Sect C
15 1 11 3 5 6 14 invfval φ X Inv C Y = X Sect C Y Y Sect C X -1
16 15 dmeqd φ dom X Inv C Y = dom X Sect C Y Y Sect C X -1
17 16 eleq2d φ F dom X Inv C Y F dom X Sect C Y Y Sect C X -1
18 eqid comp C = comp C
19 1 2 18 8 14 3 5 6 sectfval φ X Sect C Y = f g | f X H Y g Y H X g X Y comp C X f = 1 ˙ X
20 1 2 18 8 14 3 6 5 sectfval φ Y Sect C X = g f | g Y H X f X H Y f Y X comp C Y g = 1 ˙ Y
21 20 cnveqd φ Y Sect C X -1 = g f | g Y H X f X H Y f Y X comp C Y g = 1 ˙ Y -1
22 cnvopab g f | g Y H X f X H Y f Y X comp C Y g = 1 ˙ Y -1 = f g | g Y H X f X H Y f Y X comp C Y g = 1 ˙ Y
23 21 22 eqtrdi φ Y Sect C X -1 = f g | g Y H X f X H Y f Y X comp C Y g = 1 ˙ Y
24 19 23 ineq12d φ X Sect C Y Y Sect C X -1 = f g | f X H Y g Y H X g X Y comp C X f = 1 ˙ X f g | g Y H X f X H Y f Y X comp C Y g = 1 ˙ Y
25 inopab f g | f X H Y g Y H X g X Y comp C X f = 1 ˙ X f g | g Y H X f X H Y f Y X comp C Y g = 1 ˙ Y = f g | f X H Y g Y H X g X Y comp C X f = 1 ˙ X g Y H X f X H Y f Y X comp C Y g = 1 ˙ Y
26 an4 f X H Y g Y H X g X Y comp C X f = 1 ˙ X g Y H X f X H Y f Y X comp C Y g = 1 ˙ Y f X H Y g Y H X g Y H X f X H Y g X Y comp C X f = 1 ˙ X f Y X comp C Y g = 1 ˙ Y
27 an42 f X H Y g Y H X g Y H X f X H Y f X H Y g Y H X f X H Y g Y H X
28 anidm f X H Y g Y H X f X H Y g Y H X f X H Y g Y H X
29 27 28 bitri f X H Y g Y H X g Y H X f X H Y f X H Y g Y H X
30 29 anbi1i f X H Y g Y H X g Y H X f X H Y g X Y comp C X f = 1 ˙ X f Y X comp C Y g = 1 ˙ Y f X H Y g 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 X H Y g Y H X g X Y comp C X f = 1 ˙ X g Y H X f X H Y f Y X comp C Y g = 1 ˙ Y f X H Y g 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 X H Y g Y H X g X Y comp C X f = 1 ˙ X g Y H X f X H Y f Y X comp C Y g = 1 ˙ Y = f g | f X H Y g 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 X H Y g Y H X g X Y comp C X f = 1 ˙ X f g | g Y H X f X H Y f Y X comp C Y g = 1 ˙ Y = f g | f X H Y g 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 φ X Sect C Y Y Sect C X -1 = f g | f X H Y g Y H X g X Y comp C X f = 1 ˙ X f Y X comp C Y g = 1 ˙ Y
35 34 dmeqd φ dom X Sect C Y Y Sect C X -1 = dom f g | f X H Y g 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 X H Y g Y H X g X Y comp C X f = 1 ˙ X f Y X comp C Y g = 1 ˙ Y = f | g f X H Y g 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 φ dom X Sect C Y Y Sect C X -1 = f | g f X H Y g Y H X g X Y comp C X f = 1 ˙ X f Y X comp C Y g = 1 ˙ Y
38 37 eleq2d φ F dom X Sect C Y Y Sect C X -1 F f | g f X H Y g 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 X H Y F X H Y
40 39 anbi1d f = F f X H Y g Y H X F X H Y g 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 X H Y g Y H X g X Y comp C X f = 1 ˙ X f Y X comp C Y g = 1 ˙ Y F X H Y g 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 g f X H Y g Y H X g X Y comp C X f = 1 ˙ X f Y X comp C Y g = 1 ˙ Y g F X H Y g 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 X H Y F f | g f X H Y g Y H X g X Y comp C X f = 1 ˙ X f Y X comp C Y g = 1 ˙ Y g F X H Y g 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 φ F f | g f X H Y g Y H X g X Y comp C X f = 1 ˙ X f Y X comp C Y g = 1 ˙ Y g F X H Y g Y H X g X Y comp C X F = 1 ˙ X F Y X comp C Y g = 1 ˙ Y
50 7 biantrurd φ g Y H X F X H Y g Y H X
51 50 bicomd φ F X H Y g Y H X g Y H X
52 9 a1i Could not format ( ph -> .o. = ( <. X , Y >. ( comp ` C ) X ) ) : No typesetting found for |- ( ph -> .o. = ( <. X , Y >. ( comp ` C ) X ) ) with typecode |-
53 52 eqcomd Could not format ( ph -> ( <. X , Y >. ( comp ` C ) X ) = .o. ) : No typesetting found for |- ( ph -> ( <. X , Y >. ( comp ` C ) X ) = .o. ) with typecode |-
54 53 oveqd Could not format ( ph -> ( g ( <. X , Y >. ( comp ` C ) X ) F ) = ( g .o. F ) ) : No typesetting found for |- ( ph -> ( g ( <. X , Y >. ( comp ` C ) X ) F ) = ( g .o. F ) ) with typecode |-
55 54 eqeq1d Could not format ( ph -> ( ( g ( <. X , Y >. ( comp ` C ) X ) F ) = ( .1. ` X ) <-> ( g .o. F ) = ( .1. ` X ) ) ) : No typesetting found for |- ( ph -> ( ( g ( <. X , Y >. ( comp ` C ) X ) F ) = ( .1. ` X ) <-> ( g .o. F ) = ( .1. ` X ) ) ) with typecode |-
56 10 a1i φ ˙ = Y X comp C Y
57 56 eqcomd φ Y X comp C Y = ˙
58 57 oveqd φ F Y X comp C Y g = F ˙ g
59 58 eqeq1d φ F Y X comp C Y g = 1 ˙ Y F ˙ g = 1 ˙ Y
60 55 59 anbi12d Could not format ( 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 ) ) ) ) : No typesetting found for |- ( 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 ) ) ) ) with typecode |-
61 51 60 anbi12d Could not format ( 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 ) ) ) ) ) : No typesetting found for |- ( 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 ) ) ) ) ) with typecode |-
62 61 exbidv Could not format ( 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 ) ) ) ) ) : No typesetting found for |- ( 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 ) ) ) ) ) with typecode |-
63 df-rex Could not format ( 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 ) ) ) ) : No typesetting found for |- ( 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 ) ) ) ) with typecode |-
64 62 63 bitr4di Could not format ( 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 ) ) ) ) : No typesetting found for |- ( 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 ) ) ) ) with typecode |-
65 38 49 64 3bitrd Could not format ( 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 ) ) ) ) : No typesetting found for |- ( 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 ) ) ) ) with typecode |-
66 13 17 65 3bitrd Could not format ( ph -> ( F e. ( X I Y ) <-> E. g e. ( Y H X ) ( ( g .o. F ) = ( .1. ` X ) /\ ( F .* g ) = ( .1. ` Y ) ) ) ) : No typesetting found for |- ( ph -> ( F e. ( X I Y ) <-> E. g e. ( Y H X ) ( ( g .o. F ) = ( .1. ` X ) /\ ( F .* g ) = ( .1. ` Y ) ) ) ) with typecode |-