Theorem uptrai

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$$
	uptrai.n	$$⊢\phi \to \left(X{2}^{nd}\left(K\right)1^{st}\left(F\right)\left(Z\right)\right)\left(M\right)=N$$
	uptrai.z	No typesetting found for |- ( ph -> Z ( F ( C UP D ) X ) M ) with typecode |-
Assertion	uptrai	Could not format assertion : No typesetting found for |- ( ph -> 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		uptrai.n	$$⊢\phi \to \left(X{2}^{nd}\left(K\right)1^{st}\left(F\right)\left(Z\right)\right)\left(M\right)=N$$
5		uptrai.z	Could not format ( ph -> Z ( F ( C UP D ) X ) M ) : No typesetting found for |- ( ph -> Z ( F ( C UP D ) X ) M ) with typecode |-
6	1	adantr	Could not format ( ( ph /\ Z ( F ( C UP D ) X ) M ) -> ( ( 1st ` K ) ` X ) = Y ) : No typesetting found for |- ( ( ph /\ Z ( F ( C UP D ) X ) M ) -> ( ( 1st ` K ) ` X ) = Y ) with typecode |-
7	2	adantr	Could not format ( ( ph /\ Z ( F ( C UP D ) X ) M ) -> K e. ( ( D Full E ) i^i ( D Faith E ) ) ) : No typesetting found for |- ( ( ph /\ Z ( F ( C UP D ) X ) M ) -> K e. ( ( D Full E ) i^i ( D Faith E ) ) ) with typecode |-
8	3	adantr	Could not format ( ( ph /\ Z ( F ( C UP D ) X ) M ) -> ( K o.func F ) = G ) : No typesetting found for |- ( ( ph /\ Z ( F ( C UP D ) X ) M ) -> ( K o.func F ) = G ) with typecode |-
9		eqid	$$⊢{\mathrm{Base}}_D={\mathrm{Base}}_D$$
10		simpr	Could not format ( ( ph /\ Z ( F ( C UP D ) X ) M ) -> Z ( F ( C UP D ) X ) M ) : No typesetting found for |- ( ( ph /\ Z ( F ( C UP D ) X ) M ) -> Z ( F ( C UP D ) X ) M ) with typecode |-
11	10	up1st2nd	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 |-
12	11 9	uprcl3	Could not format ( ( ph /\ Z ( F ( C UP D ) X ) M ) -> X e. ( Base ` D ) ) : No typesetting found for |- ( ( ph /\ Z ( F ( C UP D ) X ) M ) -> X e. ( Base ` D ) ) with typecode |-
13	10	uprcl2a	Could not format ( ( ph /\ Z ( F ( C UP D ) X ) M ) -> F e. ( C Func D ) ) : No typesetting found for |- ( ( ph /\ Z ( F ( C UP D ) X ) M ) -> F e. ( C Func D ) ) with typecode |-
14	4	adantr	Could not format ( ( ph /\ Z ( F ( C UP D ) X ) M ) -> ( ( X ( 2nd ` K ) ( ( 1st ` F ) ` Z ) ) ` M ) = N ) : No typesetting found for |- ( ( ph /\ Z ( F ( C UP D ) X ) M ) -> ( ( X ( 2nd ` K ) ( ( 1st ` F ) ` Z ) ) ` M ) = N ) with typecode |-
15		eqid	$$⊢\mathrm{Hom}\left(D\right)=\mathrm{Hom}\left(D\right)$$
16	11 15	uprcl5	Could not format ( ( ph /\ Z ( F ( C UP D ) X ) M ) -> M e. ( X ( Hom ` D ) ( ( 1st ` F ) ` Z ) ) ) : No typesetting found for |- ( ( ph /\ Z ( F ( C UP D ) X ) M ) -> M e. ( X ( Hom ` D ) ( ( 1st ` F ) ` Z ) ) ) with typecode |-
17	6 7 8 9 12 13 14 15 16	uptra	Could not format ( ( ph /\ Z ( F ( C UP D ) X ) M ) -> ( 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 ( F ( C UP D ) X ) M <-> Z ( G ( C UP E ) Y ) N ) ) with typecode |-
18	5 17	mpdan	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 |-
19	5 18	mpbid	Could not format ( ph -> Z ( G ( C UP E ) Y ) N ) : No typesetting found for |- ( ph -> Z ( G ( C UP E ) Y ) N ) with typecode |-