Metamath Proof Explorer

Theorem monpropd

Description: If two categories have the same set of objects, morphisms, and compositions, then they have the same monomorphisms. (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Hypotheses monpropd.3 ⊢ φ → Hom 𝑓 ⁡ C = Hom 𝑓 ⁡ D
monpropd.4 ⊢ φ → comp 𝑓 ⁡ C = comp 𝑓 ⁡ D
monpropd.c ⊢ φ → C ∈ Cat
monpropd.d ⊢ φ → D ∈ Cat
Assertion monpropd ⊢ φ → Mono ⁡ C = Mono ⁡ D

Proof

Step Hyp Ref Expression
1 monpropd.3 ⊢ φ → Hom 𝑓 ⁡ C = Hom 𝑓 ⁡ D
2 monpropd.4 ⊢ φ → comp 𝑓 ⁡ C = comp 𝑓 ⁡ D
3 monpropd.c ⊢ φ → C ∈ Cat
4 monpropd.d ⊢ φ → D ∈ Cat
5 eqid ⊢ Base C = Base C
6 eqid ⊢ Hom ⁡ C = Hom ⁡ C
7 eqid ⊢ Hom ⁡ D = Hom ⁡ D
8 1 ad2antrr ⊢ φ ∧ a ∈ Base C ∧ b ∈ Base C → Hom 𝑓 ⁡ C = Hom 𝑓 ⁡ D
9 8 ad2antrr ⊢ φ ∧ a ∈ Base C ∧ b ∈ Base C ∧ f ∈ a Hom ⁡ C b ∧ c ∈ Base C → Hom 𝑓 ⁡ C = Hom 𝑓 ⁡ D
10 simpr ⊢ φ ∧ a ∈ Base C ∧ b ∈ Base C ∧ f ∈ a Hom ⁡ C b ∧ c ∈ Base C → c ∈ Base C
11 simp-4r ⊢ φ ∧ a ∈ Base C ∧ b ∈ Base C ∧ f ∈ a Hom ⁡ C b ∧ c ∈ Base C → a ∈ Base C
12 5 6 7 9 10 11 homfeqval ⊢ φ ∧ a ∈ Base C ∧ b ∈ Base C ∧ f ∈ a Hom ⁡ C b ∧ c ∈ Base C → c Hom ⁡ C a = c Hom ⁡ D a
13 eqid ⊢ comp ⁡ C = comp ⁡ C
14 eqid ⊢ comp ⁡ D = comp ⁡ D
15 1 ad5antr ⊢ φ ∧ a ∈ Base C ∧ b ∈ Base C ∧ f ∈ a Hom ⁡ C b ∧ c ∈ Base C ∧ g ∈ c Hom ⁡ C a → Hom 𝑓 ⁡ C = Hom 𝑓 ⁡ D
16 2 ad5antr ⊢ φ ∧ a ∈ Base C ∧ b ∈ Base C ∧ f ∈ a Hom ⁡ C b ∧ c ∈ Base C ∧ g ∈ c Hom ⁡ C a → comp 𝑓 ⁡ C = comp 𝑓 ⁡ D
17 simplr ⊢ φ ∧ a ∈ Base C ∧ b ∈ Base C ∧ f ∈ a Hom ⁡ C b ∧ c ∈ Base C ∧ g ∈ c Hom ⁡ C a → c ∈ Base C
18 simp-5r ⊢ φ ∧ a ∈ Base C ∧ b ∈ Base C ∧ f ∈ a Hom ⁡ C b ∧ c ∈ Base C ∧ g ∈ c Hom ⁡ C a → a ∈ Base C
19 simp-4r ⊢ φ ∧ a ∈ Base C ∧ b ∈ Base C ∧ f ∈ a Hom ⁡ C b ∧ c ∈ Base C ∧ g ∈ c Hom ⁡ C a → b ∈ Base C
20 simpr ⊢ φ ∧ a ∈ Base C ∧ b ∈ Base C ∧ f ∈ a Hom ⁡ C b ∧ c ∈ Base C ∧ g ∈ c Hom ⁡ C a → g ∈ c Hom ⁡ C a
21 simpllr ⊢ φ ∧ a ∈ Base C ∧ b ∈ Base C ∧ f ∈ a Hom ⁡ C b ∧ c ∈ Base C ∧ g ∈ c Hom ⁡ C a → f ∈ a Hom ⁡ C b
22 5 6 13 14 15 16 17 18 19 20 21 comfeqval ⊢ φ ∧ a ∈ Base C ∧ b ∈ Base C ∧ f ∈ a Hom ⁡ C b ∧ c ∈ Base C ∧ g ∈ c Hom ⁡ C a → f c a comp ⁡ C b g = f c a comp ⁡ D b g
23 12 22 mpteq12dva ⊢ φ ∧ a ∈ Base C ∧ b ∈ Base C ∧ f ∈ a Hom ⁡ C b ∧ c ∈ Base C → g ∈ c Hom ⁡ C a ⟼ f c a comp ⁡ C b g = g ∈ c Hom ⁡ D a ⟼ f c a comp ⁡ D b g
24 23 cnveqd ⊢ φ ∧ a ∈ Base C ∧ b ∈ Base C ∧ f ∈ a Hom ⁡ C b ∧ c ∈ Base C → g ∈ c Hom ⁡ C a ⟼ f c a comp ⁡ C b g -1 = g ∈ c Hom ⁡ D a ⟼ f c a comp ⁡ D b g -1
25 24 funeqd ⊢ φ ∧ a ∈ Base C ∧ b ∈ Base C ∧ f ∈ a Hom ⁡ C b ∧ c ∈ Base C → Fun ⁡ g ∈ c Hom ⁡ C a ⟼ f c a comp ⁡ C b g -1 ↔ Fun ⁡ g ∈ c Hom ⁡ D a ⟼ f c a comp ⁡ D b g -1
26 25 ralbidva ⊢ φ ∧ a ∈ Base C ∧ b ∈ Base C ∧ f ∈ a Hom ⁡ C b → ∀ c ∈ Base C Fun ⁡ g ∈ c Hom ⁡ C a ⟼ f c a comp ⁡ C b g -1 ↔ ∀ c ∈ Base C Fun ⁡ g ∈ c Hom ⁡ D a ⟼ f c a comp ⁡ D b g -1
27 26 rabbidva ⊢ φ ∧ a ∈ Base C ∧ b ∈ Base C → f ∈ a Hom ⁡ C b | ∀ c ∈ Base C Fun ⁡ g ∈ c Hom ⁡ C a ⟼ f c a comp ⁡ C b g -1 = f ∈ a Hom ⁡ C b | ∀ c ∈ Base C Fun ⁡ g ∈ c Hom ⁡ D a ⟼ f c a comp ⁡ D b g -1
28 simplr ⊢ φ ∧ a ∈ Base C ∧ b ∈ Base C → a ∈ Base C
29 simpr ⊢ φ ∧ a ∈ Base C ∧ b ∈ Base C → b ∈ Base C
30 5 6 7 8 28 29 homfeqval ⊢ φ ∧ a ∈ Base C ∧ b ∈ Base C → a Hom ⁡ C b = a Hom ⁡ D b
31 1 homfeqbas ⊢ φ → Base C = Base D
32 31 ad2antrr ⊢ φ ∧ a ∈ Base C ∧ b ∈ Base C → Base C = Base D
33 32 raleqdv ⊢ φ ∧ a ∈ Base C ∧ b ∈ Base C → ∀ c ∈ Base C Fun ⁡ g ∈ c Hom ⁡ D a ⟼ f c a comp ⁡ D b g -1 ↔ ∀ c ∈ Base D Fun ⁡ g ∈ c Hom ⁡ D a ⟼ f c a comp ⁡ D b g -1
34 30 33 rabeqbidv ⊢ φ ∧ a ∈ Base C ∧ b ∈ Base C → f ∈ a Hom ⁡ C b | ∀ c ∈ Base C Fun ⁡ g ∈ c Hom ⁡ D a ⟼ f c a comp ⁡ D b g -1 = f ∈ a Hom ⁡ D b | ∀ c ∈ Base D Fun ⁡ g ∈ c Hom ⁡ D a ⟼ f c a comp ⁡ D b g -1
35 27 34 eqtrd ⊢ φ ∧ a ∈ Base C ∧ b ∈ Base C → f ∈ a Hom ⁡ C b | ∀ c ∈ Base C Fun ⁡ g ∈ c Hom ⁡ C a ⟼ f c a comp ⁡ C b g -1 = f ∈ a Hom ⁡ D b | ∀ c ∈ Base D Fun ⁡ g ∈ c Hom ⁡ D a ⟼ f c a comp ⁡ D b g -1
36 35 3impa ⊢ φ ∧ a ∈ Base C ∧ b ∈ Base C → f ∈ a Hom ⁡ C b | ∀ c ∈ Base C Fun ⁡ g ∈ c Hom ⁡ C a ⟼ f c a comp ⁡ C b g -1 = f ∈ a Hom ⁡ D b | ∀ c ∈ Base D Fun ⁡ g ∈ c Hom ⁡ D a ⟼ f c a comp ⁡ D b g -1
37 36 mpoeq3dva ⊢ φ → a ∈ Base C , b ∈ Base C ⟼ f ∈ a Hom ⁡ C b | ∀ c ∈ Base C Fun ⁡ g ∈ c Hom ⁡ C a ⟼ f c a comp ⁡ C b g -1 = a ∈ Base C , b ∈ Base C ⟼ f ∈ a Hom ⁡ D b | ∀ c ∈ Base D Fun ⁡ g ∈ c Hom ⁡ D a ⟼ f c a comp ⁡ D b g -1
38 mpoeq12 ⊢ Base C = Base D ∧ Base C = Base D → a ∈ Base C , b ∈ Base C ⟼ f ∈ a Hom ⁡ D b | ∀ c ∈ Base D Fun ⁡ g ∈ c Hom ⁡ D a ⟼ f c a comp ⁡ D b g -1 = a ∈ Base D , b ∈ Base D ⟼ f ∈ a Hom ⁡ D b | ∀ c ∈ Base D Fun ⁡ g ∈ c Hom ⁡ D a ⟼ f c a comp ⁡ D b g -1
39 31 31 38 syl2anc ⊢ φ → a ∈ Base C , b ∈ Base C ⟼ f ∈ a Hom ⁡ D b | ∀ c ∈ Base D Fun ⁡ g ∈ c Hom ⁡ D a ⟼ f c a comp ⁡ D b g -1 = a ∈ Base D , b ∈ Base D ⟼ f ∈ a Hom ⁡ D b | ∀ c ∈ Base D Fun ⁡ g ∈ c Hom ⁡ D a ⟼ f c a comp ⁡ D b g -1
40 37 39 eqtrd ⊢ φ → a ∈ Base C , b ∈ Base C ⟼ f ∈ a Hom ⁡ C b | ∀ c ∈ Base C Fun ⁡ g ∈ c Hom ⁡ C a ⟼ f c a comp ⁡ C b g -1 = a ∈ Base D , b ∈ Base D ⟼ f ∈ a Hom ⁡ D b | ∀ c ∈ Base D Fun ⁡ g ∈ c Hom ⁡ D a ⟼ f c a comp ⁡ D b g -1
41 eqid ⊢ Mono ⁡ C = Mono ⁡ C
42 5 6 13 41 3 monfval ⊢ φ → Mono ⁡ C = a ∈ Base C , b ∈ Base C ⟼ f ∈ a Hom ⁡ C b | ∀ c ∈ Base C Fun ⁡ g ∈ c Hom ⁡ C a ⟼ f c a comp ⁡ C b g -1
43 eqid ⊢ Base D = Base D
44 eqid ⊢ Mono ⁡ D = Mono ⁡ D
45 43 7 14 44 4 monfval ⊢ φ → Mono ⁡ D = a ∈ Base D , b ∈ Base D ⟼ f ∈ a Hom ⁡ D b | ∀ c ∈ Base D Fun ⁡ g ∈ c Hom ⁡ D a ⟼ f c a comp ⁡ D b g -1
46 40 42 45 3eqtr4d ⊢ φ → Mono ⁡ C = Mono ⁡ D