funcringcsetcALTV2

Description: The "natural forgetful functor" from the category of unital rings into the category of sets which sends each ring to its underlying set (base set) and the morphisms (ring homomorphisms) to mappings of the corresponding base sets. (Contributed by AV, 16-Feb-2020) (New usage is discouraged.)

	Ref	Expression
Hypotheses	funcringcsetcALTV2.r	⊢ 𝑅 = ( RingCat ‘ 𝑈 )
	funcringcsetcALTV2.s	⊢ 𝑆 = ( SetCat ‘ 𝑈 )
	funcringcsetcALTV2.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	funcringcsetcALTV2.c	⊢ 𝐶 = ( Base ‘ 𝑆 )
	funcringcsetcALTV2.u	⊢ ( 𝜑 → 𝑈 ∈ WUni )
	funcringcsetcALTV2.f	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐵 ↦ ( Base ‘ 𝑥 ) ) )
	funcringcsetcALTV2.g	⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( I ↾ ( 𝑥 RingHom 𝑦 ) ) ) )
Assertion	funcringcsetcALTV2	⊢ ( 𝜑 → 𝐹 ( 𝑅 Func 𝑆 ) 𝐺 )

Proof

Step	Hyp	Ref	Expression
1		funcringcsetcALTV2.r	⊢ 𝑅 = ( RingCat ‘ 𝑈 )
2		funcringcsetcALTV2.s	⊢ 𝑆 = ( SetCat ‘ 𝑈 )
3		funcringcsetcALTV2.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
4		funcringcsetcALTV2.c	⊢ 𝐶 = ( Base ‘ 𝑆 )
5		funcringcsetcALTV2.u	⊢ ( 𝜑 → 𝑈 ∈ WUni )
6		funcringcsetcALTV2.f	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐵 ↦ ( Base ‘ 𝑥 ) ) )
7		funcringcsetcALTV2.g	⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( I ↾ ( 𝑥 RingHom 𝑦 ) ) ) )
8		eqid	⊢ ( Hom ‘ 𝑅 ) = ( Hom ‘ 𝑅 )
9		eqid	⊢ ( Hom ‘ 𝑆 ) = ( Hom ‘ 𝑆 )
10		eqid	⊢ ( Id ‘ 𝑅 ) = ( Id ‘ 𝑅 )
11		eqid	⊢ ( Id ‘ 𝑆 ) = ( Id ‘ 𝑆 )
12		eqid	⊢ ( comp ‘ 𝑅 ) = ( comp ‘ 𝑅 )
13		eqid	⊢ ( comp ‘ 𝑆 ) = ( comp ‘ 𝑆 )
14	1	ringccat	⊢ ( 𝑈 ∈ WUni → 𝑅 ∈ Cat )
15	5 14	syl	⊢ ( 𝜑 → 𝑅 ∈ Cat )
16	2	setccat	⊢ ( 𝑈 ∈ WUni → 𝑆 ∈ Cat )
17	5 16	syl	⊢ ( 𝜑 → 𝑆 ∈ Cat )
18	1 2 3 4 5 6	funcringcsetcALTV2lem3	⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ 𝐶 )
19	1 2 3 4 5 6 7	funcringcsetcALTV2lem4	⊢ ( 𝜑 → 𝐺 Fn ( 𝐵 × 𝐵 ) )
20	1 2 3 4 5 6 7	funcringcsetcALTV2lem8	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑎 𝐺 𝑏 ) : ( 𝑎 ( Hom ‘ 𝑅 ) 𝑏 ) ⟶ ( ( 𝐹 ‘ 𝑎 ) ( Hom ‘ 𝑆 ) ( 𝐹 ‘ 𝑏 ) ) )
21	1 2 3 4 5 6 7	funcringcsetcALTV2lem7	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( ( 𝑎 𝐺 𝑎 ) ‘ ( ( Id ‘ 𝑅 ) ‘ 𝑎 ) ) = ( ( Id ‘ 𝑆 ) ‘ ( 𝐹 ‘ 𝑎 ) ) )
22	1 2 3 4 5 6 7	funcringcsetcALTV2lem9	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( ℎ ∈ ( 𝑎 ( Hom ‘ 𝑅 ) 𝑏 ) ∧ 𝑘 ∈ ( 𝑏 ( Hom ‘ 𝑅 ) 𝑐 ) ) ) → ( ( 𝑎 𝐺 𝑐 ) ‘ ( 𝑘 ( ⟨ 𝑎 , 𝑏 ⟩ ( comp ‘ 𝑅 ) 𝑐 ) ℎ ) ) = ( ( ( 𝑏 𝐺 𝑐 ) ‘ 𝑘 ) ( ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) ⟩ ( comp ‘ 𝑆 ) ( 𝐹 ‘ 𝑐 ) ) ( ( 𝑎 𝐺 𝑏 ) ‘ ℎ ) ) )
23	3 4 8 9 10 11 12 13 15 17 18 19 20 21 22	isfuncd	⊢ ( 𝜑 → 𝐹 ( 𝑅 Func 𝑆 ) 𝐺 )

Metamath Proof Explorer

Theorem funcringcsetcALTV2

Proof