Theorem uobeq2

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

	Ref	Expression
Hypotheses	uobeq2.b	$$⊢B={\mathrm{Base}}_D$$
	uobeq2.x	$$⊢\phi \to X\in B$$
	uobeq2.f	$$⊢\phi \to F\in \left(C\mathrm{Func}D\right)$$
	uobeq2.g	$$⊢\phi \to K{\circ }_{\mathrm{func}}F=G$$
	uobeq2.y	$$⊢\phi \to 1^{st}\left(K\right)\left(X\right)=Y$$
	uobeq2.q	$$⊢Q=\mathrm{CatCat}\left(U\right)$$
	uobeq2.s	$$⊢S=\mathrm{Sect}\left(Q\right)$$
	uobeq2.k	$$⊢\phi \to K\in \left(D\mathrm{Full}E\right)$$
	uobeq2.1	$$⊢\phi \to K\in \mathrm{dom}\left(DSE\right)$$
Assertion	uobeq2	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		uobeq2.b	$$⊢B={\mathrm{Base}}_D$$
2		uobeq2.x	$$⊢\phi \to X\in B$$
3		uobeq2.f	$$⊢\phi \to F\in \left(C\mathrm{Func}D\right)$$
4		uobeq2.g	$$⊢\phi \to K{\circ }_{\mathrm{func}}F=G$$
5		uobeq2.y	$$⊢\phi \to 1^{st}\left(K\right)\left(X\right)=Y$$
6		uobeq2.q	$$⊢Q=\mathrm{CatCat}\left(U\right)$$
7		uobeq2.s	$$⊢S=\mathrm{Sect}\left(Q\right)$$
8		uobeq2.k	$$⊢\phi \to K\in \left(D\mathrm{Full}E\right)$$
9		uobeq2.1	$$⊢\phi \to K\in \mathrm{dom}\left(DSE\right)$$
10		eldmg	$$⊢K\in \mathrm{dom}\left(DSE\right)\to \left(K\in \mathrm{dom}\left(DSE\right)\leftrightarrow \exists lK\left(DSE\right)l\right)$$
11	10	ibi	$$⊢K\in \mathrm{dom}\left(DSE\right)\to \exists lK\left(DSE\right)l$$
12	9 11	syl	$$⊢\phi \to \exists lK\left(DSE\right)l$$
13		eqid	$$⊢{id}_{\mathrm{func}}\left(D\right)={id}_{\mathrm{func}}\left(D\right)$$
14	2	adantr	$$⊢\left(\phi \wedge K\left(DSE\right)l\right)\to X\in B$$
15	3	adantr	$$⊢\left(\phi \wedge K\left(DSE\right)l\right)\to F\in \left(C\mathrm{Func}D\right)$$
16	8	adantr	$$⊢\left(\phi \wedge K\left(DSE\right)l\right)\to K\in \left(D\mathrm{Full}E\right)$$
17	4	adantr	$$⊢\left(\phi \wedge K\left(DSE\right)l\right)\to K{\circ }_{\mathrm{func}}F=G$$
18	5	adantr	$$⊢\left(\phi \wedge K\left(DSE\right)l\right)\to 1^{st}\left(K\right)\left(X\right)=Y$$
19		eqid	$$⊢\mathrm{Hom}\left(Q\right)=\mathrm{Hom}\left(Q\right)$$
20	6 19 13 7	catcsect	$$⊢K\left(DSE\right)l\leftrightarrow \left(\left(K\in \left(D\mathrm{Hom}\left(Q\right)E\right)\wedge l\in \left(E\mathrm{Hom}\left(Q\right)D\right)\right)\wedge l{\circ }_{\mathrm{func}}K={id}_{\mathrm{func}}\left(D\right)\right)$$
21	20	simprbi	$$⊢K\left(DSE\right)l\to l{\circ }_{\mathrm{func}}K={id}_{\mathrm{func}}\left(D\right)$$
22	21	adantl	$$⊢\left(\phi \wedge K\left(DSE\right)l\right)\to l{\circ }_{\mathrm{func}}K={id}_{\mathrm{func}}\left(D\right)$$
23	20	simplbi	$$⊢K\left(DSE\right)l\to \left(K\in \left(D\mathrm{Hom}\left(Q\right)E\right)\wedge l\in \left(E\mathrm{Hom}\left(Q\right)D\right)\right)$$
24	23	simprd	$$⊢K\left(DSE\right)l\to l\in \left(E\mathrm{Hom}\left(Q\right)D\right)$$
25	6 19 24	elcatchom	$$⊢K\left(DSE\right)l\to l\in \left(E\mathrm{Func}D\right)$$
26	25	adantl	$$⊢\left(\phi \wedge K\left(DSE\right)l\right)\to l\in \left(E\mathrm{Func}D\right)$$
27	1 13 14 15 16 17 18 22 26	uobeq	Could not format ( ( ph /\ K ( D S E ) l ) -> dom ( F ( C UP D ) X ) = dom ( G ( C UP E ) Y ) ) : No typesetting found for |- ( ( ph /\ K ( D S E ) l ) -> dom ( F ( C UP D ) X ) = dom ( G ( C UP E ) Y ) ) with typecode |-
28	12 27	exlimddv	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 |-