Metamath Proof Explorer


Theorem cidpropd

Description: Two structures with the same base, hom-sets and composition operation have the same identity function. (Contributed by Mario Carneiro, 17-Jan-2017)

Ref Expression
Hypotheses catpropd.1 φ Hom 𝑓 C = Hom 𝑓 D
catpropd.2 φ comp 𝑓 C = comp 𝑓 D
catpropd.3 φ C V
catpropd.4 φ D W
Assertion cidpropd φ Id C = Id D

Proof

Step Hyp Ref Expression
1 catpropd.1 φ Hom 𝑓 C = Hom 𝑓 D
2 catpropd.2 φ comp 𝑓 C = comp 𝑓 D
3 catpropd.3 φ C V
4 catpropd.4 φ D W
5 1 homfeqbas φ Base C = Base D
6 5 adantr φ C Cat Base C = Base D
7 eqid Base C = Base C
8 eqid Hom C = Hom C
9 eqid Hom D = Hom D
10 1 ad4antr φ C Cat x Base C g x Hom C x y Base C Hom 𝑓 C = Hom 𝑓 D
11 simpr φ C Cat x Base C g x Hom C x y Base C y Base C
12 simpllr φ C Cat x Base C g x Hom C x y Base C x Base C
13 7 8 9 10 11 12 homfeqval φ C Cat x Base C g x Hom C x y Base C y Hom C x = y Hom D x
14 eqid comp C = comp C
15 eqid comp D = comp D
16 1 ad5antr φ C Cat x Base C g x Hom C x y Base C f y Hom C x Hom 𝑓 C = Hom 𝑓 D
17 2 ad5antr φ C Cat x Base C g x Hom C x y Base C f y Hom C x comp 𝑓 C = comp 𝑓 D
18 simplr φ C Cat x Base C g x Hom C x y Base C f y Hom C x y Base C
19 simp-4r φ C Cat x Base C g x Hom C x y Base C f y Hom C x x Base C
20 simpr φ C Cat x Base C g x Hom C x y Base C f y Hom C x f y Hom C x
21 simpllr φ C Cat x Base C g x Hom C x y Base C f y Hom C x g x Hom C x
22 7 8 14 15 16 17 18 19 19 20 21 comfeqval φ C Cat x Base C g x Hom C x y Base C f y Hom C x g y x comp C x f = g y x comp D x f
23 22 eqeq1d φ C Cat x Base C g x Hom C x y Base C f y Hom C x g y x comp C x f = f g y x comp D x f = f
24 13 23 raleqbidva φ C Cat x Base C g x Hom C x y Base C f y Hom C x g y x comp C x f = f f y Hom D x g y x comp D x f = f
25 7 8 9 10 12 11 homfeqval φ C Cat x Base C g x Hom C x y Base C x Hom C y = x Hom D y
26 10 adantr φ C Cat x Base C g x Hom C x y Base C f x Hom C y Hom 𝑓 C = Hom 𝑓 D
27 2 ad5antr φ C Cat x Base C g x Hom C x y Base C f x Hom C y comp 𝑓 C = comp 𝑓 D
28 12 adantr φ C Cat x Base C g x Hom C x y Base C f x Hom C y x Base C
29 simplr φ C Cat x Base C g x Hom C x y Base C f x Hom C y y Base C
30 simpllr φ C Cat x Base C g x Hom C x y Base C f x Hom C y g x Hom C x
31 simpr φ C Cat x Base C g x Hom C x y Base C f x Hom C y f x Hom C y
32 7 8 14 15 26 27 28 28 29 30 31 comfeqval φ C Cat x Base C g x Hom C x y Base C f x Hom C y f x x comp C y g = f x x comp D y g
33 32 eqeq1d φ C Cat x Base C g x Hom C x y Base C f x Hom C y f x x comp C y g = f f x x comp D y g = f
34 25 33 raleqbidva φ C Cat x Base C g x Hom C x y Base C f x Hom C y f x x comp C y g = f f x Hom D y f x x comp D y g = f
35 24 34 anbi12d φ C Cat x Base C g x Hom C x y Base C f y Hom C x g y x comp C x f = f f x Hom C y f x x comp C y g = f f y Hom D x g y x comp D x f = f f x Hom D y f x x comp D y g = f
36 35 ralbidva φ C Cat x Base C g x Hom C x y Base C f y Hom C x g y x comp C x f = f f x Hom C y f x x comp C y g = f y Base C f y Hom D x g y x comp D x f = f f x Hom D y f x x comp D y g = f
37 36 riotabidva φ C Cat x Base C ι g x Hom C x | y Base C f y Hom C x g y x comp C x f = f f x Hom C y f x x comp C y g = f = ι g x Hom C x | y Base C f y Hom D x g y x comp D x f = f f x Hom D y f x x comp D y g = f
38 1 ad2antrr φ C Cat x Base C Hom 𝑓 C = Hom 𝑓 D
39 simpr φ C Cat x Base C x Base C
40 7 8 9 38 39 39 homfeqval φ C Cat x Base C x Hom C x = x Hom D x
41 5 ad2antrr φ C Cat x Base C Base C = Base D
42 41 raleqdv φ C Cat x Base C y Base C f y Hom D x g y x comp D x f = f f x Hom D y f x x comp D y g = f y Base D f y Hom D x g y x comp D x f = f f x Hom D y f x x comp D y g = f
43 40 42 riotaeqbidv φ C Cat x Base C ι g x Hom C x | y Base C f y Hom D x g y x comp D x f = f f x Hom D y f x x comp D y g = f = ι g x Hom D x | y Base D f y Hom D x g y x comp D x f = f f x Hom D y f x x comp D y g = f
44 37 43 eqtrd φ C Cat x Base C ι g x Hom C x | y Base C f y Hom C x g y x comp C x f = f f x Hom C y f x x comp C y g = f = ι g x Hom D x | y Base D f y Hom D x g y x comp D x f = f f x Hom D y f x x comp D y g = f
45 6 44 mpteq12dva φ C Cat x Base C ι g x Hom C x | y Base C f y Hom C x g y x comp C x f = f f x Hom C y f x x comp C y g = f = x Base D ι g x Hom D x | y Base D f y Hom D x g y x comp D x f = f f x Hom D y f x x comp D y g = f
46 simpr φ C Cat C Cat
47 eqid Id C = Id C
48 7 8 14 46 47 cidfval φ C Cat Id C = x Base C ι g x Hom C x | y Base C f y Hom C x g y x comp C x f = f f x Hom C y f x x comp C y g = f
49 eqid Base D = Base D
50 1 2 3 4 catpropd φ C Cat D Cat
51 50 biimpa φ C Cat D Cat
52 eqid Id D = Id D
53 49 9 15 51 52 cidfval φ C Cat Id D = x Base D ι g x Hom D x | y Base D f y Hom D x g y x comp D x f = f f x Hom D y f x x comp D y g = f
54 45 48 53 3eqtr4d φ C Cat Id C = Id D
55 simpr φ ¬ C Cat ¬ C Cat
56 cidffn Id Fn Cat
57 56 fndmi dom Id = Cat
58 57 eleq2i C dom Id C Cat
59 55 58 sylnibr φ ¬ C Cat ¬ C dom Id
60 ndmfv ¬ C dom Id Id C =
61 59 60 syl φ ¬ C Cat Id C =
62 57 eleq2i D dom Id D Cat
63 50 62 bitr4di φ C Cat D dom Id
64 63 notbid φ ¬ C Cat ¬ D dom Id
65 64 biimpa φ ¬ C Cat ¬ D dom Id
66 ndmfv ¬ D dom Id Id D =
67 65 66 syl φ ¬ C Cat Id D =
68 61 67 eqtr4d φ ¬ C Cat Id C = Id D
69 54 68 pm2.61dan φ Id C = Id D