funcestrcsetc

Description: The "natural forgetful functor" from the category of extensible structures into the category of sets which sends each extensible structure to its base set, preserving the morphisms as mappings between the corresponding base sets. (Contributed by AV, 23-Mar-2020)

	Ref	Expression
Hypotheses	funcestrcsetc.e	⊢ 𝐸 = ( ExtStrCat ‘ 𝑈 )
	funcestrcsetc.s	⊢ 𝑆 = ( SetCat ‘ 𝑈 )
	funcestrcsetc.b	⊢ 𝐵 = ( Base ‘ 𝐸 )
	funcestrcsetc.c	⊢ 𝐶 = ( Base ‘ 𝑆 )
	funcestrcsetc.u	⊢ ( 𝜑 → 𝑈 ∈ WUni )
	funcestrcsetc.f	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐵 ↦ ( Base ‘ 𝑥 ) ) )
	funcestrcsetc.g	⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( I ↾ ( ( Base ‘ 𝑦 ) ↑_m ( Base ‘ 𝑥 ) ) ) ) )
Assertion	funcestrcsetc	⊢ ( 𝜑 → 𝐹 ( 𝐸 Func 𝑆 ) 𝐺 )

Proof

Step	Hyp	Ref	Expression
1		funcestrcsetc.e	⊢ 𝐸 = ( ExtStrCat ‘ 𝑈 )
2		funcestrcsetc.s	⊢ 𝑆 = ( SetCat ‘ 𝑈 )
3		funcestrcsetc.b	⊢ 𝐵 = ( Base ‘ 𝐸 )
4		funcestrcsetc.c	⊢ 𝐶 = ( Base ‘ 𝑆 )
5		funcestrcsetc.u	⊢ ( 𝜑 → 𝑈 ∈ WUni )
6		funcestrcsetc.f	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐵 ↦ ( Base ‘ 𝑥 ) ) )
7		funcestrcsetc.g	⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( I ↾ ( ( Base ‘ 𝑦 ) ↑_m ( Base ‘ 𝑥 ) ) ) ) )
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	estrccat	⊢ ( 𝑈 ∈ WUni → 𝐸 ∈ Cat )
15	5 14	syl	⊢ ( 𝜑 → 𝐸 ∈ Cat )
16	2	setccat	⊢ ( 𝑈 ∈ WUni → 𝑆 ∈ Cat )
17	5 16	syl	⊢ ( 𝜑 → 𝑆 ∈ Cat )
18	1 2 3 4 5 6	funcestrcsetclem3	⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ 𝐶 )
19	1 2 3 4 5 6 7	funcestrcsetclem4	⊢ ( 𝜑 → 𝐺 Fn ( 𝐵 × 𝐵 ) )
20	1 2 3 4 5 6 7	funcestrcsetclem8	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑎 𝐺 𝑏 ) : ( 𝑎 ( Hom ‘ 𝐸 ) 𝑏 ) ⟶ ( ( 𝐹 ‘ 𝑎 ) ( Hom ‘ 𝑆 ) ( 𝐹 ‘ 𝑏 ) ) )
21	1 2 3 4 5 6 7	funcestrcsetclem7	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( ( 𝑎 𝐺 𝑎 ) ‘ ( ( Id ‘ 𝐸 ) ‘ 𝑎 ) ) = ( ( Id ‘ 𝑆 ) ‘ ( 𝐹 ‘ 𝑎 ) ) )
22	1 2 3 4 5 6 7	funcestrcsetclem9	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( ℎ ∈ ( 𝑎 ( 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 funcestrcsetc

Proof