Metamath Proof Explorer

Theorem uptrai

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

Ref Expression
Hypotheses uptra.y 
|- ( ph -> ( ( 1st ` K ) ` X ) = Y )
uptra.k 
|- ( ph -> K e. ( ( D Full E ) i^i ( D Faith E ) ) )
uptra.g 
|- ( ph -> ( K o.func F ) = G )
uptrai.n 
|- ( ph -> ( ( X ( 2nd ` K ) ( ( 1st ` F ) ` Z ) ) ` M ) = N )
uptrai.z 
|- ( ph -> Z ( F ( C UP D ) X ) M )
Assertion uptrai 
|- ( ph -> Z ( G ( C UP E ) Y ) N )

Proof

Step Hyp Ref Expression
1 uptra.y 
 |-  ( ph -> ( ( 1st ` K ) ` X ) = Y )
2 uptra.k 
 |-  ( ph -> K e. ( ( D Full E ) i^i ( D Faith E ) ) )
3 uptra.g 
 |-  ( ph -> ( K o.func F ) = G )
4 uptrai.n 
 |-  ( ph -> ( ( X ( 2nd ` K ) ( ( 1st ` F ) ` Z ) ) ` M ) = N )
5 uptrai.z 
 |-  ( ph -> Z ( F ( C UP D ) X ) M )
6 1 adantr 
 |-  ( ( ph /\ Z ( F ( C UP D ) X ) M ) -> ( ( 1st ` K ) ` X ) = Y )
7 2 adantr 
 |-  ( ( ph /\ Z ( F ( C UP D ) X ) M ) -> K e. ( ( D Full E ) i^i ( D Faith E ) ) )
8 3 adantr 
 |-  ( ( ph /\ Z ( F ( C UP D ) X ) M ) -> ( K o.func F ) = G )
9 eqid 
 |-  ( Base ` D ) = ( Base ` D )
10 simpr 
 |-  ( ( ph /\ Z ( F ( C UP D ) X ) M ) -> Z ( F ( C UP D ) X ) M )
11 10 up1st2nd 
 |-  ( ( ph /\ Z ( F ( C UP D ) X ) M ) -> Z ( <. ( 1st ` F ) , ( 2nd ` F ) >. ( C UP D ) X ) M )
12 11 9 uprcl3 
 |-  ( ( ph /\ Z ( F ( C UP D ) X ) M ) -> X e. ( Base ` D ) )
13 10 uprcl2a 
 |-  ( ( ph /\ Z ( F ( C UP D ) X ) M ) -> F e. ( C Func D ) )
14 4 adantr 
 |-  ( ( ph /\ Z ( F ( C UP D ) X ) M ) -> ( ( X ( 2nd ` K ) ( ( 1st ` F ) ` Z ) ) ` M ) = N )
15 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
16 11 15 uprcl5 
 |-  ( ( ph /\ Z ( F ( C UP D ) X ) M ) -> M e. ( X ( Hom ` D ) ( ( 1st ` F ) ` Z ) ) )
17 6 7 8 9 12 13 14 15 16 uptra 
 |-  ( ( ph /\ Z ( F ( C UP D ) X ) M ) -> ( Z ( F ( C UP D ) X ) M <-> Z ( G ( C UP E ) Y ) N ) )
18 5 17 mpdan 
 |-  ( ph -> ( Z ( F ( C UP D ) X ) M <-> Z ( G ( C UP E ) Y ) N ) )
19 5 18 mpbid 
 |-  ( ph -> Z ( G ( C UP E ) Y ) N )