Metamath Proof Explorer

Theorem uptr2a

Description: Universal property and fully faithful functor surjective on objects. (Contributed by Zhi Wang, 25-Nov-2025)

Ref Expression
Hypotheses uptr2a.a 
|- A = ( Base ` C )
uptr2a.b 
|- B = ( Base ` D )
uptr2a.y 
|- ( ph -> Y = ( ( 1st ` K ) ` X ) )
uptr2a.f 
|- ( ph -> ( G o.func K ) = F )
uptr2a.x 
|- ( ph -> X e. A )
uptr2a.g 
|- ( ph -> G e. ( D Func E ) )
uptr2a.k 
|- ( ph -> K e. ( ( C Full D ) i^i ( C Faith D ) ) )
uptr2a.1 
|- ( ph -> ( 1st ` K ) : A -onto-> B )
Assertion uptr2a 
|- ( ph -> ( X ( F ( C UP E ) Z ) M <-> Y ( G ( D UP E ) Z ) M ) )

Proof

Step Hyp Ref Expression
1 uptr2a.a 
 |-  A = ( Base ` C )
2 uptr2a.b 
 |-  B = ( Base ` D )
3 uptr2a.y 
 |-  ( ph -> Y = ( ( 1st ` K ) ` X ) )
4 uptr2a.f 
 |-  ( ph -> ( G o.func K ) = F )
5 uptr2a.x 
 |-  ( ph -> X e. A )
6 uptr2a.g 
 |-  ( ph -> G e. ( D Func E ) )
7 uptr2a.k 
 |-  ( ph -> K e. ( ( C Full D ) i^i ( C Faith D ) ) )
8 uptr2a.1 
 |-  ( ph -> ( 1st ` K ) : A -onto-> B )
9 relfull 
 |-  Rel ( C Full D )
10 relin1 
 |-  ( Rel ( C Full D ) -> Rel ( ( C Full D ) i^i ( C Faith D ) ) )
11 9 10 ax-mp 
 |-  Rel ( ( C Full D ) i^i ( C Faith D ) )
12 1st2ndbr 
 |-  ( ( Rel ( ( C Full D ) i^i ( C Faith D ) ) /\ K e. ( ( C Full D ) i^i ( C Faith D ) ) ) -> ( 1st ` K ) ( ( C Full D ) i^i ( C Faith D ) ) ( 2nd ` K ) )
13 11 7 12 sylancr 
 |-  ( ph -> ( 1st ` K ) ( ( C Full D ) i^i ( C Faith D ) ) ( 2nd ` K ) )
14 inss1 
 |-  ( ( C Full D ) i^i ( C Faith D ) ) C_ ( C Full D )
15 fullfunc 
 |-  ( C Full D ) C_ ( C Func D )
16 14 15 sstri 
 |-  ( ( C Full D ) i^i ( C Faith D ) ) C_ ( C Func D )
17 16 7 sselid 
 |-  ( ph -> K e. ( C Func D ) )
18 17 6 cofu1st2nd 
 |-  ( ph -> ( G o.func K ) = ( <. ( 1st ` G ) , ( 2nd ` G ) >. o.func <. ( 1st ` K ) , ( 2nd ` K ) >. ) )
19 relfunc 
 |-  Rel ( C Func E )
20 17 6 cofucl 
 |-  ( ph -> ( G o.func K ) e. ( C Func E ) )
21 4 20 eqeltrrd 
 |-  ( ph -> F e. ( C Func E ) )
22 1st2nd 
 |-  ( ( Rel ( C Func E ) /\ F e. ( C Func E ) ) -> F = <. ( 1st ` F ) , ( 2nd ` F ) >. )
23 19 21 22 sylancr 
 |-  ( ph -> F = <. ( 1st ` F ) , ( 2nd ` F ) >. )
24 4 18 23 3eqtr3d 
 |-  ( ph -> ( <. ( 1st ` G ) , ( 2nd ` G ) >. o.func <. ( 1st ` K ) , ( 2nd ` K ) >. ) = <. ( 1st ` F ) , ( 2nd ` F ) >. )
25 6 func1st2nd 
 |-  ( ph -> ( 1st ` G ) ( D Func E ) ( 2nd ` G ) )
26 1 2 3 8 13 24 5 25 uptr2 
 |-  ( ph -> ( X ( <. ( 1st ` F ) , ( 2nd ` F ) >. ( C UP E ) Z ) M <-> Y ( <. ( 1st ` G ) , ( 2nd ` G ) >. ( D UP E ) Z ) M ) )
27 21 up1st2ndb 
 |-  ( ph -> ( X ( F ( C UP E ) Z ) M <-> X ( <. ( 1st ` F ) , ( 2nd ` F ) >. ( C UP E ) Z ) M ) )
28 6 up1st2ndb 
 |-  ( ph -> ( Y ( G ( D UP E ) Z ) M <-> Y ( <. ( 1st ` G ) , ( 2nd ` G ) >. ( D UP E ) Z ) M ) )
29 26 27 28 3bitr4d 
 |-  ( ph -> ( X ( F ( C UP E ) Z ) M <-> Y ( G ( D UP E ) Z ) M ) )