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

Theorem ringcvalALTV 41311
 Description: Value of the category of rings (in a universe). (Contributed by AV, 13-Feb-2020.) (New usage is discouraged.)
Hypotheses
Ref Expression
ringcvalALTV.c 𝐶 = (RingCatALTV‘𝑈)
ringcvalALTV.u (𝜑𝑈𝑉)
ringcvalALTV.b (𝜑𝐵 = (𝑈 ∩ Ring))
ringcvalALTV.h (𝜑𝐻 = (𝑥𝐵, 𝑦𝐵 ↦ (𝑥 RingHom 𝑦)))
ringcvalALTV.o (𝜑· = (𝑣 ∈ (𝐵 × 𝐵), 𝑧𝐵 ↦ (𝑔 ∈ ((2nd𝑣) RingHom 𝑧), 𝑓 ∈ ((1st𝑣) RingHom (2nd𝑣)) ↦ (𝑔𝑓))))
Assertion
Ref Expression
ringcvalALTV (𝜑𝐶 = {⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), · ⟩})
Distinct variable groups:   𝑓,𝑔,𝑣,𝑥,𝑦,𝑧   𝑣,𝐵,𝑥,𝑦,𝑧   𝑣,𝑈,𝑥,𝑦,𝑧   𝜑,𝑣,𝑥,𝑦,𝑧
Allowed substitution hints:   𝜑(𝑓,𝑔)   𝐵(𝑓,𝑔)   𝐶(𝑥,𝑦,𝑧,𝑣,𝑓,𝑔)   · (𝑥,𝑦,𝑧,𝑣,𝑓,𝑔)   𝑈(𝑓,𝑔)   𝐻(𝑥,𝑦,𝑧,𝑣,𝑓,𝑔)   𝑉(𝑥,𝑦,𝑧,𝑣,𝑓,𝑔)

Proof of Theorem ringcvalALTV
Dummy variables 𝑏 𝑢 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ringcvalALTV.c . 2 𝐶 = (RingCatALTV‘𝑈)
2 df-ringcALTV 41310 . . . 4 RingCatALTV = (𝑢 ∈ V ↦ (𝑢 ∩ Ring) / 𝑏{⟨(Base‘ndx), 𝑏⟩, ⟨(Hom ‘ndx), (𝑥𝑏, 𝑦𝑏 ↦ (𝑥 RingHom 𝑦))⟩, ⟨(comp‘ndx), (𝑣 ∈ (𝑏 × 𝑏), 𝑧𝑏 ↦ (𝑔 ∈ ((2nd𝑣) RingHom 𝑧), 𝑓 ∈ ((1st𝑣) RingHom (2nd𝑣)) ↦ (𝑔𝑓)))⟩})
32a1i 11 . . 3 (𝜑 → RingCatALTV = (𝑢 ∈ V ↦ (𝑢 ∩ Ring) / 𝑏{⟨(Base‘ndx), 𝑏⟩, ⟨(Hom ‘ndx), (𝑥𝑏, 𝑦𝑏 ↦ (𝑥 RingHom 𝑦))⟩, ⟨(comp‘ndx), (𝑣 ∈ (𝑏 × 𝑏), 𝑧𝑏 ↦ (𝑔 ∈ ((2nd𝑣) RingHom 𝑧), 𝑓 ∈ ((1st𝑣) RingHom (2nd𝑣)) ↦ (𝑔𝑓)))⟩}))
4 vex 3189 . . . . . 6 𝑢 ∈ V
54inex1 4761 . . . . 5 (𝑢 ∩ Ring) ∈ V
65a1i 11 . . . 4 ((𝜑𝑢 = 𝑈) → (𝑢 ∩ Ring) ∈ V)
7 ineq1 3787 . . . . . 6 (𝑢 = 𝑈 → (𝑢 ∩ Ring) = (𝑈 ∩ Ring))
87adantl 482 . . . . 5 ((𝜑𝑢 = 𝑈) → (𝑢 ∩ Ring) = (𝑈 ∩ Ring))
9 ringcvalALTV.b . . . . . 6 (𝜑𝐵 = (𝑈 ∩ Ring))
109adantr 481 . . . . 5 ((𝜑𝑢 = 𝑈) → 𝐵 = (𝑈 ∩ Ring))
118, 10eqtr4d 2658 . . . 4 ((𝜑𝑢 = 𝑈) → (𝑢 ∩ Ring) = 𝐵)
12 simpr 477 . . . . . 6 (((𝜑𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → 𝑏 = 𝐵)
1312opeq2d 4379 . . . . 5 (((𝜑𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → ⟨(Base‘ndx), 𝑏⟩ = ⟨(Base‘ndx), 𝐵⟩)
14 eqidd 2622 . . . . . . . 8 (((𝜑𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → (𝑥 RingHom 𝑦) = (𝑥 RingHom 𝑦))
1512, 12, 14mpt2eq123dv 6673 . . . . . . 7 (((𝜑𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → (𝑥𝑏, 𝑦𝑏 ↦ (𝑥 RingHom 𝑦)) = (𝑥𝐵, 𝑦𝐵 ↦ (𝑥 RingHom 𝑦)))
16 ringcvalALTV.h . . . . . . . 8 (𝜑𝐻 = (𝑥𝐵, 𝑦𝐵 ↦ (𝑥 RingHom 𝑦)))
1716ad2antrr 761 . . . . . . 7 (((𝜑𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → 𝐻 = (𝑥𝐵, 𝑦𝐵 ↦ (𝑥 RingHom 𝑦)))
1815, 17eqtr4d 2658 . . . . . 6 (((𝜑𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → (𝑥𝑏, 𝑦𝑏 ↦ (𝑥 RingHom 𝑦)) = 𝐻)
1918opeq2d 4379 . . . . 5 (((𝜑𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → ⟨(Hom ‘ndx), (𝑥𝑏, 𝑦𝑏 ↦ (𝑥 RingHom 𝑦))⟩ = ⟨(Hom ‘ndx), 𝐻⟩)
2012sqxpeqd 5103 . . . . . . . 8 (((𝜑𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → (𝑏 × 𝑏) = (𝐵 × 𝐵))
21 eqidd 2622 . . . . . . . 8 (((𝜑𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → (𝑔 ∈ ((2nd𝑣) RingHom 𝑧), 𝑓 ∈ ((1st𝑣) RingHom (2nd𝑣)) ↦ (𝑔𝑓)) = (𝑔 ∈ ((2nd𝑣) RingHom 𝑧), 𝑓 ∈ ((1st𝑣) RingHom (2nd𝑣)) ↦ (𝑔𝑓)))
2220, 12, 21mpt2eq123dv 6673 . . . . . . 7 (((𝜑𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → (𝑣 ∈ (𝑏 × 𝑏), 𝑧𝑏 ↦ (𝑔 ∈ ((2nd𝑣) RingHom 𝑧), 𝑓 ∈ ((1st𝑣) RingHom (2nd𝑣)) ↦ (𝑔𝑓))) = (𝑣 ∈ (𝐵 × 𝐵), 𝑧𝐵 ↦ (𝑔 ∈ ((2nd𝑣) RingHom 𝑧), 𝑓 ∈ ((1st𝑣) RingHom (2nd𝑣)) ↦ (𝑔𝑓))))
23 ringcvalALTV.o . . . . . . . 8 (𝜑· = (𝑣 ∈ (𝐵 × 𝐵), 𝑧𝐵 ↦ (𝑔 ∈ ((2nd𝑣) RingHom 𝑧), 𝑓 ∈ ((1st𝑣) RingHom (2nd𝑣)) ↦ (𝑔𝑓))))
2423ad2antrr 761 . . . . . . 7 (((𝜑𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → · = (𝑣 ∈ (𝐵 × 𝐵), 𝑧𝐵 ↦ (𝑔 ∈ ((2nd𝑣) RingHom 𝑧), 𝑓 ∈ ((1st𝑣) RingHom (2nd𝑣)) ↦ (𝑔𝑓))))
2522, 24eqtr4d 2658 . . . . . 6 (((𝜑𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → (𝑣 ∈ (𝑏 × 𝑏), 𝑧𝑏 ↦ (𝑔 ∈ ((2nd𝑣) RingHom 𝑧), 𝑓 ∈ ((1st𝑣) RingHom (2nd𝑣)) ↦ (𝑔𝑓))) = · )
2625opeq2d 4379 . . . . 5 (((𝜑𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → ⟨(comp‘ndx), (𝑣 ∈ (𝑏 × 𝑏), 𝑧𝑏 ↦ (𝑔 ∈ ((2nd𝑣) RingHom 𝑧), 𝑓 ∈ ((1st𝑣) RingHom (2nd𝑣)) ↦ (𝑔𝑓)))⟩ = ⟨(comp‘ndx), · ⟩)
2713, 19, 26tpeq123d 4255 . . . 4 (((𝜑𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → {⟨(Base‘ndx), 𝑏⟩, ⟨(Hom ‘ndx), (𝑥𝑏, 𝑦𝑏 ↦ (𝑥 RingHom 𝑦))⟩, ⟨(comp‘ndx), (𝑣 ∈ (𝑏 × 𝑏), 𝑧𝑏 ↦ (𝑔 ∈ ((2nd𝑣) RingHom 𝑧), 𝑓 ∈ ((1st𝑣) RingHom (2nd𝑣)) ↦ (𝑔𝑓)))⟩} = {⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), · ⟩})
286, 11, 27csbied2 3543 . . 3 ((𝜑𝑢 = 𝑈) → (𝑢 ∩ Ring) / 𝑏{⟨(Base‘ndx), 𝑏⟩, ⟨(Hom ‘ndx), (𝑥𝑏, 𝑦𝑏 ↦ (𝑥 RingHom 𝑦))⟩, ⟨(comp‘ndx), (𝑣 ∈ (𝑏 × 𝑏), 𝑧𝑏 ↦ (𝑔 ∈ ((2nd𝑣) RingHom 𝑧), 𝑓 ∈ ((1st𝑣) RingHom (2nd𝑣)) ↦ (𝑔𝑓)))⟩} = {⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), · ⟩})
29 ringcvalALTV.u . . . 4 (𝜑𝑈𝑉)
30 elex 3198 . . . 4 (𝑈𝑉𝑈 ∈ V)
3129, 30syl 17 . . 3 (𝜑𝑈 ∈ V)
32 tpex 6913 . . . 4 {⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), · ⟩} ∈ V
3332a1i 11 . . 3 (𝜑 → {⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), · ⟩} ∈ V)
343, 28, 31, 33fvmptd 6247 . 2 (𝜑 → (RingCatALTV‘𝑈) = {⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), · ⟩})
351, 34syl5eq 2667 1 (𝜑𝐶 = {⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), · ⟩})
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 384   = wceq 1480   ∈ wcel 1987  Vcvv 3186  ⦋csb 3515   ∩ cin 3555  {ctp 4154  ⟨cop 4156   ↦ cmpt 4675   × cxp 5074   ∘ ccom 5080  ‘cfv 5849  (class class class)co 6607   ↦ cmpt2 6609  1st c1st 7114  2nd c2nd 7115  ndxcnx 15781  Basecbs 15784  Hom chom 15876  compcco 15877  Ringcrg 18471   RingHom crh 18636  RingCatALTVcringcALTV 41308 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4743  ax-nul 4751  ax-pr 4869  ax-un 6905 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3188  df-sbc 3419  df-csb 3516  df-dif 3559  df-un 3561  df-in 3563  df-ss 3570  df-nul 3894  df-if 4061  df-sn 4151  df-pr 4153  df-tp 4155  df-op 4157  df-uni 4405  df-br 4616  df-opab 4676  df-mpt 4677  df-id 4991  df-xp 5082  df-rel 5083  df-cnv 5084  df-co 5085  df-dm 5086  df-iota 5812  df-fun 5851  df-fv 5857  df-oprab 6611  df-mpt2 6612  df-ringcALTV 41310 This theorem is referenced by:  ringcbasALTV  41350  ringchomfvalALTV  41351  ringccofvalALTV  41354
 Copyright terms: Public domain W3C validator