Metamath Proof Explorer

Theorem uobeqterm

Description: Universal objects and terminal categories. (Contributed by Zhi Wang, 17-Nov-2025)

Ref Expression
Hypotheses uobeqterm.a 
|- A = ( Base ` D )
uobeqterm.b 
|- B = ( Base ` E )
uobeqterm.x 
|- ( ph -> X e. A )
uobeqterm.y 
|- ( ph -> Y e. B )
uobeqterm.f 
|- ( ph -> F e. ( C Func D ) )
uobeqterm.g 
|- ( ph -> G e. ( C Func E ) )
uobeqterm.d 
|- ( ph -> D e. TermCat )
uobeqterm.e 
|- ( ph -> E e. TermCat )
Assertion uobeqterm 
|- ( ph -> dom ( F ( C UP D ) X ) = dom ( G ( C UP E ) Y ) )

Proof

Step Hyp Ref Expression
1 uobeqterm.a 
 |-  A = ( Base ` D )
2 uobeqterm.b 
 |-  B = ( Base ` E )
3 uobeqterm.x 
 |-  ( ph -> X e. A )
4 uobeqterm.y 
 |-  ( ph -> Y e. B )
5 uobeqterm.f 
 |-  ( ph -> F e. ( C Func D ) )
6 uobeqterm.g 
 |-  ( ph -> G e. ( C Func E ) )
7 uobeqterm.d 
 |-  ( ph -> D e. TermCat )
8 uobeqterm.e 
 |-  ( ph -> E e. TermCat )
9 eqid 
 |-  ( CatCat ` { D , E } ) = ( CatCat ` { D , E } )
10 eqid 
 |-  ( Base ` ( CatCat ` { D , E } ) ) = ( Base ` ( CatCat ` { D , E } ) )
11 prid1g 
 |-  ( D e. TermCat -> D e. { D , E } )
12 7 11 syl 
 |-  ( ph -> D e. { D , E } )
13 7 termccd 
 |-  ( ph -> D e. Cat )
14 12 13 elind 
 |-  ( ph -> D e. ( { D , E } i^i Cat ) )
15 prex 
 |-  { D , E } e. _V
16 15 a1i 
 |-  ( ph -> { D , E } e. _V )
17 9 10 16 catcbas 
 |-  ( ph -> ( Base ` ( CatCat ` { D , E } ) ) = ( { D , E } i^i Cat ) )
18 14 17 eleqtrrd 
 |-  ( ph -> D e. ( Base ` ( CatCat ` { D , E } ) ) )
19 prid2g 
 |-  ( E e. TermCat -> E e. { D , E } )
20 8 19 syl 
 |-  ( ph -> E e. { D , E } )
21 8 termccd 
 |-  ( ph -> E e. Cat )
22 20 21 elind 
 |-  ( ph -> E e. ( { D , E } i^i Cat ) )
23 22 17 eleqtrrd 
 |-  ( ph -> E e. ( Base ` ( CatCat ` { D , E } ) ) )
24 9 10 18 23 7 termcciso 
 |-  ( ph -> ( E e. TermCat <-> D ( ~=c ` ( CatCat ` { D , E } ) ) E ) )
25 8 24 mpbid 
 |-  ( ph -> D ( ~=c ` ( CatCat ` { D , E } ) ) E )
26 eqid 
 |-  ( Iso ` ( CatCat ` { D , E } ) ) = ( Iso ` ( CatCat ` { D , E } ) )
27 9 catccat 
 |-  ( { D , E } e. _V -> ( CatCat ` { D , E } ) e. Cat )
28 16 27 syl 
 |-  ( ph -> ( CatCat ` { D , E } ) e. Cat )
29 26 10 28 18 23 cic 
 |-  ( ph -> ( D ( ~=c ` ( CatCat ` { D , E } ) ) E <-> E. k k e. ( D ( Iso ` ( CatCat ` { D , E } ) ) E ) ) )
30 25 29 mpbid 
 |-  ( ph -> E. k k e. ( D ( Iso ` ( CatCat ` { D , E } ) ) E ) )
31 3 adantr 
 |-  ( ( ph /\ k e. ( D ( Iso ` ( CatCat ` { D , E } ) ) E ) ) -> X e. A )
32 5 adantr 
 |-  ( ( ph /\ k e. ( D ( Iso ` ( CatCat ` { D , E } ) ) E ) ) -> F e. ( C Func D ) )
33 fullfunc 
 |-  ( D Full E ) C_ ( D Func E )
34 simpr 
 |-  ( ( ph /\ k e. ( D ( Iso ` ( CatCat ` { D , E } ) ) E ) ) -> k e. ( D ( Iso ` ( CatCat ` { D , E } ) ) E ) )
35 9 1 2 26 34 catcisoi 
 |-  ( ( ph /\ k e. ( D ( Iso ` ( CatCat ` { D , E } ) ) E ) ) -> ( k e. ( ( D Full E ) i^i ( D Faith E ) ) /\ ( 1st ` k ) : A -1-1-onto-> B ) )
36 35 simpld 
 |-  ( ( ph /\ k e. ( D ( Iso ` ( CatCat ` { D , E } ) ) E ) ) -> k e. ( ( D Full E ) i^i ( D Faith E ) ) )
37 36 elin1d 
 |-  ( ( ph /\ k e. ( D ( Iso ` ( CatCat ` { D , E } ) ) E ) ) -> k e. ( D Full E ) )
38 33 37 sselid 
 |-  ( ( ph /\ k e. ( D ( Iso ` ( CatCat ` { D , E } ) ) E ) ) -> k e. ( D Func E ) )
39 6 adantr 
 |-  ( ( ph /\ k e. ( D ( Iso ` ( CatCat ` { D , E } ) ) E ) ) -> G e. ( C Func E ) )
40 8 adantr 
 |-  ( ( ph /\ k e. ( D ( Iso ` ( CatCat ` { D , E } ) ) E ) ) -> E e. TermCat )
41 32 38 39 40 cofuterm 
 |-  ( ( ph /\ k e. ( D ( Iso ` ( CatCat ` { D , E } ) ) E ) ) -> ( k o.func F ) = G )
42 38 func1st2nd 
 |-  ( ( ph /\ k e. ( D ( Iso ` ( CatCat ` { D , E } ) ) E ) ) -> ( 1st ` k ) ( D Func E ) ( 2nd ` k ) )
43 1 2 42 funcf1 
 |-  ( ( ph /\ k e. ( D ( Iso ` ( CatCat ` { D , E } ) ) E ) ) -> ( 1st ` k ) : A --> B )
44 43 31 ffvelcdmd 
 |-  ( ( ph /\ k e. ( D ( Iso ` ( CatCat ` { D , E } ) ) E ) ) -> ( ( 1st ` k ) ` X ) e. B )
45 4 adantr 
 |-  ( ( ph /\ k e. ( D ( Iso ` ( CatCat ` { D , E } ) ) E ) ) -> Y e. B )
46 40 2 44 45 termcbasmo 
 |-  ( ( ph /\ k e. ( D ( Iso ` ( CatCat ` { D , E } ) ) E ) ) -> ( ( 1st ` k ) ` X ) = Y )
47 1 31 32 41 46 9 26 34 uobeq3 
 |-  ( ( ph /\ k e. ( D ( Iso ` ( CatCat ` { D , E } ) ) E ) ) -> dom ( F ( C UP D ) X ) = dom ( G ( C UP E ) Y ) )
48 30 47 exlimddv 
 |-  ( ph -> dom ( F ( C UP D ) X ) = dom ( G ( C UP E ) Y ) )