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

Theorem cofull 15827
 Description: The composition of two full functors is full. Proposition 3.30(d) in [Adamek] p. 35. (Contributed by Mario Carneiro, 28-Jan-2017.)
Hypotheses
Ref Expression
cofull.f Full
cofull.g Full
Assertion
Ref Expression
cofull func Full

Proof of Theorem cofull
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 relfunc 15755 . . 3
2 fullfunc 15799 . . . . 5 Full
3 cofull.f . . . . 5 Full
42, 3sseldi 3462 . . . 4
5 fullfunc 15799 . . . . 5 Full
6 cofull.g . . . . 5 Full
75, 6sseldi 3462 . . . 4
84, 7cofucl 15781 . . 3 func
9 1st2nd 6850 . . 3 func func func func
101, 8, 9sylancr 667 . 2 func func func
11 1st2ndbr 6853 . . . . 5 func func func
121, 8, 11sylancr 667 . . . 4 func func
13 eqid 2422 . . . . . . . 8
14 eqid 2422 . . . . . . . 8
15 eqid 2422 . . . . . . . 8
16 relfull 15801 . . . . . . . . 9 Full
176adantr 466 . . . . . . . . 9 Full
18 1st2ndbr 6853 . . . . . . . . 9 Full Full Full
1916, 17, 18sylancr 667 . . . . . . . 8 Full
20 eqid 2422 . . . . . . . . . 10
21 relfunc 15755 . . . . . . . . . . 11
224adantr 466 . . . . . . . . . . 11
23 1st2ndbr 6853 . . . . . . . . . . 11
2421, 22, 23sylancr 667 . . . . . . . . . 10
2520, 13, 24funcf1 15759 . . . . . . . . 9
26 simprl 762 . . . . . . . . 9
2725, 26ffvelrnd 6035 . . . . . . . 8
28 simprr 764 . . . . . . . . 9
2925, 28ffvelrnd 6035 . . . . . . . 8
3013, 14, 15, 19, 27, 29fullfo 15805 . . . . . . 7
31 eqid 2422 . . . . . . . 8
32 relfull 15801 . . . . . . . . 9 Full
333adantr 466 . . . . . . . . 9 Full
34 1st2ndbr 6853 . . . . . . . . 9 Full Full Full
3532, 33, 34sylancr 667 . . . . . . . 8 Full
3620, 15, 31, 35, 26, 28fullfo 15805 . . . . . . 7
37 foco 5817 . . . . . . 7
3830, 36, 37syl2anc 665 . . . . . 6
397adantr 466 . . . . . . . 8
4020, 22, 39, 26, 28cofu2nd 15778 . . . . . . 7 func
41 eqidd 2423 . . . . . . 7
4220, 22, 39, 26cofu1 15777 . . . . . . . 8 func
4320, 22, 39, 28cofu1 15777 . . . . . . . 8 func
4442, 43oveq12d 6320 . . . . . . 7 func func
4540, 41, 44foeq123d 5824 . . . . . 6 func func func
4638, 45mpbird 235 . . . . 5 func func func
4746ralrimivva 2846 . . . 4 func func func
4820, 14, 31isfull2 15804 . . . 4 func Full func func func func func func
4912, 47, 48sylanbrc 668 . . 3 func Full func
50 df-br 4421 . . 3 func Full func func func Full
5149, 50sylib 199 . 2 func func Full
5210, 51eqeltrd 2510 1 func Full
 Colors of variables: wff setvar class Syntax hints:   wi 4   wa 370   wceq 1437   wcel 1868  wral 2775  cop 4002   class class class wbr 4420   ccom 4854   wrel 4855  wfo 5596  cfv 5598  (class class class)co 6302  c1st 6802  c2nd 6803  cbs 15109   chom 15189   cfunc 15747   func ccofu 15749   Full cful 15795 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-rep 4533  ax-sep 4543  ax-nul 4552  ax-pow 4599  ax-pr 4657  ax-un 6594 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-reu 2782  df-rmo 2783  df-rab 2784  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-op 4003  df-uni 4217  df-iun 4298  df-br 4421  df-opab 4480  df-mpt 4481  df-id 4765  df-xp 4856  df-rel 4857  df-cnv 4858  df-co 4859  df-dm 4860  df-rn 4861  df-res 4862  df-ima 4863  df-iota 5562  df-fun 5600  df-fn 5601  df-f 5602  df-f1 5603  df-fo 5604  df-f1o 5605  df-fv 5606  df-riota 6264  df-ov 6305  df-oprab 6306  df-mpt2 6307  df-1st 6804  df-2nd 6805  df-map 7479  df-ixp 7528  df-cat 15562  df-cid 15563  df-func 15751  df-cofu 15753  df-full 15797 This theorem is referenced by:  coffth  15829
 Copyright terms: Public domain W3C validator