Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  hofpropd Structured version   Unicode version

Theorem hofpropd 15393
 Description: If two categories have the same set of objects, morphisms, and compositions, then they have the same Hom functor. (Contributed by Mario Carneiro, 26-Jan-2017.)
Hypotheses
Ref Expression
hofpropd.1 f f
hofpropd.2 compf compf
hofpropd.c
hofpropd.d
Assertion
Ref Expression
hofpropd HomF HomF

Proof of Theorem hofpropd
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 hofpropd.1 . . 3 f f
21homfeqbas 14951 . . . . 5
32, 2xpeq12d 5024 . . . 4
43adantr 465 . . . 4
5 eqid 2467 . . . . . 6
6 eqid 2467 . . . . . 6
7 eqid 2467 . . . . . 6
81adantr 465 . . . . . 6 f f
9 xp1st 6814 . . . . . . 7
109ad2antll 728 . . . . . 6
11 xp1st 6814 . . . . . . 7
1211ad2antrl 727 . . . . . 6
135, 6, 7, 8, 10, 12homfeqval 14952 . . . . 5
14 xp2nd 6815 . . . . . . . 8
1514ad2antrl 727 . . . . . . 7
16 xp2nd 6815 . . . . . . . 8
1716ad2antll 728 . . . . . . 7
185, 6, 7, 8, 15, 17homfeqval 14952 . . . . . 6
1918adantr 465 . . . . 5
205, 6, 7, 8, 12, 15homfeqval 14952 . . . . . . . . 9
21 df-ov 6286 . . . . . . . . 9
22 df-ov 6286 . . . . . . . . 9
2320, 21, 223eqtr3g 2531 . . . . . . . 8
24 1st2nd2 6821 . . . . . . . . . 10
2524ad2antrl 727 . . . . . . . . 9
2625fveq2d 5869 . . . . . . . 8
2725fveq2d 5869 . . . . . . . 8
2823, 26, 273eqtr4d 2518 . . . . . . 7
2928adantr 465 . . . . . 6
30 eqid 2467 . . . . . . . 8 comp comp
31 eqid 2467 . . . . . . . 8 comp comp
328ad2antrr 725 . . . . . . . 8 f f
33 hofpropd.2 . . . . . . . . 9 compf compf
3433ad3antrrr 729 . . . . . . . 8 compf compf
3510ad2antrr 725 . . . . . . . 8
3612ad2antrr 725 . . . . . . . 8
3717ad2antrr 725 . . . . . . . 8
38 simplrl 759 . . . . . . . 8
3925ad2antrr 725 . . . . . . . . . . 11
4039oveq1d 6298 . . . . . . . . . 10 comp comp
4140oveqd 6300 . . . . . . . . 9 comp comp
42 hofpropd.c . . . . . . . . . . 11
4342ad3antrrr 729 . . . . . . . . . 10
4415ad2antrr 725 . . . . . . . . . 10
4526adantr 465 . . . . . . . . . . . . 13
4645, 21syl6eqr 2526 . . . . . . . . . . . 12
4746eleq2d 2537 . . . . . . . . . . 11
4847biimpa 484 . . . . . . . . . 10
49 simplrr 760 . . . . . . . . . 10
505, 6, 30, 43, 36, 44, 37, 48, 49catcocl 14939 . . . . . . . . 9 comp
5141, 50eqeltrd 2555 . . . . . . . 8 comp
525, 6, 30, 31, 32, 34, 35, 36, 37, 38, 51comfeqval 14963 . . . . . . 7 comp comp comp comp
535, 6, 30, 31, 32, 34, 36, 44, 37, 48, 49comfeqval 14963 . . . . . . . . 9 comp comp
5439oveq1d 6298 . . . . . . . . . 10 comp comp
5554oveqd 6300 . . . . . . . . 9 comp comp
5653, 41, 553eqtr4d 2518 . . . . . . . 8 comp comp
5756oveq1d 6298 . . . . . . 7 comp comp comp comp
5852, 57eqtrd 2508 . . . . . 6 comp comp comp comp
5929, 58mpteq12dva 4524 . . . . 5 comp comp comp comp
6013, 19, 59mpt2eq123dva 6341 . . . 4 comp comp comp comp
613, 4, 60mpt2eq123dva 6341 . . 3 comp comp comp comp
621, 61opeq12d 4221 . 2 f comp comp f comp comp
63 eqid 2467 . . 3 HomF HomF
6463, 42, 5, 6, 30hofval 15378 . 2 HomF f comp comp
65 eqid 2467 . . 3 HomF HomF
66 hofpropd.d . . 3
67 eqid 2467 . . 3
6865, 66, 67, 7, 31hofval 15378 . 2 HomF f comp comp
6962, 64, 683eqtr4d 2518 1 HomF HomF
 Colors of variables: wff setvar class Syntax hints:   wi 4   wa 369   wceq 1379   wcel 1767  cop 4033   cmpt 4505   cxp 4997  cfv 5587  (class class class)co 6283   cmpt2 6285  c1st 6782  c2nd 6783  cbs 14489   chom 14565  compcco 14566  ccat 14918   f chomf 14920  compfccomf 14921  HomFchof 15374 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4558  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6575 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-reu 2821  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-iun 4327  df-br 4448  df-opab 4506  df-mpt 4507  df-id 4795  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5550  df-fun 5589  df-fn 5590  df-f 5591  df-f1 5592  df-fo 5593  df-f1o 5594  df-fv 5595  df-ov 6286  df-oprab 6287  df-mpt2 6288  df-1st 6784  df-2nd 6785  df-cat 14922  df-homf 14924  df-comf 14925  df-hof 15376 This theorem is referenced by:  yonpropd  15394  oppcyon  15395
 Copyright terms: Public domain W3C validator