Metamath Proof Explorer

Theorem uptra

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 )
uptra.b 
|- B = ( Base ` D )
uptra.x 
|- ( ph -> X e. B )
uptra.f 
|- ( ph -> F e. ( C Func D ) )
uptra.n 
|- ( ph -> ( ( X ( 2nd ` K ) ( ( 1st ` F ) ` Z ) ) ` M ) = N )
uptra.j 
|- J = ( Hom ` D )
uptra.m 
|- ( ph -> M e. ( X J ( ( 1st ` F ) ` Z ) ) )
Assertion uptra 
|- ( ph -> ( Z ( F ( C UP D ) X ) M <-> 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 uptra.b 
 |-  B = ( Base ` D )
5 uptra.x 
 |-  ( ph -> X e. B )
6 uptra.f 
 |-  ( ph -> F e. ( C Func D ) )
7 uptra.n 
 |-  ( ph -> ( ( X ( 2nd ` K ) ( ( 1st ` F ) ` Z ) ) ` M ) = N )
8 uptra.j 
 |-  J = ( Hom ` D )
9 uptra.m 
 |-  ( ph -> M e. ( X J ( ( 1st ` F ) ` Z ) ) )
10 relfull 
 |-  Rel ( D Full E )
11 relin1 
 |-  ( Rel ( D Full E ) -> Rel ( ( D Full E ) i^i ( D Faith E ) ) )
12 10 11 ax-mp 
 |-  Rel ( ( D Full E ) i^i ( D Faith E ) )
13 1st2ndbr 
 |-  ( ( Rel ( ( D Full E ) i^i ( D Faith E ) ) /\ K e. ( ( D Full E ) i^i ( D Faith E ) ) ) -> ( 1st ` K ) ( ( D Full E ) i^i ( D Faith E ) ) ( 2nd ` K ) )
14 12 2 13 sylancr 
 |-  ( ph -> ( 1st ` K ) ( ( D Full E ) i^i ( D Faith E ) ) ( 2nd ` K ) )
15 inss1 
 |-  ( ( D Full E ) i^i ( D Faith E ) ) C_ ( D Full E )
16 fullfunc 
 |-  ( D Full E ) C_ ( D Func E )
17 15 16 sstri 
 |-  ( ( D Full E ) i^i ( D Faith E ) ) C_ ( D Func E )
18 17 2 sselid 
 |-  ( ph -> K e. ( D Func E ) )
19 6 18 cofu1st2nd 
 |-  ( ph -> ( K o.func F ) = ( <. ( 1st ` K ) , ( 2nd ` K ) >. o.func <. ( 1st ` F ) , ( 2nd ` F ) >. ) )
20 relfunc 
 |-  Rel ( C Func E )
21 6 18 cofucl 
 |-  ( ph -> ( K o.func F ) e. ( C Func E ) )
22 3 21 eqeltrrd 
 |-  ( ph -> G e. ( C Func E ) )
23 1st2nd 
 |-  ( ( Rel ( C Func E ) /\ G e. ( C Func E ) ) -> G = <. ( 1st ` G ) , ( 2nd ` G ) >. )
24 20 22 23 sylancr 
 |-  ( ph -> G = <. ( 1st ` G ) , ( 2nd ` G ) >. )
25 3 19 24 3eqtr3d 
 |-  ( ph -> ( <. ( 1st ` K ) , ( 2nd ` K ) >. o.func <. ( 1st ` F ) , ( 2nd ` F ) >. ) = <. ( 1st ` G ) , ( 2nd ` G ) >. )
26 6 func1st2nd 
 |-  ( ph -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
27 1 14 25 4 5 26 7 8 9 uptr 
 |-  ( ph -> ( Z ( <. ( 1st ` F ) , ( 2nd ` F ) >. ( C UP D ) X ) M <-> Z ( <. ( 1st ` G ) , ( 2nd ` G ) >. ( C UP E ) Y ) N ) )
28 6 up1st2ndb 
 |-  ( ph -> ( Z ( F ( C UP D ) X ) M <-> Z ( <. ( 1st ` F ) , ( 2nd ` F ) >. ( C UP D ) X ) M ) )
29 22 up1st2ndb 
 |-  ( ph -> ( Z ( G ( C UP E ) Y ) N <-> Z ( <. ( 1st ` G ) , ( 2nd ` G ) >. ( C UP E ) Y ) N ) )
30 27 28 29 3bitr4d 
 |-  ( ph -> ( Z ( F ( C UP D ) X ) M <-> Z ( G ( C UP E ) Y ) N ) )