Metamath Proof Explorer

Theorem cofidvala

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

		Ref	Expression
	Hypotheses	cofidvala.i	⊢ 𝐼 = ( id_func ‘ 𝐷 )
		cofidvala.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
		cofidvala.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐷 Func 𝐸 ) )
		cofidvala.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐸 Func 𝐷 ) )
		cofidvala.o	⊢ ( 𝜑 → ( 𝐺 ∘_func 𝐹 ) = 𝐼 )
		cofidvala.h	⊢ 𝐻 = ( Hom ‘ 𝐷 )
	Assertion	cofidvala	⊢ ( 𝜑 → ( ( ( 1^st ‘ 𝐺 ) ∘ ( 1^st ‘ 𝐹 ) ) = ( I ↾ 𝐵 ) ∧ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ) ) = ( 𝑧 ∈ ( 𝐵 × 𝐵 ) ↦ ( I ↾ ( 𝐻 ‘ 𝑧 ) ) ) ) )

Proof

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