Theorem uptra

Description: Universal property and fully faithful functor. (Contributed by Zhi Wang, 16-Nov-2025)

	Ref	Expression
Hypotheses	uptra.y	$$⊢\phi \to 1^{st}\left(K\right)\left(X\right)=Y$$
	uptra.k	$$⊢\phi \to K\in \left(\left(D\mathrm{Full}E\right)\cap \left(D\mathrm{Faith}E\right)\right)$$
	uptra.g	$$⊢\phi \to K{\circ }_{\mathrm{func}}F=G$$
	uptra.b	$$⊢B={\mathrm{Base}}_D$$
	uptra.x	$$⊢\phi \to X\in B$$
	uptra.f	$$⊢\phi \to F\in \left(C\mathrm{Func}D\right)$$
	uptra.n	$$⊢\phi \to \left(X{2}^{nd}\left(K\right)1^{st}\left(F\right)\left(Z\right)\right)\left(M\right)=N$$
	uptra.j	$$⊢J=\mathrm{Hom}\left(D\right)$$
	uptra.m	$$⊢\phi \to M\in \left(XJ{1}^{st}\left(F\right)\left(Z\right)\right)$$
Assertion	uptra	Could not format assertion : No typesetting found for |- ( ph -> ( Z ( F ( C UP D ) X ) M <-> Z ( G ( C UP E ) Y ) N ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		uptra.y	$$⊢\phi \to 1^{st}\left(K\right)\left(X\right)=Y$$
2		uptra.k	$$⊢\phi \to K\in \left(\left(D\mathrm{Full}E\right)\cap \left(D\mathrm{Faith}E\right)\right)$$
3		uptra.g	$$⊢\phi \to K{\circ }_{\mathrm{func}}F=G$$
4		uptra.b	$$⊢B={\mathrm{Base}}_D$$
5		uptra.x	$$⊢\phi \to X\in B$$
6		uptra.f	$$⊢\phi \to F\in \left(C\mathrm{Func}D\right)$$
7		uptra.n	$$⊢\phi \to \left(X{2}^{nd}\left(K\right)1^{st}\left(F\right)\left(Z\right)\right)\left(M\right)=N$$
8		uptra.j	$$⊢J=\mathrm{Hom}\left(D\right)$$
9		uptra.m	$$⊢\phi \to M\in \left(XJ{1}^{st}\left(F\right)\left(Z\right)\right)$$
10		relfull	$$⊢\mathrm{Rel}\left(D\mathrm{Full}E\right)$$
11		relin1	$$⊢\mathrm{Rel}\left(D\mathrm{Full}E\right)\to \mathrm{Rel}\left(\left(D\mathrm{Full}E\right)\cap \left(D\mathrm{Faith}E\right)\right)$$
12	10 11	ax-mp	$$⊢\mathrm{Rel}\left(\left(D\mathrm{Full}E\right)\cap \left(D\mathrm{Faith}E\right)\right)$$
13		1st2ndbr	$$⊢\left(\mathrm{Rel}\left(\left(D\mathrm{Full}E\right)\cap \left(D\mathrm{Faith}E\right)\right)\wedge K\in \left(\left(D\mathrm{Full}E\right)\cap \left(D\mathrm{Faith}E\right)\right)\right)\to 1^{st}\left(K\right)\left(\left(D\mathrm{Full}E\right)\cap \left(D\mathrm{Faith}E\right)\right)2^{nd}\left(K\right)$$
14	12 2 13	sylancr	$$⊢\phi \to 1^{st}\left(K\right)\left(\left(D\mathrm{Full}E\right)\cap \left(D\mathrm{Faith}E\right)\right)2^{nd}\left(K\right)$$
15		inss1	$$⊢\left(D\mathrm{Full}E\right)\cap \left(D\mathrm{Faith}E\right)\subseteq D\mathrm{Full}E$$
16		fullfunc	$$⊢D\mathrm{Full}E\subseteq D\mathrm{Func}E$$
17	15 16	sstri	$$⊢\left(D\mathrm{Full}E\right)\cap \left(D\mathrm{Faith}E\right)\subseteq D\mathrm{Func}E$$
18	17 2	sselid	$$⊢\phi \to K\in \left(D\mathrm{Func}E\right)$$
19	6 18	cofu1st2nd	$$⊢\phi \to K{\circ }_{\mathrm{func}}F=⟨1^{st}\left(K\right),2^{nd}\left(K\right)⟩{\circ }_{\mathrm{func}}⟨1^{st}\left(F\right),2^{nd}\left(F\right)⟩$$
20		relfunc	$$⊢\mathrm{Rel}\left(C\mathrm{Func}E\right)$$
21	6 18	cofucl	$$⊢\phi \to K{\circ }_{\mathrm{func}}F\in \left(C\mathrm{Func}E\right)$$
22	3 21	eqeltrrd	$$⊢\phi \to G\in \left(C\mathrm{Func}E\right)$$
23		1st2nd	$$⊢\left(\mathrm{Rel}\left(C\mathrm{Func}E\right)\wedge G\in \left(C\mathrm{Func}E\right)\right)\to G=⟨1^{st}\left(G\right),2^{nd}\left(G\right)⟩$$
24	20 22 23	sylancr	$$⊢\phi \to G=⟨1^{st}\left(G\right),2^{nd}\left(G\right)⟩$$
25	3 19 24	3eqtr3d	$$⊢\phi \to ⟨1^{st}\left(K\right),2^{nd}\left(K\right)⟩{\circ }_{\mathrm{func}}⟨1^{st}\left(F\right),2^{nd}\left(F\right)⟩=⟨1^{st}\left(G\right),2^{nd}\left(G\right)⟩$$
26	6	func1st2nd	$$⊢\phi \to 1^{st}\left(F\right)\left(C\mathrm{Func}D\right)2^{nd}\left(F\right)$$
27	1 14 25 4 5 26 7 8 9	uptr	Could not format ( ph -> ( Z ( <. ( 1st ` F ) , ( 2nd ` F ) >. ( C UP D ) X ) M <-> Z ( <. ( 1st ` G ) , ( 2nd ` G ) >. ( C UP E ) Y ) N ) ) : No typesetting found for |- ( ph -> ( Z ( <. ( 1st ` F ) , ( 2nd ` F ) >. ( C UP D ) X ) M <-> Z ( <. ( 1st ` G ) , ( 2nd ` G ) >. ( C UP E ) Y ) N ) ) with typecode |-
28	6	up1st2ndb	Could not format ( ph -> ( Z ( F ( C UP D ) X ) M <-> Z ( <. ( 1st ` F ) , ( 2nd ` F ) >. ( C UP D ) X ) M ) ) : No typesetting found for |- ( ph -> ( Z ( F ( C UP D ) X ) M <-> Z ( <. ( 1st ` F ) , ( 2nd ` F ) >. ( C UP D ) X ) M ) ) with typecode |-
29	22	up1st2ndb	Could not format ( ph -> ( Z ( G ( C UP E ) Y ) N <-> Z ( <. ( 1st ` G ) , ( 2nd ` G ) >. ( C UP E ) Y ) N ) ) : No typesetting found for |- ( ph -> ( Z ( G ( C UP E ) Y ) N <-> Z ( <. ( 1st ` G ) , ( 2nd ` G ) >. ( C UP E ) Y ) N ) ) with typecode |-
30	27 28 29	3bitr4d	Could not format ( ph -> ( Z ( F ( C UP D ) X ) M <-> Z ( G ( C UP E ) Y ) N ) ) : No typesetting found for |- ( ph -> ( Z ( F ( C UP D ) X ) M <-> Z ( G ( C UP E ) Y ) N ) ) with typecode |-