Theorem uptri

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

	Ref	Expression
Hypotheses	uptr.y	|- ( ph -> ( R ` X ) = Y )
	uptr.r	|- ( ph -> R ( ( D Full E ) i^i ( D Faith E ) ) S )
	uptr.k	|- ( ph -> ( <. R , S >. o.func <. F , G >. ) = <. K , L >. )
	uptri.n	|- ( ph -> ( ( X S ( F ` Z ) ) ` M ) = N )
	uptri.z	|- ( ph -> Z ( <. F , G >. ( C UP D ) X ) M )
Assertion	uptri	|- ( ph -> Z ( <. K , L >. ( C UP E ) Y ) N )

Proof

Step	Hyp	Ref	Expression
1		uptr.y	|- ( ph -> ( R ` X ) = Y )
2		uptr.r	|- ( ph -> R ( ( D Full E ) i^i ( D Faith E ) ) S )
3		uptr.k	|- ( ph -> ( <. R , S >. o.func <. F , G >. ) = <. K , L >. )
4		uptri.n	|- ( ph -> ( ( X S ( F ` Z ) ) ` M ) = N )
5		uptri.z	|- ( ph -> Z ( <. F , G >. ( C UP D ) X ) M )
6	1	adantr	|- ( ( ph /\ Z ( <. F , G >. ( C UP D ) X ) M ) -> ( R ` X ) = Y )
7	2	adantr	|- ( ( ph /\ Z ( <. F , G >. ( C UP D ) X ) M ) -> R ( ( D Full E ) i^i ( D Faith E ) ) S )
8	3	adantr	|- ( ( ph /\ Z ( <. F , G >. ( C UP D ) X ) M ) -> ( <. R , S >. o.func <. F , G >. ) = <. K , L >. )
9		eqid	|- ( Base ` D ) = ( Base ` D )
10	5	adantr	|- ( ( ph /\ Z ( <. F , G >. ( C UP D ) X ) M ) -> Z ( <. F , G >. ( C UP D ) X ) M )
11	10 9	uprcl3	|- ( ( ph /\ Z ( <. F , G >. ( C UP D ) X ) M ) -> X e. ( Base ` D ) )
12	10	uprcl2	|- ( ( ph /\ Z ( <. F , G >. ( C UP D ) X ) M ) -> F ( C Func D ) G )
13	4	adantr	|- ( ( ph /\ Z ( <. F , G >. ( C UP D ) X ) M ) -> ( ( X S ( F ` Z ) ) ` M ) = N )
14		eqid	|- ( Hom ` D ) = ( Hom ` D )
15	10 14	uprcl5	|- ( ( ph /\ Z ( <. F , G >. ( C UP D ) X ) M ) -> M e. ( X ( Hom ` D ) ( F ` Z ) ) )
16	6 7 8 9 11 12 13 14 15	uptr	|- ( ( 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 ) )
17	5 16	mpdan	|- ( ph -> ( Z ( <. F , G >. ( C UP D ) X ) M <-> Z ( <. K , L >. ( C UP E ) Y ) N ) )
18	5 17	mpbid	|- ( ph -> Z ( <. K , L >. ( C UP E ) Y ) N )