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

Theorem srhmsubcOLD 33047
 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.) (New usage is discouraged.)
Hypotheses
Ref Expression
srhmsubcOLD.s
srhmsubcOLD.c
srhmsubcOLD.j RingHom
Assertion
Ref Expression
srhmsubcOLD SubcatRingCatOLD
Distinct variable groups:   ,   ,,   ,,   ,,
Allowed substitution hints:   ()   (,)

Proof of Theorem srhmsubcOLD
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 srhmsubcOLD.c . . . 4
2 eleq1 2529 . . . . . . 7
3 srhmsubcOLD.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 RingCatOLD RingCatOLD
11 eqid 2457 . . . . . . 7 RingCatOLD RingCatOLD
12 simpl 457 . . . . . . 7
13 eqid 2457 . . . . . . 7 RingCatOLD RingCatOLD
143, 1srhmsubcOLDlem2 33045 . . . . . . . 8 RingCatOLD
1514adantrr 716 . . . . . . 7 RingCatOLD
163, 1srhmsubcOLDlem2 33045 . . . . . . . 8 RingCatOLD
1716adantrl 715 . . . . . . 7 RingCatOLD
1810, 11, 12, 13, 15, 17ringchomOLD 33000 . . . . . 6 RingCatOLD RingHom
199, 18syl5sseqr 3548 . . . . 5 RingHom RingCatOLD
20 srhmsubcOLD.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 RingCatOLD f RingCatOLD
3029, 11, 13, 15, 17homfval 15108 . . . . 5 f RingCatOLD RingCatOLD
3119, 28, 303sstr4d 3542 . . . 4 f RingCatOLD
3231ralrimivva 2878 . . 3 f RingCatOLD
33 ovex 6324 . . . . . 6 RingHom
3420, 33fnmpt2i 6868 . . . . 5
3534a1i 11 . . . 4
3629, 11homffn 15109 . . . . 5 f RingCatOLD RingCatOLD RingCatOLD
37 id 22 . . . . . . . . 9
3810, 11, 37ringcbasOLD 32998 . . . . . . . 8 RingCatOLD
3938eqcomd 2465 . . . . . . 7 RingCatOLD
4039sqxpeqd 5034 . . . . . 6 RingCatOLD RingCatOLD
4140fneq2d 5678 . . . . 5 f RingCatOLD f RingCatOLD RingCatOLD RingCatOLD
4236, 41mpbiri 233 . . . 4 f RingCatOLD
43 inex1g 4599 . . . 4
4435, 42, 43isssc 15236 . . 3 cat f RingCatOLD f RingCatOLD
458, 32, 44mpbir2and 922 . 2 cat f RingCatOLD
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 RingCatOLD RingCatOLD
54 simpl 457 . . . . . 6
5510, 11, 53, 54, 14, 50ringcidOLD 33006 . . . . 5 RingCatOLD
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 RingCatOLD
64 eqid 2457 . . . . . . . . 9 compRingCatOLD compRingCatOLD
6510ringccatOLD 33005 . . . . . . . . . 10 RingCatOLD
6665ad3antrrr 729 . . . . . . . . 9 RingCatOLD
6714adantr 465 . . . . . . . . . 10 RingCatOLD
6867adantr 465 . . . . . . . . 9 RingCatOLD
6916ad2ant2r 746 . . . . . . . . . 10 RingCatOLD
7069adantr 465 . . . . . . . . 9 RingCatOLD
713, 1srhmsubcOLDlem2 33045 . . . . . . . . . . 11 RingCatOLD
7271ad2ant2rl 748 . . . . . . . . . 10 RingCatOLD
7372adantr 465 . . . . . . . . 9 RingCatOLD
7454adantr 465 . . . . . . . . . . . . . . 15
75 simpl 457 . . . . . . . . . . . . . . . 16
7659, 75anim12i 566 . . . . . . . . . . . . . . 15
7774, 76jca 532 . . . . . . . . . . . . . 14
783, 1, 20srhmsubcOLDlem3 33046 . . . . . . . . . . . . . 14 RingCatOLD
7977, 78syl 16 . . . . . . . . . . . . 13 RingCatOLD
8079eleq2d 2527 . . . . . . . . . . . 12 RingCatOLD
8180biimpcd 224 . . . . . . . . . . 11 RingCatOLD
8281adantr 465 . . . . . . . . . 10 RingCatOLD
8382impcom 430 . . . . . . . . 9 RingCatOLD
843, 1, 20srhmsubcOLDlem3 33046 . . . . . . . . . . . . . 14 RingCatOLD
8584adantlr 714 . . . . . . . . . . . . 13 RingCatOLD
8685eleq2d 2527 . . . . . . . . . . . 12 RingCatOLD
8786biimpd 207 . . . . . . . . . . 11 RingCatOLD
8887adantld 467 . . . . . . . . . 10 RingCatOLD
8988imp 429 . . . . . . . . 9 RingCatOLD
9011, 13, 64, 66, 68, 70, 73, 83, 89catcocl 15102 . . . . . . . 8 compRingCatOLD RingCatOLD
9110, 11, 74, 13, 67, 72ringchomOLD 33000 . . . . . . . . . 10 RingCatOLD RingHom
9291eqcomd 2465 . . . . . . . . 9 RingHom RingCatOLD
9392adantr 465 . . . . . . . 8 RingHom RingCatOLD
9490, 93eleqtrrd 2548 . . . . . . 7 compRingCatOLD 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 compRingCatOLD
105104ralrimivva 2878 . . . . 5 compRingCatOLD
106105ralrimivva 2878 . . . 4 compRingCatOLD
10763, 106jca 532 . . 3 RingCatOLD compRingCatOLD
108107ralrimiva 2871 . 2 RingCatOLD compRingCatOLD
10929, 53, 64, 65, 35issubc2 15252 . 2 SubcatRingCatOLD cat f RingCatOLD RingCatOLD compRingCatOLD
11045, 108, 109mpbir2and 922 1 SubcatRingCatOLD
 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  RingCatOLDcringcOLD 32956 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-plusg 14725  df-hom 14736  df-cco 14737  df-0g 14859  df-cat 15085  df-cid 15086  df-homf 15087  df-ssc 15226  df-subc 15228  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-ringcOLD 32958 This theorem is referenced by:  sringcatOLD  33048  crhmsubcOLD  33049  drhmsubcOLD  33051  fldhmsubcOLD  33055
 Copyright terms: Public domain W3C validator