Theorem cofidval

Description: The property " <. F , G >. is a section of <. K , L >. " in a category of small categories (in a universe); expressed explicitly. (Contributed by Zhi Wang, 15-Nov-2025)

	Ref	Expression
Hypotheses	cofidval.i	⊢ 𝐼 = ( idfunc ‘ 𝐷 )
	cofidval.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
	cofidval.f	⊢ ( 𝜑 → 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 )
	cofidval.k	⊢ ( 𝜑 → 𝐾 ( 𝐸 Func 𝐷 ) 𝐿 )
	cofidval.o	⊢ ( 𝜑 → ( ⟨ 𝐾 , 𝐿 ⟩ ∘func ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐼 )
	cofidval.h	⊢ 𝐻 = ( Hom ‘ 𝐷 )
Assertion	cofidval	⊢ ( 𝜑 → ( ( 𝐾 ∘ 𝐹 ) = ( I ↾ 𝐵 ) ∧ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝐹 ‘ 𝑦 ) ) ∘ ( 𝑥 𝐺 𝑦 ) ) ) = ( 𝑧 ∈ ( 𝐵 × 𝐵 ) ↦ ( I ↾ ( 𝐻 ‘ 𝑧 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		cofidval.i	⊢ 𝐼 = ( idfunc ‘ 𝐷 )
2		cofidval.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
3		cofidval.f	⊢ ( 𝜑 → 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 )
4		cofidval.k	⊢ ( 𝜑 → 𝐾 ( 𝐸 Func 𝐷 ) 𝐿 )
5		cofidval.o	⊢ ( 𝜑 → ( ⟨ 𝐾 , 𝐿 ⟩ ∘func ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐼 )
6		cofidval.h	⊢ 𝐻 = ( Hom ‘ 𝐷 )
7	2 3 4	cofuval2	⊢ ( 𝜑 → ( ⟨ 𝐾 , 𝐿 ⟩ ∘func ⟨ 𝐹 , 𝐺 ⟩ ) = ⟨ ( 𝐾 ∘ 𝐹 ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝐹 ‘ 𝑦 ) ) ∘ ( 𝑥 𝐺 𝑦 ) ) ) ⟩ )
8	3	funcrcl2	⊢ ( 𝜑 → 𝐷 ∈ Cat )
9	1 2 8 6	idfuval	⊢ ( 𝜑 → 𝐼 = ⟨ ( I ↾ 𝐵 ) , ( 𝑧 ∈ ( 𝐵 × 𝐵 ) ↦ ( I ↾ ( 𝐻 ‘ 𝑧 ) ) ) ⟩ )
10	5 7 9	3eqtr3d	⊢ ( 𝜑 → ⟨ ( 𝐾 ∘ 𝐹 ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝐹 ‘ 𝑦 ) ) ∘ ( 𝑥 𝐺 𝑦 ) ) ) ⟩ = ⟨ ( I ↾ 𝐵 ) , ( 𝑧 ∈ ( 𝐵 × 𝐵 ) ↦ ( I ↾ ( 𝐻 ‘ 𝑧 ) ) ) ⟩ )
11	2	fvexi	⊢ 𝐵 ∈ V
12		resiexg	⊢ ( 𝐵 ∈ V → ( I ↾ 𝐵 ) ∈ V )
13	11 12	ax-mp	⊢ ( I ↾ 𝐵 ) ∈ V
14	11 11	xpex	⊢ ( 𝐵 × 𝐵 ) ∈ V
15	14	mptex	⊢ ( 𝑧 ∈ ( 𝐵 × 𝐵 ) ↦ ( I ↾ ( 𝐻 ‘ 𝑧 ) ) ) ∈ V
16	13 15	opth2	⊢ ( ⟨ ( 𝐾 ∘ 𝐹 ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝐹 ‘ 𝑦 ) ) ∘ ( 𝑥 𝐺 𝑦 ) ) ) ⟩ = ⟨ ( I ↾ 𝐵 ) , ( 𝑧 ∈ ( 𝐵 × 𝐵 ) ↦ ( I ↾ ( 𝐻 ‘ 𝑧 ) ) ) ⟩ ↔ ( ( 𝐾 ∘ 𝐹 ) = ( I ↾ 𝐵 ) ∧ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝐹 ‘ 𝑦 ) ) ∘ ( 𝑥 𝐺 𝑦 ) ) ) = ( 𝑧 ∈ ( 𝐵 × 𝐵 ) ↦ ( I ↾ ( 𝐻 ‘ 𝑧 ) ) ) ) )
17	10 16	sylib	⊢ ( 𝜑 → ( ( 𝐾 ∘ 𝐹 ) = ( I ↾ 𝐵 ) ∧ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝐹 ‘ 𝑦 ) ) ∘ ( 𝑥 𝐺 𝑦 ) ) ) = ( 𝑧 ∈ ( 𝐵 × 𝐵 ) ↦ ( I ↾ ( 𝐻 ‘ 𝑧 ) ) ) ) )