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

Theorem fullsubc 15463
 Description: The full subcategory generated by a subset of objects is the category with these objects and the same morphisms as the original. The result is always a subcategory (and it is full, meaning that all morphisms of the original category between objects in the subcategory is also in the subcategory), see definition 4.1(2) of [Adamek] p. 48. (Contributed by Mario Carneiro, 4-Jan-2017.)
Hypotheses
Ref Expression
fullsubc.b
fullsubc.h f
fullsubc.c
fullsubc.s
Assertion
Ref Expression
fullsubc Subcat

Proof of Theorem fullsubc
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fullsubc.h . . . . 5 f
2 fullsubc.b . . . . 5
31, 2homffn 15306 . . . 4
4 fvex 5859 . . . . 5
52, 4eqeltri 2486 . . . 4
6 sscres 15436 . . . 4 cat
73, 5, 6mp2an 670 . . 3 cat
87a1i 11 . 2 cat
9 eqid 2402 . . . . . 6
10 eqid 2402 . . . . . 6
11 fullsubc.c . . . . . . 7
1211adantr 463 . . . . . 6
13 fullsubc.s . . . . . . 7
1413sselda 3442 . . . . . 6
152, 9, 10, 12, 14catidcl 15296 . . . . 5
16 simpr 459 . . . . . . 7
1716, 16ovresd 6424 . . . . . 6
181, 2, 9, 14, 14homfval 15305 . . . . . 6
1917, 18eqtrd 2443 . . . . 5
2015, 19eleqtrrd 2493 . . . 4
21 eqid 2402 . . . . . . . . . 10 comp comp
2212ad3antrrr 728 . . . . . . . . . 10
2314ad3antrrr 728 . . . . . . . . . 10
2413adantr 463 . . . . . . . . . . . . 13
2524sselda 3442 . . . . . . . . . . . 12
2625adantr 463 . . . . . . . . . . 11
2726adantr 463 . . . . . . . . . 10
2824adantr 463 . . . . . . . . . . . 12
2928sselda 3442 . . . . . . . . . . 11
3029adantr 463 . . . . . . . . . 10
31 simprl 756 . . . . . . . . . 10
32 simprr 758 . . . . . . . . . 10
332, 9, 21, 22, 23, 27, 30, 31, 32catcocl 15299 . . . . . . . . 9 comp
3416ad3antrrr 728 . . . . . . . . . . 11
35 simplr 754 . . . . . . . . . . 11
3634, 35ovresd 6424 . . . . . . . . . 10
371, 2, 9, 23, 30homfval 15305 . . . . . . . . . 10
3836, 37eqtrd 2443 . . . . . . . . 9
3933, 38eleqtrrd 2493 . . . . . . . 8 comp
4039ralrimivva 2825 . . . . . . 7 comp
41 simplr 754 . . . . . . . . . . 11
42 simpr 459 . . . . . . . . . . 11
4341, 42ovresd 6424 . . . . . . . . . 10
4414adantr 463 . . . . . . . . . . 11
451, 2, 9, 44, 25homfval 15305 . . . . . . . . . 10
4643, 45eqtrd 2443 . . . . . . . . 9
4746adantr 463 . . . . . . . 8
48 simplr 754 . . . . . . . . . . 11
49 simpr 459 . . . . . . . . . . 11
5048, 49ovresd 6424 . . . . . . . . . 10
511, 2, 9, 26, 29homfval 15305 . . . . . . . . . 10
5250, 51eqtrd 2443 . . . . . . . . 9
5352raleqdv 3010 . . . . . . . 8 comp comp
5447, 53raleqbidv 3018 . . . . . . 7 comp comp
5540, 54mpbird 232 . . . . . 6 comp
5655ralrimiva 2818 . . . . 5 comp
5756ralrimiva 2818 . . . 4 comp
5820, 57jca 530 . . 3 comp
5958ralrimiva 2818 . 2 comp
60 xpss12 4929 . . . . 5
6113, 13, 60syl2anc 659 . . . 4
62 fnssres 5675 . . . 4
633, 61, 62sylancr 661 . . 3
641, 10, 21, 11, 63issubc2 15449 . 2 Subcat cat comp
658, 59, 64mpbir2and 923 1 Subcat
 Colors of variables: wff setvar class Syntax hints:   wi 4   wa 367   wceq 1405   wcel 1842  wral 2754  cvv 3059   wss 3414  cop 3978   class class class wbr 4395   cxp 4821   cres 4825   wfn 5564  cfv 5569  (class class class)co 6278  cbs 14841   chom 14920  compcco 14921  ccat 15278  ccid 15279   f chomf 15280   cat cssc 15420  Subcatcsubc 15422 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 4507  ax-sep 4517  ax-nul 4525  ax-pow 4572  ax-pr 4630  ax-un 6574 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 2759  df-rex 2760  df-reu 2761  df-rmo 2762  df-rab 2763  df-v 3061  df-sbc 3278  df-csb 3374  df-dif 3417  df-un 3419  df-in 3421  df-ss 3428  df-nul 3739  df-if 3886  df-pw 3957  df-sn 3973  df-pr 3975  df-op 3979  df-uni 4192  df-iun 4273  df-br 4396  df-opab 4454  df-mpt 4455  df-id 4738  df-xp 4829  df-rel 4830  df-cnv 4831  df-co 4832  df-dm 4833  df-rn 4834  df-res 4835  df-ima 4836  df-iota 5533  df-fun 5571  df-fn 5572  df-f 5573  df-f1 5574  df-fo 5575  df-f1o 5576  df-fv 5577  df-riota 6240  df-ov 6281  df-oprab 6282  df-mpt2 6283  df-1st 6784  df-2nd 6785  df-pm 7460  df-ixp 7508  df-cat 15282  df-cid 15283  df-homf 15284  df-ssc 15423  df-subc 15425 This theorem is referenced by:  resscat  15465  funcres2c  15514  ressffth  15551  funcsetcres2  15696
 Copyright terms: Public domain W3C validator