Metamath Proof Explorer

Theorem uptr

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 >. )
uptr.b 
|- B = ( Base ` D )
uptr.x 
|- ( ph -> X e. B )
uptr.f 
|- ( ph -> F ( C Func D ) G )
uptr.n 
|- ( ph -> ( ( X S ( F ` Z ) ) ` M ) = N )
uptr.j 
|- J = ( Hom ` D )
uptr.m 
|- ( ph -> M e. ( X J ( F ` Z ) ) )
Assertion uptr 
|- ( ph -> ( Z ( <. F , G >. ( C UP D ) X ) M <-> 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 uptr.b 
 |-  B = ( Base ` D )
5 uptr.x 
 |-  ( ph -> X e. B )
6 uptr.f 
 |-  ( ph -> F ( C Func D ) G )
7 uptr.n 
 |-  ( ph -> ( ( X S ( F ` Z ) ) ` M ) = N )
8 uptr.j 
 |-  J = ( Hom ` D )
9 uptr.m 
 |-  ( ph -> M e. ( X J ( F ` Z ) ) )
10 simpr 
 |-  ( ( ph /\ Z ( <. F , G >. ( C UP D ) X ) M ) -> Z ( <. F , G >. ( C UP D ) X ) M )
11 simpr 
 |-  ( ( ph /\ Z ( <. K , L >. ( C UP E ) Y ) N ) -> Z ( <. K , L >. ( C UP E ) Y ) N )
12 1 adantr 
 |-  ( ( ph /\ Z ( <. K , L >. ( C UP E ) Y ) N ) -> ( R ` X ) = Y )
13 2 adantr 
 |-  ( ( ph /\ Z ( <. K , L >. ( C UP E ) Y ) N ) -> R ( ( D Full E ) i^i ( D Faith E ) ) S )
14 3 adantr 
 |-  ( ( ph /\ Z ( <. K , L >. ( C UP E ) Y ) N ) -> ( <. R , S >. o.func <. F , G >. ) = <. K , L >. )
15 5 adantr 
 |-  ( ( ph /\ Z ( <. K , L >. ( C UP E ) Y ) N ) -> X e. B )
16 6 adantr 
 |-  ( ( ph /\ Z ( <. K , L >. ( C UP E ) Y ) N ) -> F ( C Func D ) G )
17 7 adantr 
 |-  ( ( ph /\ Z ( <. K , L >. ( C UP E ) Y ) N ) -> ( ( X S ( F ` Z ) ) ` M ) = N )
18 9 adantr 
 |-  ( ( ph /\ Z ( <. K , L >. ( C UP E ) Y ) N ) -> M e. ( X J ( F ` Z ) ) )
19 eqid 
 |-  ( Base ` C ) = ( Base ` C )
20 11 19 uprcl4 
 |-  ( ( ph /\ Z ( <. K , L >. ( C UP E ) Y ) N ) -> Z e. ( Base ` C ) )
21 12 13 14 4 15 16 17 8 18 19 20 uptrlem3 
 |-  ( ( ph /\ Z ( <. K , L >. ( C UP E ) Y ) N ) -> ( Z ( <. F , G >. ( C UP D ) X ) M <-> Z ( <. K , L >. ( C UP E ) Y ) N ) )
22 11 21 mpbird 
 |-  ( ( ph /\ Z ( <. K , L >. ( C UP E ) Y ) N ) -> Z ( <. F , G >. ( C UP D ) X ) M )
23 1 adantr 
 |-  ( ( ph /\ Z ( <. F , G >. ( C UP D ) X ) M ) -> ( R ` X ) = Y )
24 2 adantr 
 |-  ( ( ph /\ Z ( <. F , G >. ( C UP D ) X ) M ) -> R ( ( D Full E ) i^i ( D Faith E ) ) S )
25 3 adantr 
 |-  ( ( ph /\ Z ( <. F , G >. ( C UP D ) X ) M ) -> ( <. R , S >. o.func <. F , G >. ) = <. K , L >. )
26 5 adantr 
 |-  ( ( ph /\ Z ( <. F , G >. ( C UP D ) X ) M ) -> X e. B )
27 6 adantr 
 |-  ( ( ph /\ Z ( <. F , G >. ( C UP D ) X ) M ) -> F ( C Func D ) G )
28 7 adantr 
 |-  ( ( ph /\ Z ( <. F , G >. ( C UP D ) X ) M ) -> ( ( X S ( F ` Z ) ) ` M ) = N )
29 9 adantr 
 |-  ( ( ph /\ Z ( <. F , G >. ( C UP D ) X ) M ) -> M e. ( X J ( F ` Z ) ) )
30 10 19 uprcl4 
 |-  ( ( ph /\ Z ( <. F , G >. ( C UP D ) X ) M ) -> Z e. ( Base ` C ) )
31 23 24 25 4 26 27 28 8 29 19 30 uptrlem3 
 |-  ( ( 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 ) )
32 10 22 31 bibiad 
 |-  ( ph -> ( Z ( <. F , G >. ( C UP D ) X ) M <-> Z ( <. K , L >. ( C UP E ) Y ) N ) )