Metamath Proof Explorer

Theorem uptrar

Description: Universal property and fully faithful functor. (Contributed by Zhi Wang, 17-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 ) )
uptrar.m 
|- ( ph -> ( `' ( X ( 2nd ` K ) ( ( 1st ` F ) ` Z ) ) ` N ) = M )
uptrar.z 
|- ( ph -> Z ( G ( C UP E ) Y ) N )
Assertion uptrar 
|- ( ph -> Z ( F ( C UP D ) X ) M )

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 uptrar.m 
 |-  ( ph -> ( `' ( X ( 2nd ` K ) ( ( 1st ` F ) ` Z ) ) ` N ) = M )
8 uptrar.z 
 |-  ( ph -> Z ( G ( C UP E ) Y ) N )
9 1 adantr 
 |-  ( ( ph /\ Z ( G ( C UP E ) Y ) N ) -> ( ( 1st ` K ) ` X ) = Y )
10 2 adantr 
 |-  ( ( ph /\ Z ( G ( C UP E ) Y ) N ) -> K e. ( ( D Full E ) i^i ( D Faith E ) ) )
11 3 adantr 
 |-  ( ( ph /\ Z ( G ( C UP E ) Y ) N ) -> ( K o.func F ) = G )
12 5 adantr 
 |-  ( ( ph /\ Z ( G ( C UP E ) Y ) N ) -> X e. B )
13 6 adantr 
 |-  ( ( ph /\ Z ( G ( C UP E ) Y ) N ) -> F e. ( C Func D ) )
14 7 adantr 
 |-  ( ( ph /\ Z ( G ( C UP E ) Y ) N ) -> ( `' ( X ( 2nd ` K ) ( ( 1st ` F ) ` Z ) ) ` N ) = M )
15 14 fveq2d 
 |-  ( ( ph /\ Z ( G ( C UP E ) Y ) N ) -> ( ( X ( 2nd ` K ) ( ( 1st ` F ) ` Z ) ) ` ( `' ( X ( 2nd ` K ) ( ( 1st ` F ) ` Z ) ) ` N ) ) = ( ( X ( 2nd ` K ) ( ( 1st ` F ) ` Z ) ) ` M ) )
16 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
17 eqid 
 |-  ( Hom ` E ) = ( Hom ` E )
18 relfull 
 |-  Rel ( D Full E )
19 relin1 
 |-  ( Rel ( D Full E ) -> Rel ( ( D Full E ) i^i ( D Faith E ) ) )
20 18 19 ax-mp 
 |-  Rel ( ( D Full E ) i^i ( D Faith E ) )
21 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 ) )
22 20 2 21 sylancr 
 |-  ( ph -> ( 1st ` K ) ( ( D Full E ) i^i ( D Faith E ) ) ( 2nd ` K ) )
23 22 adantr 
 |-  ( ( ph /\ Z ( G ( C UP E ) Y ) N ) -> ( 1st ` K ) ( ( D Full E ) i^i ( D Faith E ) ) ( 2nd ` K ) )
24 eqid 
 |-  ( Base ` C ) = ( Base ` C )
25 13 func1st2nd 
 |-  ( ( ph /\ Z ( G ( C UP E ) Y ) N ) -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
26 24 4 25 funcf1 
 |-  ( ( ph /\ Z ( G ( C UP E ) Y ) N ) -> ( 1st ` F ) : ( Base ` C ) --> B )
27 simpr 
 |-  ( ( ph /\ Z ( G ( C UP E ) Y ) N ) -> Z ( G ( C UP E ) Y ) N )
28 27 up1st2nd 
 |-  ( ( ph /\ Z ( G ( C UP E ) Y ) N ) -> Z ( <. ( 1st ` G ) , ( 2nd ` G ) >. ( C UP E ) Y ) N )
29 28 24 uprcl4 
 |-  ( ( ph /\ Z ( G ( C UP E ) Y ) N ) -> Z e. ( Base ` C ) )
30 26 29 ffvelcdmd 
 |-  ( ( ph /\ Z ( G ( C UP E ) Y ) N ) -> ( ( 1st ` F ) ` Z ) e. B )
31 4 16 17 23 12 30 ffthf1o 
 |-  ( ( ph /\ Z ( G ( C UP E ) Y ) N ) -> ( X ( 2nd ` K ) ( ( 1st ` F ) ` Z ) ) : ( X ( Hom ` D ) ( ( 1st ` F ) ` Z ) ) -1-1-onto-> ( ( ( 1st ` K ) ` X ) ( Hom ` E ) ( ( 1st ` K ) ` ( ( 1st ` F ) ` Z ) ) ) )
32 inss1 
 |-  ( ( D Full E ) i^i ( D Faith E ) ) C_ ( D Full E )
33 fullfunc 
 |-  ( D Full E ) C_ ( D Func E )
34 32 33 sstri 
 |-  ( ( D Full E ) i^i ( D Faith E ) ) C_ ( D Func E )
35 34 2 sselid 
 |-  ( ph -> K e. ( D Func E ) )
36 35 adantr 
 |-  ( ( ph /\ Z ( G ( C UP E ) Y ) N ) -> K e. ( D Func E ) )
37 24 13 36 29 cofu1 
 |-  ( ( ph /\ Z ( G ( C UP E ) Y ) N ) -> ( ( 1st ` ( K o.func F ) ) ` Z ) = ( ( 1st ` K ) ` ( ( 1st ` F ) ` Z ) ) )
38 11 fveq2d 
 |-  ( ( ph /\ Z ( G ( C UP E ) Y ) N ) -> ( 1st ` ( K o.func F ) ) = ( 1st ` G ) )
39 38 fveq1d 
 |-  ( ( ph /\ Z ( G ( C UP E ) Y ) N ) -> ( ( 1st ` ( K o.func F ) ) ` Z ) = ( ( 1st ` G ) ` Z ) )
40 37 39 eqtr3d 
 |-  ( ( ph /\ Z ( G ( C UP E ) Y ) N ) -> ( ( 1st ` K ) ` ( ( 1st ` F ) ` Z ) ) = ( ( 1st ` G ) ` Z ) )
41 9 40 oveq12d 
 |-  ( ( ph /\ Z ( G ( C UP E ) Y ) N ) -> ( ( ( 1st ` K ) ` X ) ( Hom ` E ) ( ( 1st ` K ) ` ( ( 1st ` F ) ` Z ) ) ) = ( Y ( Hom ` E ) ( ( 1st ` G ) ` Z ) ) )
42 41 f1oeq3d 
 |-  ( ( ph /\ Z ( G ( C UP E ) Y ) N ) -> ( ( X ( 2nd ` K ) ( ( 1st ` F ) ` Z ) ) : ( X ( Hom ` D ) ( ( 1st ` F ) ` Z ) ) -1-1-onto-> ( ( ( 1st ` K ) ` X ) ( Hom ` E ) ( ( 1st ` K ) ` ( ( 1st ` F ) ` Z ) ) ) <-> ( X ( 2nd ` K ) ( ( 1st ` F ) ` Z ) ) : ( X ( Hom ` D ) ( ( 1st ` F ) ` Z ) ) -1-1-onto-> ( Y ( Hom ` E ) ( ( 1st ` G ) ` Z ) ) ) )
43 31 42 mpbid 
 |-  ( ( ph /\ Z ( G ( C UP E ) Y ) N ) -> ( X ( 2nd ` K ) ( ( 1st ` F ) ` Z ) ) : ( X ( Hom ` D ) ( ( 1st ` F ) ` Z ) ) -1-1-onto-> ( Y ( Hom ` E ) ( ( 1st ` G ) ` Z ) ) )
44 28 17 uprcl5 
 |-  ( ( ph /\ Z ( G ( C UP E ) Y ) N ) -> N e. ( Y ( Hom ` E ) ( ( 1st ` G ) ` Z ) ) )
45 f1ocnvfv2 
 |-  ( ( ( X ( 2nd ` K ) ( ( 1st ` F ) ` Z ) ) : ( X ( Hom ` D ) ( ( 1st ` F ) ` Z ) ) -1-1-onto-> ( Y ( Hom ` E ) ( ( 1st ` G ) ` Z ) ) /\ N e. ( Y ( Hom ` E ) ( ( 1st ` G ) ` Z ) ) ) -> ( ( X ( 2nd ` K ) ( ( 1st ` F ) ` Z ) ) ` ( `' ( X ( 2nd ` K ) ( ( 1st ` F ) ` Z ) ) ` N ) ) = N )
46 43 44 45 syl2anc 
 |-  ( ( ph /\ Z ( G ( C UP E ) Y ) N ) -> ( ( X ( 2nd ` K ) ( ( 1st ` F ) ` Z ) ) ` ( `' ( X ( 2nd ` K ) ( ( 1st ` F ) ` Z ) ) ` N ) ) = N )
47 15 46 eqtr3d 
 |-  ( ( ph /\ Z ( G ( C UP E ) Y ) N ) -> ( ( X ( 2nd ` K ) ( ( 1st ` F ) ` Z ) ) ` M ) = N )
48 f1ocnvdm 
 |-  ( ( ( X ( 2nd ` K ) ( ( 1st ` F ) ` Z ) ) : ( X ( Hom ` D ) ( ( 1st ` F ) ` Z ) ) -1-1-onto-> ( Y ( Hom ` E ) ( ( 1st ` G ) ` Z ) ) /\ N e. ( Y ( Hom ` E ) ( ( 1st ` G ) ` Z ) ) ) -> ( `' ( X ( 2nd ` K ) ( ( 1st ` F ) ` Z ) ) ` N ) e. ( X ( Hom ` D ) ( ( 1st ` F ) ` Z ) ) )
49 43 44 48 syl2anc 
 |-  ( ( ph /\ Z ( G ( C UP E ) Y ) N ) -> ( `' ( X ( 2nd ` K ) ( ( 1st ` F ) ` Z ) ) ` N ) e. ( X ( Hom ` D ) ( ( 1st ` F ) ` Z ) ) )
50 14 49 eqeltrrd 
 |-  ( ( ph /\ Z ( G ( C UP E ) Y ) N ) -> M e. ( X ( Hom ` D ) ( ( 1st ` F ) ` Z ) ) )
51 9 10 11 4 12 13 47 16 50 uptra 
 |-  ( ( ph /\ Z ( G ( C UP E ) Y ) N ) -> ( Z ( F ( C UP D ) X ) M <-> Z ( G ( C UP E ) Y ) N ) )
52 8 51 mpdan 
 |-  ( ph -> ( Z ( F ( C UP D ) X ) M <-> Z ( G ( C UP E ) Y ) N ) )
53 8 52 mpbird 
 |-  ( ph -> Z ( F ( C UP D ) X ) M )