Mathbox for Alexander van der Vekens < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  srhmsubc Structured version   Unicode version

Theorem srhmsubc 33028
 Description: According to df-subc 15228, the subcategories Subcat of a category are subsets of the homomorphisms of ( see subcssc 15256 and subcss2 15259). Therefore, the set of special ring homomorphisms (i.e. ring homomorphisms from a special ring to another ring of that kind) is a "subcategory" of the category of (unital) rings. (Contributed by AV, 19-Feb-2020.)
Hypotheses
Ref Expression
srhmsubc.s
srhmsubc.c
srhmsubc.j RingHom
Assertion
Ref Expression
srhmsubc SubcatRingCat
Distinct variable groups:   ,   ,,   ,,   ,,
Allowed substitution hints:   ()   (,)

Proof of Theorem srhmsubc
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 srhmsubc.c . . . 4
2 eleq1 2529 . . . . . . 7
3 srhmsubc.s . . . . . . 7
42, 3vtoclri 3184 . . . . . 6
54ssriv 3503 . . . . 5
6 sslin 3720 . . . . 5
75, 6mp1i 12 . . . 4
81, 7syl5eqss 3543 . . 3
9 ssid 3518 . . . . . 6 RingHom RingHom
10 eqid 2457 . . . . . . 7 RingCat RingCat
11 eqid 2457 . . . . . . 7 RingCat RingCat
12 simpl 457 . . . . . . 7
13 eqid 2457 . . . . . . 7 RingCat RingCat
143, 1srhmsubclem2 33026 . . . . . . . 8 RingCat
1514adantrr 716 . . . . . . 7 RingCat
163, 1srhmsubclem2 33026 . . . . . . . 8 RingCat
1716adantrl 715 . . . . . . 7 RingCat
1810, 11, 12, 13, 15, 17ringchom 32965 . . . . . 6 RingCat RingHom
199, 18syl5sseqr 3548 . . . . 5 RingHom RingCat
20 srhmsubc.j . . . . . . 7 RingHom
2120a1i 11 . . . . . 6 RingHom
22 oveq12 6305 . . . . . . 7 RingHom RingHom
2322adantl 466 . . . . . 6 RingHom RingHom
24 simprl 756 . . . . . 6
25 simprr 757 . . . . . 6
26 ovex 6324 . . . . . . 7 RingHom
2726a1i 11 . . . . . 6 RingHom
2821, 23, 24, 25, 27ovmpt2d 6429 . . . . 5 RingHom
29 eqid 2457 . . . . . 6 f RingCat f RingCat
3029, 11, 13, 15, 17homfval 15108 . . . . 5 f RingCat RingCat
3119, 28, 303sstr4d 3542 . . . 4 f RingCat
3231ralrimivva 2878 . . 3 f RingCat
33 ovex 6324 . . . . . 6 RingHom
3420, 33fnmpt2i 6868 . . . . 5
3534a1i 11 . . . 4
3629, 11homffn 15109 . . . . 5 f RingCat RingCat RingCat
37 id 22 . . . . . . . . 9
3810, 11, 37ringcbas 32963 . . . . . . . 8 RingCat
3938eqcomd 2465 . . . . . . 7 RingCat
4039sqxpeqd 5034 . . . . . 6 RingCat RingCat
4140fneq2d 5678 . . . . 5 f RingCat f RingCat RingCat RingCat
4236, 41mpbiri 233 . . . 4 f RingCat
43 inex1g 4599 . . . 4
4435, 42, 43isssc 15236 . . 3 cat f RingCat f RingCat
458, 32, 44mpbir2and 922 . 2 cat f RingCat
461elin2 3685 . . . . . . . 8
474adantl 466 . . . . . . . 8
4846, 47sylbi 195 . . . . . . 7
4948adantl 466 . . . . . 6
50 eqid 2457 . . . . . . 7
5150idrhm 17507 . . . . . 6 RingHom
5249, 51syl 16 . . . . 5 RingHom
53 eqid 2457 . . . . . 6 RingCat RingCat
54 simpl 457 . . . . . 6
5510, 11, 53, 54, 14, 50ringcid 32977 . . . . 5 RingCat
5620a1i 11 . . . . . 6 RingHom
57 oveq12 6305 . . . . . . 7 RingHom RingHom
5857adantl 466 . . . . . 6 RingHom RingHom
59 simpr 461 . . . . . 6
60 ovex 6324 . . . . . . 7 RingHom
6160a1i 11 . . . . . 6 RingHom
6256, 58, 59, 59, 61ovmpt2d 6429 . . . . 5 RingHom
6352, 55, 623eltr4d 2560 . . . 4 RingCat
64 eqid 2457 . . . . . . . . 9 compRingCat compRingCat
6510ringccat 32976 . . . . . . . . . 10 RingCat
6665ad3antrrr 729 . . . . . . . . 9 RingCat
6714adantr 465 . . . . . . . . . 10 RingCat
6867adantr 465 . . . . . . . . 9 RingCat
6916ad2ant2r 746 . . . . . . . . . 10 RingCat
7069adantr 465 . . . . . . . . 9 RingCat
713, 1srhmsubclem2 33026 . . . . . . . . . . 11 RingCat
7271ad2ant2rl 748 . . . . . . . . . 10 RingCat
7372adantr 465 . . . . . . . . 9 RingCat
7454adantr 465 . . . . . . . . . . . . . . 15
75 simpl 457 . . . . . . . . . . . . . . . 16
7659, 75anim12i 566 . . . . . . . . . . . . . . 15
7774, 76jca 532 . . . . . . . . . . . . . 14
783, 1, 20srhmsubclem3 33027 . . . . . . . . . . . . . 14 RingCat
7977, 78syl 16 . . . . . . . . . . . . 13 RingCat
8079eleq2d 2527 . . . . . . . . . . . 12 RingCat
8180biimpcd 224 . . . . . . . . . . 11 RingCat
8281adantr 465 . . . . . . . . . 10 RingCat
8382impcom 430 . . . . . . . . 9 RingCat
843, 1, 20srhmsubclem3 33027 . . . . . . . . . . . . . 14 RingCat
8584adantlr 714 . . . . . . . . . . . . 13 RingCat
8685eleq2d 2527 . . . . . . . . . . . 12 RingCat
8786biimpd 207 . . . . . . . . . . 11 RingCat
8887adantld 467 . . . . . . . . . 10 RingCat
8988imp 429 . . . . . . . . 9 RingCat
9011, 13, 64, 66, 68, 70, 73, 83, 89catcocl 15102 . . . . . . . 8 compRingCat RingCat
9110, 11, 74, 13, 67, 72ringchom 32965 . . . . . . . . . 10 RingCat RingHom
9291eqcomd 2465 . . . . . . . . 9 RingHom RingCat
9392adantr 465 . . . . . . . 8 RingHom RingCat
9490, 93eleqtrrd 2548 . . . . . . 7 compRingCat RingHom
9520a1i 11 . . . . . . . . 9 RingHom
96 oveq12 6305 . . . . . . . . . 10 RingHom RingHom
9796adantl 466 . . . . . . . . 9 RingHom RingHom
9859adantr 465 . . . . . . . . 9
99 simprr 757 . . . . . . . . 9
100 ovex 6324 . . . . . . . . . 10 RingHom
101100a1i 11 . . . . . . . . 9 RingHom
10295, 97, 98, 99, 101ovmpt2d 6429 . . . . . . . 8 RingHom
103102adantr 465 . . . . . . 7 RingHom
10494, 103eleqtrrd 2548 . . . . . 6 compRingCat
105104ralrimivva 2878 . . . . 5 compRingCat
106105ralrimivva 2878 . . . 4 compRingCat
10763, 106jca 532 . . 3 RingCat compRingCat
108107ralrimiva 2871 . 2 RingCat compRingCat
10929, 53, 64, 65, 35issubc2 15252 . 2 SubcatRingCat cat f RingCat RingCat compRingCat
11045, 108, 109mpbir2and 922 1 SubcatRingCat
 Colors of variables: wff setvar class Syntax hints:   wi 4   wa 369   wceq 1395   wcel 1819  wral 2807  cvv 3109   cin 3470   wss 3471  cop 4038   class class class wbr 4456   cid 4799   cxp 5006   cres 5010   wfn 5589  cfv 5594  (class class class)co 6296   cmpt2 6298  cbs 14644   chom 14723  compcco 14724  ccat 15081  ccid 15082   f chomf 15083   cat cssc 15223  Subcatcsubc 15225  crg 17325   RingHom crh 17488  RingCatcringc 32955 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-8 1821  ax-9 1823  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-rep 4568  ax-sep 4578  ax-nul 4586  ax-pow 4634  ax-pr 4695  ax-un 6591  ax-cnex 9565  ax-resscn 9566  ax-1cn 9567  ax-icn 9568  ax-addcl 9569  ax-addrcl 9570  ax-mulcl 9571  ax-mulrcl 9572  ax-mulcom 9573  ax-addass 9574  ax-mulass 9575  ax-distr 9576  ax-i2m1 9577  ax-1ne0 9578  ax-1rid 9579  ax-rnegex 9580  ax-rrecex 9581  ax-cnre 9582  ax-pre-lttri 9583  ax-pre-lttrn 9584  ax-pre-ltadd 9585  ax-pre-mulgt0 9586 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-fal 1401  df-ex 1614  df-nf 1618  df-sb 1741  df-eu 2287  df-mo 2288  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-nel 2655  df-ral 2812  df-rex 2813  df-reu 2814  df-rmo 2815  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3431  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-pss 3487  df-nul 3794  df-if 3945  df-pw 4017  df-sn 4033  df-pr 4035  df-tp 4037  df-op 4039  df-uni 4252  df-int 4289  df-iun 4334  df-br 4457  df-opab 4516  df-mpt 4517  df-tr 4551  df-eprel 4800  df-id 4804  df-po 4809  df-so 4810  df-fr 4847  df-we 4849  df-ord 4890  df-on 4891  df-lim 4892  df-suc 4893  df-xp 5014  df-rel 5015  df-cnv 5016  df-co 5017  df-dm 5018  df-rn 5019  df-res 5020  df-ima 5021  df-iota 5557  df-fun 5596  df-fn 5597  df-f 5598  df-f1 5599  df-fo 5600  df-f1o 5601  df-fv 5602  df-riota 6258  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-om 6700  df-1st 6799  df-2nd 6800  df-recs 7060  df-rdg 7094  df-1o 7148  df-oadd 7152  df-er 7329  df-map 7440  df-pm 7441  df-ixp 7489  df-en 7536  df-dom 7537  df-sdom 7538  df-fin 7539  df-pnf 9647  df-mnf 9648  df-xr 9649  df-ltxr 9650  df-le 9651  df-sub 9826  df-neg 9827  df-nn 10557  df-2 10615  df-3 10616  df-4 10617  df-5 10618  df-6 10619  df-7 10620  df-8 10621  df-9 10622  df-10 10623  df-n0 10817  df-z 10886  df-dec 11001  df-uz 11107  df-fz 11698  df-struct 14646  df-ndx 14647  df-slot 14648  df-base 14649  df-sets 14650  df-ress 14651  df-plusg 14725  df-hom 14736  df-cco 14737  df-0g 14859  df-cat 15085  df-cid 15086  df-homf 15087  df-ssc 15226  df-resc 15227  df-subc 15228  df-estrc 15519  df-mgm 15999  df-sgrp 16038  df-mnd 16048  df-mhm 16093  df-grp 16184  df-ghm 16392  df-mgp 17269  df-ur 17281  df-ring 17327  df-rnghom 17491  df-ringc 32957 This theorem is referenced by:  sringcat  33029  crhmsubc  33030  drhmsubc  33032  fldhmsubc  33036
 Copyright terms: Public domain W3C validator