Definition df-ringcALTV

Description: Definition of the category Ring, relativized to a subset u . This is the category of all rings in u and homomorphisms between these rings. Generally, we will take u to be a weak universe or Grothendieck universe, because these sets have closure properties as good as the real thing. (Contributed by AV, 13-Feb-2020) (New usage is discouraged.)

	Ref	Expression
Assertion	df-ringcALTV	⊢ RingCatALTV = ( 𝑢 ∈ V ↦ ⦋ ( 𝑢 ∩ Ring ) / 𝑏 ⦌ { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( Hom ‘ ndx ) , ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( 𝑥 RingHom 𝑦 ) ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( 𝑏 × 𝑏 ) , 𝑧 ∈ 𝑏 ↦ ( 𝑔 ∈ ( ( 2nd ‘ 𝑣 ) RingHom 𝑧 ) , 𝑓 ∈ ( ( 1st ‘ 𝑣 ) RingHom ( 2nd ‘ 𝑣 ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) ) ⟩ } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cringcALTV	⊢ RingCatALTV
1		vu	⊢ 𝑢
2		cvv	⊢ V
3	1	cv	⊢ 𝑢
4		crg	⊢ Ring
5	3 4	cin	⊢ ( 𝑢 ∩ Ring )
6		vb	⊢ 𝑏
7		cbs	⊢ Base
8		cnx	⊢ ndx
9	8 7	cfv	⊢ ( Base ‘ ndx )
10	6	cv	⊢ 𝑏
11	9 10	cop	⊢ ⟨ ( Base ‘ ndx ) , 𝑏 ⟩
12		chom	⊢ Hom
13	8 12	cfv	⊢ ( Hom ‘ ndx )
14		vx	⊢ 𝑥
15		vy	⊢ 𝑦
16	14	cv	⊢ 𝑥
17		crh	⊢ RingHom
18	15	cv	⊢ 𝑦
19	16 18 17	co	⊢ ( 𝑥 RingHom 𝑦 )
20	14 15 10 10 19	cmpo	⊢ ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( 𝑥 RingHom 𝑦 ) )
21	13 20	cop	⊢ ⟨ ( Hom ‘ ndx ) , ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( 𝑥 RingHom 𝑦 ) ) ⟩
22		cco	⊢ comp
23	8 22	cfv	⊢ ( comp ‘ ndx )
24		vv	⊢ 𝑣
25	10 10	cxp	⊢ ( 𝑏 × 𝑏 )
26		vz	⊢ 𝑧
27		vg	⊢ 𝑔
28		c2nd	⊢ 2nd
29	24	cv	⊢ 𝑣
30	29 28	cfv	⊢ ( 2nd ‘ 𝑣 )
31	26	cv	⊢ 𝑧
32	30 31 17	co	⊢ ( ( 2nd ‘ 𝑣 ) RingHom 𝑧 )
33		vf	⊢ 𝑓
34		c1st	⊢ 1st
35	29 34	cfv	⊢ ( 1st ‘ 𝑣 )
36	35 30 17	co	⊢ ( ( 1st ‘ 𝑣 ) RingHom ( 2nd ‘ 𝑣 ) )
37	27	cv	⊢ 𝑔
38	33	cv	⊢ 𝑓
39	37 38	ccom	⊢ ( 𝑔 ∘ 𝑓 )
40	27 33 32 36 39	cmpo	⊢ ( 𝑔 ∈ ( ( 2nd ‘ 𝑣 ) RingHom 𝑧 ) , 𝑓 ∈ ( ( 1st ‘ 𝑣 ) RingHom ( 2nd ‘ 𝑣 ) ) ↦ ( 𝑔 ∘ 𝑓 ) )
41	24 26 25 10 40	cmpo	⊢ ( 𝑣 ∈ ( 𝑏 × 𝑏 ) , 𝑧 ∈ 𝑏 ↦ ( 𝑔 ∈ ( ( 2nd ‘ 𝑣 ) RingHom 𝑧 ) , 𝑓 ∈ ( ( 1st ‘ 𝑣 ) RingHom ( 2nd ‘ 𝑣 ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) )
42	23 41	cop	⊢ ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( 𝑏 × 𝑏 ) , 𝑧 ∈ 𝑏 ↦ ( 𝑔 ∈ ( ( 2nd ‘ 𝑣 ) RingHom 𝑧 ) , 𝑓 ∈ ( ( 1st ‘ 𝑣 ) RingHom ( 2nd ‘ 𝑣 ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) ) ⟩
43	11 21 42	ctp	⊢ { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( Hom ‘ ndx ) , ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( 𝑥 RingHom 𝑦 ) ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( 𝑏 × 𝑏 ) , 𝑧 ∈ 𝑏 ↦ ( 𝑔 ∈ ( ( 2nd ‘ 𝑣 ) RingHom 𝑧 ) , 𝑓 ∈ ( ( 1st ‘ 𝑣 ) RingHom ( 2nd ‘ 𝑣 ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) ) ⟩ }
44	6 5 43	csb	⊢ ⦋ ( 𝑢 ∩ Ring ) / 𝑏 ⦌ { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( Hom ‘ ndx ) , ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( 𝑥 RingHom 𝑦 ) ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( 𝑏 × 𝑏 ) , 𝑧 ∈ 𝑏 ↦ ( 𝑔 ∈ ( ( 2nd ‘ 𝑣 ) RingHom 𝑧 ) , 𝑓 ∈ ( ( 1st ‘ 𝑣 ) RingHom ( 2nd ‘ 𝑣 ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) ) ⟩ }
45	1 2 44	cmpt	⊢ ( 𝑢 ∈ V ↦ ⦋ ( 𝑢 ∩ Ring ) / 𝑏 ⦌ { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( Hom ‘ ndx ) , ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( 𝑥 RingHom 𝑦 ) ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( 𝑏 × 𝑏 ) , 𝑧 ∈ 𝑏 ↦ ( 𝑔 ∈ ( ( 2nd ‘ 𝑣 ) RingHom 𝑧 ) , 𝑓 ∈ ( ( 1st ‘ 𝑣 ) RingHom ( 2nd ‘ 𝑣 ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) ) ⟩ } )
46	0 45	wceq	⊢ RingCatALTV = ( 𝑢 ∈ V ↦ ⦋ ( 𝑢 ∩ Ring ) / 𝑏 ⦌ { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( Hom ‘ ndx ) , ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( 𝑥 RingHom 𝑦 ) ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( 𝑏 × 𝑏 ) , 𝑧 ∈ 𝑏 ↦ ( 𝑔 ∈ ( ( 2nd ‘ 𝑣 ) RingHom 𝑧 ) , 𝑓 ∈ ( ( 1st ‘ 𝑣 ) RingHom ( 2nd ‘ 𝑣 ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) ) ⟩ } )