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

Theorem natpropd 15587
 Description: If two categories have the same set of objects, morphisms, and compositions, then they have the same natural transformations. (Contributed by Mario Carneiro, 26-Jan-2017.)
Hypotheses
Ref Expression
fucpropd.1 f f
fucpropd.2 compf compf
fucpropd.3 f f
fucpropd.4 compf compf
fucpropd.a
fucpropd.b
fucpropd.c
fucpropd.d
Assertion
Ref Expression
natpropd Nat Nat

Proof of Theorem natpropd
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fucpropd.1 . . . 4 f f
2 fucpropd.2 . . . 4 compf compf
3 fucpropd.3 . . . 4 f f
4 fucpropd.4 . . . 4 compf compf
5 fucpropd.a . . . 4
6 fucpropd.b . . . 4
7 fucpropd.c . . . 4
8 fucpropd.d . . . 4
91, 2, 3, 4, 5, 6, 7, 8funcpropd 15511 . . 3
11 nfv 1728 . . . 4
12 nfcsb1v 3388 . . . . 5 comp comp
1312a1i 11 . . . 4 comp comp
14 fvex 5858 . . . . 5
1514a1i 11 . . . 4
16 nfv 1728 . . . . . 6
17 nfcsb1v 3388 . . . . . . 7 comp comp
1817a1i 11 . . . . . 6 comp comp
19 fvex 5858 . . . . . . 7
2019a1i 11 . . . . . 6
21 eqid 2402 . . . . . . . . . . 11
22 eqid 2402 . . . . . . . . . . 11
23 eqid 2402 . . . . . . . . . . 11
243ad4antr 730 . . . . . . . . . . 11 f f
25 eqid 2402 . . . . . . . . . . . . 13
26 simplr 754 . . . . . . . . . . . . . 14
27 relfunc 15473 . . . . . . . . . . . . . . 15
28 simpllr 761 . . . . . . . . . . . . . . . 16
2928simpld 457 . . . . . . . . . . . . . . 15
30 1st2ndbr 6832 . . . . . . . . . . . . . . 15
3127, 29, 30sylancr 661 . . . . . . . . . . . . . 14
3226, 31eqbrtrd 4414 . . . . . . . . . . . . 13
3325, 21, 32funcf1 15477 . . . . . . . . . . . 12
3433ffvelrnda 6008 . . . . . . . . . . 11
35 simpr 459 . . . . . . . . . . . . . 14
3628simprd 461 . . . . . . . . . . . . . . 15
37 1st2ndbr 6832 . . . . . . . . . . . . . . 15
3827, 36, 37sylancr 661 . . . . . . . . . . . . . 14
3935, 38eqbrtrd 4414 . . . . . . . . . . . . 13
4025, 21, 39funcf1 15477 . . . . . . . . . . . 12
4140ffvelrnda 6008 . . . . . . . . . . 11
4221, 22, 23, 24, 34, 41homfeqval 15308 . . . . . . . . . 10
4342ixpeq2dva 7521 . . . . . . . . 9
441homfeqbas 15307 . . . . . . . . . . 11
4544ad3antrrr 728 . . . . . . . . . 10
4645ixpeq1d 7518 . . . . . . . . 9
4743, 46eqtrd 2443 . . . . . . . 8
48 fveq2 5848 . . . . . . . . . . . 12
49 fveq2 5848 . . . . . . . . . . . 12
5048, 49oveq12d 6295 . . . . . . . . . . 11
5150cbvixpv 7524 . . . . . . . . . 10
5251eleq2i 2480 . . . . . . . . 9
5345adantr 463 . . . . . . . . . 10
5453adantr 463 . . . . . . . . . . 11
55 eqid 2402 . . . . . . . . . . . . 13
56 eqid 2402 . . . . . . . . . . . . 13
571ad6antr 734 . . . . . . . . . . . . 13 f f
58 simplr 754 . . . . . . . . . . . . 13
59 simpr 459 . . . . . . . . . . . . 13
6025, 55, 56, 57, 58, 59homfeqval 15308 . . . . . . . . . . . 12
61 eqid 2402 . . . . . . . . . . . . . 14 comp comp
62 eqid 2402 . . . . . . . . . . . . . 14 comp comp
633ad7antr 736 . . . . . . . . . . . . . 14 f f
644ad7antr 736 . . . . . . . . . . . . . 14 compf compf
6534adantlr 713 . . . . . . . . . . . . . . 15
6665ad2antrr 724 . . . . . . . . . . . . . 14
6733ad2antrr 724 . . . . . . . . . . . . . . . 16
6867ffvelrnda 6008 . . . . . . . . . . . . . . 15
6968adantr 463 . . . . . . . . . . . . . 14
7040ad2antrr 724 . . . . . . . . . . . . . . . 16
7170ffvelrnda 6008 . . . . . . . . . . . . . . 15
7271adantr 463 . . . . . . . . . . . . . 14
7332ad3antrrr 728 . . . . . . . . . . . . . . . 16
7425, 55, 22, 73, 58, 59funcf2 15479 . . . . . . . . . . . . . . 15
7574ffvelrnda 6008 . . . . . . . . . . . . . 14
76 simplr 754 . . . . . . . . . . . . . . . 16
77 fveq2 5848 . . . . . . . . . . . . . . . . . 18
78 fveq2 5848 . . . . . . . . . . . . . . . . . 18
7977, 78oveq12d 6295 . . . . . . . . . . . . . . . . 17
8079fvixp 7511 . . . . . . . . . . . . . . . 16
8176, 80sylan 469 . . . . . . . . . . . . . . 15
8281adantr 463 . . . . . . . . . . . . . 14
8321, 22, 61, 62, 63, 64, 66, 69, 72, 75, 82comfeqval 15319 . . . . . . . . . . . . 13 comp comp
8441adantlr 713 . . . . . . . . . . . . . . 15
8584ad2antrr 724 . . . . . . . . . . . . . 14
86 fveq2 5848 . . . . . . . . . . . . . . . . . 18
87 fveq2 5848 . . . . . . . . . . . . . . . . . 18
8886, 87oveq12d 6295 . . . . . . . . . . . . . . . . 17
8988fvixp 7511 . . . . . . . . . . . . . . . 16
9089adantll 712 . . . . . . . . . . . . . . 15
9190ad2antrr 724 . . . . . . . . . . . . . 14
9239ad3antrrr 728 . . . . . . . . . . . . . . . 16
9325, 55, 22, 92, 58, 59funcf2 15479 . . . . . . . . . . . . . . 15
9493ffvelrnda 6008 . . . . . . . . . . . . . 14
9521, 22, 61, 62, 63, 64, 66, 85, 72, 91, 94comfeqval 15319 . . . . . . . . . . . . 13 comp comp
9683, 95eqeq12d 2424 . . . . . . . . . . . 12 comp comp comp comp
9760, 96raleqbidva 3019 . . . . . . . . . . 11 comp comp comp comp
9854, 97raleqbidva 3019 . . . . . . . . . 10 comp comp comp comp
9953, 98raleqbidva 3019 . . . . . . . . 9 comp comp comp comp
10052, 99sylan2b 473 . . . . . . . 8 comp comp comp comp
10147, 100rabeqbidva 3054 . . . . . . 7 comp comp comp comp
102 csbeq1a 3381 . . . . . . . 8 comp comp comp comp
103102adantl 464 . . . . . . 7 comp comp comp comp
104101, 103eqtrd 2443 . . . . . 6 comp comp comp comp
10516, 18, 20, 104csbiedf 3393 . . . . 5 comp comp comp comp
106 csbeq1a 3381 . . . . . 6 comp comp comp comp
107106adantl 464 . . . . 5 comp comp comp comp
108105, 107eqtrd 2443 . . . 4 comp comp comp comp
10911, 13, 15, 108csbiedf 3393 . . 3 comp comp comp comp
1109, 10, 109mpt2eq123dva 6338 . 2 comp comp comp comp
111 eqid 2402 . . 3 Nat Nat
112111, 25, 55, 22, 61natfval 15557 . 2 Nat comp comp
113 eqid 2402 . . 3 Nat Nat
114 eqid 2402 . . 3
115113, 114, 56, 23, 62natfval 15557 . 2 Nat comp comp
116110, 112, 1153eqtr4g 2468 1 Nat Nat
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 184   wa 367   wceq 1405   wcel 1842  wnfc 2550  wral 2753  crab 2757  cvv 3058  csb 3372  cop 3977   class class class wbr 4394   wrel 4827  wf 5564  cfv 5568  (class class class)co 6277   cmpt2 6279  c1st 6781  c2nd 6782  cixp 7506  cbs 14839   chom 14918  compcco 14919  ccat 15276   f chomf 15278  compfccomf 15279   cfunc 15465   Nat cnat 15552 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-8 1844  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-rep 4506  ax-sep 4516  ax-nul 4524  ax-pow 4571  ax-pr 4629  ax-un 6573 This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-fal 1411  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-ral 2758  df-rex 2759  df-reu 2760  df-rab 2762  df-v 3060  df-sbc 3277  df-csb 3373  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-nul 3738  df-if 3885  df-pw 3956  df-sn 3972  df-pr 3974  df-op 3978  df-uni 4191  df-iun 4272  df-br 4395  df-opab 4453  df-mpt 4454  df-id 4737  df-xp 4828  df-rel 4829  df-cnv 4830  df-co 4831  df-dm 4832  df-rn 4833  df-res 4834  df-ima 4835  df-iota 5532  df-fun 5570  df-fn 5571  df-f 5572  df-f1 5573  df-fo 5574  df-f1o 5575  df-fv 5576  df-riota 6239  df-ov 6280  df-oprab 6281  df-mpt2 6282  df-1st 6783  df-2nd 6784  df-map 7458  df-ixp 7507  df-cat 15280  df-cid 15281  df-homf 15282  df-comf 15283  df-func 15469  df-nat 15554 This theorem is referenced by:  fucpropd  15588
 Copyright terms: Public domain W3C validator