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	|- I = ( idFunc ` D )
	cofidvala.b	|- B = ( Base ` D )
	cofidvala.f	|- ( ph -> F e. ( D Func E ) )
	cofidvala.g	|- ( ph -> G e. ( E Func D ) )
	cofidvala.o	|- ( ph -> ( G o.func F ) = I )
	cofidvala.h	|- H = ( Hom ` D )
Assertion	cofidvala	|- ( ph -> ( ( ( 1st ` G ) o. ( 1st ` F ) ) = ( _I |` B ) /\ ( x e. B , y e. B |-> ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` y ) ) o. ( x ( 2nd ` F ) y ) ) ) = ( z e. ( B X. B ) |-> ( _I |` ( H ` z ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		cofidvala.i	|- I = ( idFunc ` D )
2		cofidvala.b	|- B = ( Base ` D )
3		cofidvala.f	|- ( ph -> F e. ( D Func E ) )
4		cofidvala.g	|- ( ph -> G e. ( E Func D ) )
5		cofidvala.o	|- ( ph -> ( G o.func F ) = I )
6		cofidvala.h	|- H = ( Hom ` D )
7	2 3 4	cofuval	|- ( ph -> ( G o.func F ) = <. ( ( 1st ` G ) o. ( 1st ` F ) ) , ( x e. B , y e. B |-> ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` y ) ) o. ( x ( 2nd ` F ) y ) ) ) >. )
8	3	func1st2nd	|- ( ph -> ( 1st ` F ) ( D Func E ) ( 2nd ` F ) )
9	8	funcrcl2	|- ( ph -> D e. Cat )
10	1 2 9 6	idfuval	|- ( ph -> I = <. ( _I |` B ) , ( z e. ( B X. B ) |-> ( _I |` ( H ` z ) ) ) >. )
11	5 7 10	3eqtr3d	|- ( ph -> <. ( ( 1st ` G ) o. ( 1st ` F ) ) , ( x e. B , y e. B |-> ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` y ) ) o. ( x ( 2nd ` F ) y ) ) ) >. = <. ( _I |` B ) , ( z e. ( B X. B ) |-> ( _I |` ( H ` z ) ) ) >. )
12	2	fvexi	|- B e. _V
13		resiexg	|- ( B e. _V -> ( _I |` B ) e. _V )
14	12 13	ax-mp	|- ( _I |` B ) e. _V
15	12 12	xpex	|- ( B X. B ) e. _V
16	15	mptex	|- ( z e. ( B X. B ) |-> ( _I |` ( H ` z ) ) ) e. _V
17	14 16	opth2	|- ( <. ( ( 1st ` G ) o. ( 1st ` F ) ) , ( x e. B , y e. B |-> ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` y ) ) o. ( x ( 2nd ` F ) y ) ) ) >. = <. ( _I |` B ) , ( z e. ( B X. B ) |-> ( _I |` ( H ` z ) ) ) >. <-> ( ( ( 1st ` G ) o. ( 1st ` F ) ) = ( _I |` B ) /\ ( x e. B , y e. B |-> ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` y ) ) o. ( x ( 2nd ` F ) y ) ) ) = ( z e. ( B X. B ) |-> ( _I |` ( H ` z ) ) ) ) )
18	11 17	sylib	|- ( ph -> ( ( ( 1st ` G ) o. ( 1st ` F ) ) = ( _I |` B ) /\ ( x e. B , y e. B |-> ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` y ) ) o. ( x ( 2nd ` F ) y ) ) ) = ( z e. ( B X. B ) |-> ( _I |` ( H ` z ) ) ) ) )