Theorem 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={\mathrm{Base}}_D$$
	uobffth.x	$$⊢\phi \to X\in B$$
	uobffth.f	$$⊢\phi \to F\in \left(C\mathrm{Func}D\right)$$
	uobffth.g	$$⊢\phi \to K{\circ }_{\mathrm{func}}F=G$$
	uobffth.y	$$⊢\phi \to 1^{st}\left(K\right)\left(X\right)=Y$$
	uobeq.i	$$⊢I={id}_{\mathrm{func}}\left(D\right)$$
	uobeq.k	$$⊢\phi \to K\in \left(D\mathrm{Full}E\right)$$
	uobeq.n	$$⊢\phi \to L{\circ }_{\mathrm{func}}K=I$$
	uobeq.l	$$⊢\phi \to L\in \left(E\mathrm{Func}D\right)$$
Assertion	uobeq	Could not format assertion : No typesetting found for |- ( ph -> dom ( F ( C UP D ) X ) = dom ( G ( C UP E ) Y ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		uobffth.b	$$⊢B={\mathrm{Base}}_D$$
2		uobffth.x	$$⊢\phi \to X\in B$$
3		uobffth.f	$$⊢\phi \to F\in \left(C\mathrm{Func}D\right)$$
4		uobffth.g	$$⊢\phi \to K{\circ }_{\mathrm{func}}F=G$$
5		uobffth.y	$$⊢\phi \to 1^{st}\left(K\right)\left(X\right)=Y$$
6		uobeq.i	$$⊢I={id}_{\mathrm{func}}\left(D\right)$$
7		uobeq.k	$$⊢\phi \to K\in \left(D\mathrm{Full}E\right)$$
8		uobeq.n	$$⊢\phi \to L{\circ }_{\mathrm{func}}K=I$$
9		uobeq.l	$$⊢\phi \to L\in \left(E\mathrm{Func}D\right)$$
10		relfunc	$$⊢\mathrm{Rel}\left(D\mathrm{Func}E\right)$$
11		fullfunc	$$⊢D\mathrm{Full}E\subseteq D\mathrm{Func}E$$
12	11 7	sselid	$$⊢\phi \to K\in \left(D\mathrm{Func}E\right)$$
13		1st2nd	$$⊢\left(\mathrm{Rel}\left(D\mathrm{Func}E\right)\wedge K\in \left(D\mathrm{Func}E\right)\right)\to K=⟨1^{st}\left(K\right),2^{nd}\left(K\right)⟩$$
14	10 12 13	sylancr	$$⊢\phi \to K=⟨1^{st}\left(K\right),2^{nd}\left(K\right)⟩$$
15	12	func1st2nd	$$⊢\phi \to 1^{st}\left(K\right)\left(D\mathrm{Func}E\right)2^{nd}\left(K\right)$$
16	9	func1st2nd	$$⊢\phi \to 1^{st}\left(L\right)\left(E\mathrm{Func}D\right)2^{nd}\left(L\right)$$
17	12 9	cofu1st2nd	$$⊢\phi \to L{\circ }_{\mathrm{func}}K=⟨1^{st}\left(L\right),2^{nd}\left(L\right)⟩{\circ }_{\mathrm{func}}⟨1^{st}\left(K\right),2^{nd}\left(K\right)⟩$$
18	17 8	eqtr3d	$$⊢\phi \to ⟨1^{st}\left(L\right),2^{nd}\left(L\right)⟩{\circ }_{\mathrm{func}}⟨1^{st}\left(K\right),2^{nd}\left(K\right)⟩=I$$
19	6 15 16 18	cofidfth	$$⊢\phi \to 1^{st}\left(K\right)\left(D\mathrm{Faith}E\right)2^{nd}\left(K\right)$$
20		df-br	$$⊢1^{st}\left(K\right)\left(D\mathrm{Faith}E\right)2^{nd}\left(K\right)\leftrightarrow ⟨1^{st}\left(K\right),2^{nd}\left(K\right)⟩\in \left(D\mathrm{Faith}E\right)$$
21	19 20	sylib	$$⊢\phi \to ⟨1^{st}\left(K\right),2^{nd}\left(K\right)⟩\in \left(D\mathrm{Faith}E\right)$$
22	14 21	eqeltrd	$$⊢\phi \to K\in \left(D\mathrm{Faith}E\right)$$
23	7 22	elind	$$⊢\phi \to K\in \left(\left(D\mathrm{Full}E\right)\cap \left(D\mathrm{Faith}E\right)\right)$$
24	1 2 3 4 5 23	uobffth	Could not format ( ph -> dom ( F ( C UP D ) X ) = dom ( G ( C UP E ) Y ) ) : No typesetting found for |- ( ph -> dom ( F ( C UP D ) X ) = dom ( G ( C UP E ) Y ) ) with typecode |-