uobeq

Description: If a full functor (in fact, a full embedding) is a section of a functor (surjective on objects), then the sets of universal objects are equal. (Contributed by Zhi Wang, 17-Nov-2025)

	Ref	Expression
Hypotheses	uobffth.b	\|- B = ( Base ` D )
	uobffth.x	\|- ( ph -> X e. B )
	uobffth.f	\|- ( ph -> F e. ( C Func D ) )
	uobffth.g	\|- ( ph -> ( K o.func F ) = G )
	uobffth.y	\|- ( ph -> ( ( 1st ` K ) ` X ) = Y )
	uobeq.i	\|- I = ( idFunc ` D )
	uobeq.k	\|- ( ph -> K e. ( D Full E ) )
	uobeq.n	\|- ( ph -> ( L o.func K ) = I )
	uobeq.l	\|- ( ph -> L e. ( E Func D ) )
Assertion	uobeq	\|- ( ph -> dom ( F ( C UP D ) X ) = dom ( G ( C UP E ) Y ) )

Proof

Step	Hyp	Ref	Expression
1		uobffth.b	\|- B = ( Base ` D )
2		uobffth.x	\|- ( ph -> X e. B )
3		uobffth.f	\|- ( ph -> F e. ( C Func D ) )
4		uobffth.g	\|- ( ph -> ( K o.func F ) = G )
5		uobffth.y	\|- ( ph -> ( ( 1st ` K ) ` X ) = Y )
6		uobeq.i	\|- I = ( idFunc ` D )
7		uobeq.k	\|- ( ph -> K e. ( D Full E ) )
8		uobeq.n	\|- ( ph -> ( L o.func K ) = I )
9		uobeq.l	\|- ( ph -> L e. ( E Func D ) )
10		relfunc	\|- Rel ( D Func E )
11		fullfunc	\|- ( D Full E ) C_ ( D Func E )
12	11 7	sselid	\|- ( ph -> K e. ( D Func E ) )
13		1st2nd	\|- ( ( Rel ( D Func E ) /\ K e. ( D Func E ) ) -> K = <. ( 1st ` K ) , ( 2nd ` K ) >. )
14	10 12 13	sylancr	\|- ( ph -> K = <. ( 1st ` K ) , ( 2nd ` K ) >. )
15	12	func1st2nd	\|- ( ph -> ( 1st ` K ) ( D Func E ) ( 2nd ` K ) )
16	9	func1st2nd	\|- ( ph -> ( 1st ` L ) ( E Func D ) ( 2nd ` L ) )
17	12 9	cofu1st2nd	\|- ( ph -> ( L o.func K ) = ( <. ( 1st ` L ) , ( 2nd ` L ) >. o.func <. ( 1st ` K ) , ( 2nd ` K ) >. ) )
18	17 8	eqtr3d	\|- ( ph -> ( <. ( 1st ` L ) , ( 2nd ` L ) >. o.func <. ( 1st ` K ) , ( 2nd ` K ) >. ) = I )
19	6 15 16 18	cofidfth	\|- ( ph -> ( 1st ` K ) ( D Faith E ) ( 2nd ` K ) )
20		df-br	\|- ( ( 1st ` K ) ( D Faith E ) ( 2nd ` K ) <-> <. ( 1st ` K ) , ( 2nd ` K ) >. e. ( D Faith E ) )
21	19 20	sylib	\|- ( ph -> <. ( 1st ` K ) , ( 2nd ` K ) >. e. ( D Faith E ) )
22	14 21	eqeltrd	\|- ( ph -> K e. ( D Faith E ) )
23	7 22	elind	\|- ( ph -> K e. ( ( D Full E ) i^i ( D Faith E ) ) )
24	1 2 3 4 5 23	uobffth	\|- ( ph -> dom ( F ( C UP D ) X ) = dom ( G ( C UP E ) Y ) )

Metamath Proof Explorer

Theorem uobeq

Proof