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 ⊢BaseC=BaseC
6 eqid ⊢Hom⁡C=Hom⁡C
7 eqid ⊢Hom⁡D=Hom⁡D
8 1 ad2antrr ⊢φ∧a∈BaseC∧b∈BaseC→Hom𝑓⁡C=Hom𝑓⁡D
9 8 ad2antrr ⊢φ∧a∈BaseC∧b∈BaseC∧f∈aHom⁡Cb∧c∈BaseC→Hom𝑓⁡C=Hom𝑓⁡D
10 simpr ⊢φ∧a∈BaseC∧b∈BaseC∧f∈aHom⁡Cb∧c∈BaseC→c∈BaseC
11 simp-4r ⊢φ∧a∈BaseC∧b∈BaseC∧f∈aHom⁡Cb∧c∈BaseC→a∈BaseC
12 5 6 7 9 10 11 homfeqval ⊢φ∧a∈BaseC∧b∈BaseC∧f∈aHom⁡Cb∧c∈BaseC→cHom⁡Ca=cHom⁡Da
13 eqid ⊢comp⁡C=comp⁡C
14 eqid ⊢comp⁡D=comp⁡D
15 1 ad5antr ⊢φ∧a∈BaseC∧b∈BaseC∧f∈aHom⁡Cb∧c∈BaseC∧g∈cHom⁡Ca→Hom𝑓⁡C=Hom𝑓⁡D
16 2 ad5antr ⊢φ∧a∈BaseC∧b∈BaseC∧f∈aHom⁡Cb∧c∈BaseC∧g∈cHom⁡Ca→comp𝑓⁡C=comp𝑓⁡D
17 simplr ⊢φ∧a∈BaseC∧b∈BaseC∧f∈aHom⁡Cb∧c∈BaseC∧g∈cHom⁡Ca→c∈BaseC
18 simp-5r ⊢φ∧a∈BaseC∧b∈BaseC∧f∈aHom⁡Cb∧c∈BaseC∧g∈cHom⁡Ca→a∈BaseC
19 simp-4r ⊢φ∧a∈BaseC∧b∈BaseC∧f∈aHom⁡Cb∧c∈BaseC∧g∈cHom⁡Ca→b∈BaseC
20 simpr ⊢φ∧a∈BaseC∧b∈BaseC∧f∈aHom⁡Cb∧c∈BaseC∧g∈cHom⁡Ca→g∈cHom⁡Ca
21 simpllr ⊢φ∧a∈BaseC∧b∈BaseC∧f∈aHom⁡Cb∧c∈BaseC∧g∈cHom⁡Ca→f∈aHom⁡Cb
22 5 6 13 14 15 16 17 18 19 20 21 comfeqval ⊢φ∧a∈BaseC∧b∈BaseC∧f∈aHom⁡Cb∧c∈BaseC∧g∈cHom⁡Ca→fcacomp⁡Cbg=fcacomp⁡Dbg
23 12 22 mpteq12dva ⊢φ∧a∈BaseC∧b∈BaseC∧f∈aHom⁡Cb∧c∈BaseC→g∈cHom⁡Ca⟼fcacomp⁡Cbg=g∈cHom⁡Da⟼fcacomp⁡Dbg
24 23 cnveqd ⊢φ∧a∈BaseC∧b∈BaseC∧f∈aHom⁡Cb∧c∈BaseC→g∈cHom⁡Ca⟼fcacomp⁡Cbg-1=g∈cHom⁡Da⟼fcacomp⁡Dbg-1
25 24 funeqd ⊢φ∧a∈BaseC∧b∈BaseC∧f∈aHom⁡Cb∧c∈BaseC→Fun⁡g∈cHom⁡Ca⟼fcacomp⁡Cbg-1↔Fun⁡g∈cHom⁡Da⟼fcacomp⁡Dbg-1
26 25 ralbidva ⊢φ∧a∈BaseC∧b∈BaseC∧f∈aHom⁡Cb→∀c∈BaseCFun⁡g∈cHom⁡Ca⟼fcacomp⁡Cbg-1↔∀c∈BaseCFun⁡g∈cHom⁡Da⟼fcacomp⁡Dbg-1
27 26 rabbidva ⊢φ∧a∈BaseC∧b∈BaseC→f∈aHom⁡Cb|∀c∈BaseCFun⁡g∈cHom⁡Ca⟼fcacomp⁡Cbg-1=f∈aHom⁡Cb|∀c∈BaseCFun⁡g∈cHom⁡Da⟼fcacomp⁡Dbg-1
28 simplr ⊢φ∧a∈BaseC∧b∈BaseC→a∈BaseC
29 simpr ⊢φ∧a∈BaseC∧b∈BaseC→b∈BaseC
30 5 6 7 8 28 29 homfeqval ⊢φ∧a∈BaseC∧b∈BaseC→aHom⁡Cb=aHom⁡Db
31 1 homfeqbas ⊢φ→BaseC=BaseD
32 31 ad2antrr ⊢φ∧a∈BaseC∧b∈BaseC→BaseC=BaseD
33 32 raleqdv ⊢φ∧a∈BaseC∧b∈BaseC→∀c∈BaseCFun⁡g∈cHom⁡Da⟼fcacomp⁡Dbg-1↔∀c∈BaseDFun⁡g∈cHom⁡Da⟼fcacomp⁡Dbg-1
34 30 33 rabeqbidv ⊢φ∧a∈BaseC∧b∈BaseC→f∈aHom⁡Cb|∀c∈BaseCFun⁡g∈cHom⁡Da⟼fcacomp⁡Dbg-1=f∈aHom⁡Db|∀c∈BaseDFun⁡g∈cHom⁡Da⟼fcacomp⁡Dbg-1
35 27 34 eqtrd ⊢φ∧a∈BaseC∧b∈BaseC→f∈aHom⁡Cb|∀c∈BaseCFun⁡g∈cHom⁡Ca⟼fcacomp⁡Cbg-1=f∈aHom⁡Db|∀c∈BaseDFun⁡g∈cHom⁡Da⟼fcacomp⁡Dbg-1
36 35 3impa ⊢φ∧a∈BaseC∧b∈BaseC→f∈aHom⁡Cb|∀c∈BaseCFun⁡g∈cHom⁡Ca⟼fcacomp⁡Cbg-1=f∈aHom⁡Db|∀c∈BaseDFun⁡g∈cHom⁡Da⟼fcacomp⁡Dbg-1
37 36 mpoeq3dva ⊢φ→a∈BaseC,b∈BaseC⟼f∈aHom⁡Cb|∀c∈BaseCFun⁡g∈cHom⁡Ca⟼fcacomp⁡Cbg-1=a∈BaseC,b∈BaseC⟼f∈aHom⁡Db|∀c∈BaseDFun⁡g∈cHom⁡Da⟼fcacomp⁡Dbg-1
38 mpoeq12 ⊢BaseC=BaseD∧BaseC=BaseD→a∈BaseC,b∈BaseC⟼f∈aHom⁡Db|∀c∈BaseDFun⁡g∈cHom⁡Da⟼fcacomp⁡Dbg-1=a∈BaseD,b∈BaseD⟼f∈aHom⁡Db|∀c∈BaseDFun⁡g∈cHom⁡Da⟼fcacomp⁡Dbg-1
39 31 31 38 syl2anc ⊢φ→a∈BaseC,b∈BaseC⟼f∈aHom⁡Db|∀c∈BaseDFun⁡g∈cHom⁡Da⟼fcacomp⁡Dbg-1=a∈BaseD,b∈BaseD⟼f∈aHom⁡Db|∀c∈BaseDFun⁡g∈cHom⁡Da⟼fcacomp⁡Dbg-1
40 37 39 eqtrd ⊢φ→a∈BaseC,b∈BaseC⟼f∈aHom⁡Cb|∀c∈BaseCFun⁡g∈cHom⁡Ca⟼fcacomp⁡Cbg-1=a∈BaseD,b∈BaseD⟼f∈aHom⁡Db|∀c∈BaseDFun⁡g∈cHom⁡Da⟼fcacomp⁡Dbg-1
41 eqid ⊢Mono⁡C=Mono⁡C
42 5 6 13 41 3 monfval ⊢φ→Mono⁡C=a∈BaseC,b∈BaseC⟼f∈aHom⁡Cb|∀c∈BaseCFun⁡g∈cHom⁡Ca⟼fcacomp⁡Cbg-1
43 eqid ⊢BaseD=BaseD
44 eqid ⊢Mono⁡D=Mono⁡D
45 43 7 14 44 4 monfval ⊢φ→Mono⁡D=a∈BaseD,b∈BaseD⟼f∈aHom⁡Db|∀c∈BaseDFun⁡g∈cHom⁡Da⟼fcacomp⁡Dbg-1
46 40 42 45 3eqtr4d ⊢φ→Mono⁡C=Mono⁡D