Theorem uptri

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

	Ref	Expression
Hypotheses	uptr.y	$$⊢\phi \to R\left(X\right)=Y$$
	uptr.r	$$⊢\phi \to R\left(\left(D\mathrm{Full}E\right)\cap \left(D\mathrm{Faith}E\right)\right)S$$
	uptr.k	$$⊢\phi \to ⟨R,S⟩{\circ }_{\mathrm{func}}⟨F,G⟩=⟨K,L⟩$$
	uptri.n	$$⊢\phi \to \left(XSF\left(Z\right)\right)\left(M\right)=N$$
	uptri.z	No typesetting found for |- ( ph -> Z ( <. F , G >. ( C UP D ) X ) M ) with typecode |-
Assertion	uptri	Could not format assertion : No typesetting found for |- ( ph -> Z ( <. K , L >. ( C UP E ) Y ) N ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		uptr.y	$$⊢\phi \to R\left(X\right)=Y$$
2		uptr.r	$$⊢\phi \to R\left(\left(D\mathrm{Full}E\right)\cap \left(D\mathrm{Faith}E\right)\right)S$$
3		uptr.k	$$⊢\phi \to ⟨R,S⟩{\circ }_{\mathrm{func}}⟨F,G⟩=⟨K,L⟩$$
4		uptri.n	$$⊢\phi \to \left(XSF\left(Z\right)\right)\left(M\right)=N$$
5		uptri.z	Could not format ( ph -> Z ( <. F , G >. ( C UP D ) X ) M ) : No typesetting found for |- ( ph -> Z ( <. F , G >. ( C UP D ) X ) M ) with typecode |-
6	1	adantr	Could not format ( ( ph /\ Z ( <. F , G >. ( C UP D ) X ) M ) -> ( R ` X ) = Y ) : No typesetting found for |- ( ( ph /\ Z ( <. F , G >. ( C UP D ) X ) M ) -> ( R ` X ) = Y ) with typecode |-
7	2	adantr	Could not format ( ( ph /\ Z ( <. F , G >. ( C UP D ) X ) M ) -> R ( ( D Full E ) i^i ( D Faith E ) ) S ) : No typesetting found for |- ( ( ph /\ Z ( <. F , G >. ( C UP D ) X ) M ) -> R ( ( D Full E ) i^i ( D Faith E ) ) S ) with typecode |-
8	3	adantr	Could not format ( ( ph /\ Z ( <. F , G >. ( C UP D ) X ) M ) -> ( <. R , S >. o.func <. F , G >. ) = <. K , L >. ) : No typesetting found for |- ( ( ph /\ Z ( <. F , G >. ( C UP D ) X ) M ) -> ( <. R , S >. o.func <. F , G >. ) = <. K , L >. ) with typecode |-
9		eqid	$$⊢{\mathrm{Base}}_D={\mathrm{Base}}_D$$
10	5	adantr	Could not format ( ( ph /\ Z ( <. F , G >. ( C UP D ) X ) M ) -> Z ( <. F , G >. ( C UP D ) X ) M ) : No typesetting found for |- ( ( ph /\ Z ( <. F , G >. ( C UP D ) X ) M ) -> Z ( <. F , G >. ( C UP D ) X ) M ) with typecode |-
11	10 9	uprcl3	Could not format ( ( ph /\ Z ( <. F , G >. ( C UP D ) X ) M ) -> X e. ( Base ` D ) ) : No typesetting found for |- ( ( ph /\ Z ( <. F , G >. ( C UP D ) X ) M ) -> X e. ( Base ` D ) ) with typecode |-
12	10	uprcl2	Could not format ( ( ph /\ Z ( <. F , G >. ( C UP D ) X ) M ) -> F ( C Func D ) G ) : No typesetting found for |- ( ( ph /\ Z ( <. F , G >. ( C UP D ) X ) M ) -> F ( C Func D ) G ) with typecode |-
13	4	adantr	Could not format ( ( ph /\ Z ( <. F , G >. ( C UP D ) X ) M ) -> ( ( X S ( F ` Z ) ) ` M ) = N ) : No typesetting found for |- ( ( ph /\ Z ( <. F , G >. ( C UP D ) X ) M ) -> ( ( X S ( F ` Z ) ) ` M ) = N ) with typecode |-
14		eqid	$$⊢\mathrm{Hom}\left(D\right)=\mathrm{Hom}\left(D\right)$$
15	10 14	uprcl5	Could not format ( ( ph /\ Z ( <. F , G >. ( C UP D ) X ) M ) -> M e. ( X ( Hom ` D ) ( F ` Z ) ) ) : No typesetting found for |- ( ( ph /\ Z ( <. F , G >. ( C UP D ) X ) M ) -> M e. ( X ( Hom ` D ) ( F ` Z ) ) ) with typecode |-
16	6 7 8 9 11 12 13 14 15	uptr	Could not format ( ( ph /\ Z ( <. F , G >. ( C UP D ) X ) M ) -> ( Z ( <. F , G >. ( C UP D ) X ) M <-> Z ( <. K , L >. ( C UP E ) Y ) N ) ) : No typesetting found for |- ( ( ph /\ Z ( <. F , G >. ( C UP D ) X ) M ) -> ( Z ( <. F , G >. ( C UP D ) X ) M <-> Z ( <. K , L >. ( C UP E ) Y ) N ) ) with typecode |-
17	5 16	mpdan	Could not format ( ph -> ( Z ( <. F , G >. ( C UP D ) X ) M <-> Z ( <. K , L >. ( C UP E ) Y ) N ) ) : No typesetting found for |- ( ph -> ( Z ( <. F , G >. ( C UP D ) X ) M <-> Z ( <. K , L >. ( C UP E ) Y ) N ) ) with typecode |-
18	5 17	mpbid	Could not format ( ph -> Z ( <. K , L >. ( C UP E ) Y ) N ) : No typesetting found for |- ( ph -> Z ( <. K , L >. ( C UP E ) Y ) N ) with typecode |-