This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem termopropd

Description: Two structures with the same base, hom-sets and composition operation have the same terminal objects. (Contributed by Zhi Wang, 26-Oct-2025)

Ref Expression
Hypotheses initopropd.1 
|- ( ph -> ( Homf ` C ) = ( Homf ` D ) )
initopropd.2 
|- ( ph -> ( comf ` C ) = ( comf ` D ) )
Assertion termopropd 
|- ( ph -> ( TermO ` C ) = ( TermO ` D ) )

Proof

Step Hyp Ref Expression
1 initopropd.1 
 |-  ( ph -> ( Homf ` C ) = ( Homf ` D ) )
2 initopropd.2 
 |-  ( ph -> ( comf ` C ) = ( comf ` D ) )
3 1 adantr 
 |-  ( ( ph /\ -. C e. _V ) -> ( Homf ` C ) = ( Homf ` D ) )
4 2 adantr 
 |-  ( ( ph /\ -. C e. _V ) -> ( comf ` C ) = ( comf ` D ) )
5 simpr 
 |-  ( ( ph /\ -. C e. _V ) -> -. C e. _V )
6 3 4 5 termopropdlem 
 |-  ( ( ph /\ -. C e. _V ) -> ( TermO ` C ) = ( TermO ` D ) )
7 1 adantr 
 |-  ( ( ph /\ -. D e. _V ) -> ( Homf ` C ) = ( Homf ` D ) )
8 7 eqcomd 
 |-  ( ( ph /\ -. D e. _V ) -> ( Homf ` D ) = ( Homf ` C ) )
9 2 adantr 
 |-  ( ( ph /\ -. D e. _V ) -> ( comf ` C ) = ( comf ` D ) )
10 9 eqcomd 
 |-  ( ( ph /\ -. D e. _V ) -> ( comf ` D ) = ( comf ` C ) )
11 simpr 
 |-  ( ( ph /\ -. D e. _V ) -> -. D e. _V )
12 8 10 11 termopropdlem 
 |-  ( ( ph /\ -. D e. _V ) -> ( TermO ` D ) = ( TermO ` C ) )
13 12 eqcomd 
 |-  ( ( ph /\ -. D e. _V ) -> ( TermO ` C ) = ( TermO ` D ) )
14 1 adantr 
 |-  ( ( ph /\ ( C e. _V /\ D e. _V ) ) -> ( Homf ` C ) = ( Homf ` D ) )
15 14 adantr 
 |-  ( ( ( ph /\ ( C e. _V /\ D e. _V ) ) /\ C e. Cat ) -> ( Homf ` C ) = ( Homf ` D ) )
16 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
17 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
18 eqidd 
 |-  ( ( ( ph /\ ( C e. _V /\ D e. _V ) ) /\ C e. Cat ) -> ( Base ` C ) = ( Base ` C ) )
19 15 homfeqbas 
 |-  ( ( ( ph /\ ( C e. _V /\ D e. _V ) ) /\ C e. Cat ) -> ( Base ` C ) = ( Base ` D ) )
20 16 17 18 19 homfeq 
 |-  ( ( ( ph /\ ( C e. _V /\ D e. _V ) ) /\ C e. Cat ) -> ( ( Homf ` C ) = ( Homf ` D ) <-> A. b e. ( Base ` C ) A. a e. ( Base ` C ) ( b ( Hom ` C ) a ) = ( b ( Hom ` D ) a ) ) )
21 ralcom 
 |-  ( A. b e. ( Base ` C ) A. a e. ( Base ` C ) ( b ( Hom ` C ) a ) = ( b ( Hom ` D ) a ) <-> A. a e. ( Base ` C ) A. b e. ( Base ` C ) ( b ( Hom ` C ) a ) = ( b ( Hom ` D ) a ) )
22 20 21 bitrdi 
 |-  ( ( ( ph /\ ( C e. _V /\ D e. _V ) ) /\ C e. Cat ) -> ( ( Homf ` C ) = ( Homf ` D ) <-> A. a e. ( Base ` C ) A. b e. ( Base ` C ) ( b ( Hom ` C ) a ) = ( b ( Hom ` D ) a ) ) )
23 15 22 mpbid 
 |-  ( ( ( ph /\ ( C e. _V /\ D e. _V ) ) /\ C e. Cat ) -> A. a e. ( Base ` C ) A. b e. ( Base ` C ) ( b ( Hom ` C ) a ) = ( b ( Hom ` D ) a ) )
24 23 r19.21bi 
 |-  ( ( ( ( ph /\ ( C e. _V /\ D e. _V ) ) /\ C e. Cat ) /\ a e. ( Base ` C ) ) -> A. b e. ( Base ` C ) ( b ( Hom ` C ) a ) = ( b ( Hom ` D ) a ) )
25 24 r19.21bi 
 |-  ( ( ( ( ( ph /\ ( C e. _V /\ D e. _V ) ) /\ C e. Cat ) /\ a e. ( Base ` C ) ) /\ b e. ( Base ` C ) ) -> ( b ( Hom ` C ) a ) = ( b ( Hom ` D ) a ) )
26 25 eleq2d 
 |-  ( ( ( ( ( ph /\ ( C e. _V /\ D e. _V ) ) /\ C e. Cat ) /\ a e. ( Base ` C ) ) /\ b e. ( Base ` C ) ) -> ( h e. ( b ( Hom ` C ) a ) <-> h e. ( b ( Hom ` D ) a ) ) )
27 26 eubidv 
 |-  ( ( ( ( ( ph /\ ( C e. _V /\ D e. _V ) ) /\ C e. Cat ) /\ a e. ( Base ` C ) ) /\ b e. ( Base ` C ) ) -> ( E! h h e. ( b ( Hom ` C ) a ) <-> E! h h e. ( b ( Hom ` D ) a ) ) )
28 27 ralbidva 
 |-  ( ( ( ( ph /\ ( C e. _V /\ D e. _V ) ) /\ C e. Cat ) /\ a e. ( Base ` C ) ) -> ( A. b e. ( Base ` C ) E! h h e. ( b ( Hom ` C ) a ) <-> A. b e. ( Base ` C ) E! h h e. ( b ( Hom ` D ) a ) ) )
29 28 pm5.32da 
 |-  ( ( ( ph /\ ( C e. _V /\ D e. _V ) ) /\ C e. Cat ) -> ( ( a e. ( Base ` C ) /\ A. b e. ( Base ` C ) E! h h e. ( b ( Hom ` C ) a ) ) <-> ( a e. ( Base ` C ) /\ A. b e. ( Base ` C ) E! h h e. ( b ( Hom ` D ) a ) ) ) )
30 19 eleq2d 
 |-  ( ( ( ph /\ ( C e. _V /\ D e. _V ) ) /\ C e. Cat ) -> ( a e. ( Base ` C ) <-> a e. ( Base ` D ) ) )
31 19 raleqdv 
 |-  ( ( ( ph /\ ( C e. _V /\ D e. _V ) ) /\ C e. Cat ) -> ( A. b e. ( Base ` C ) E! h h e. ( b ( Hom ` D ) a ) <-> A. b e. ( Base ` D ) E! h h e. ( b ( Hom ` D ) a ) ) )
32 30 31 anbi12d 
 |-  ( ( ( ph /\ ( C e. _V /\ D e. _V ) ) /\ C e. Cat ) -> ( ( a e. ( Base ` C ) /\ A. b e. ( Base ` C ) E! h h e. ( b ( Hom ` D ) a ) ) <-> ( a e. ( Base ` D ) /\ A. b e. ( Base ` D ) E! h h e. ( b ( Hom ` D ) a ) ) ) )
33 29 32 bitrd 
 |-  ( ( ( ph /\ ( C e. _V /\ D e. _V ) ) /\ C e. Cat ) -> ( ( a e. ( Base ` C ) /\ A. b e. ( Base ` C ) E! h h e. ( b ( Hom ` C ) a ) ) <-> ( a e. ( Base ` D ) /\ A. b e. ( Base ` D ) E! h h e. ( b ( Hom ` D ) a ) ) ) )
34 33 rabbidva2 
 |-  ( ( ( ph /\ ( C e. _V /\ D e. _V ) ) /\ C e. Cat ) -> { a e. ( Base ` C ) | A. b e. ( Base ` C ) E! h h e. ( b ( Hom ` C ) a ) } = { a e. ( Base ` D ) | A. b e. ( Base ` D ) E! h h e. ( b ( Hom ` D ) a ) } )
35 simpr 
 |-  ( ( ( ph /\ ( C e. _V /\ D e. _V ) ) /\ C e. Cat ) -> C e. Cat )
36 eqid 
 |-  ( Base ` C ) = ( Base ` C )
37 35 36 16 termoval 
 |-  ( ( ( ph /\ ( C e. _V /\ D e. _V ) ) /\ C e. Cat ) -> ( TermO ` C ) = { a e. ( Base ` C ) | A. b e. ( Base ` C ) E! h h e. ( b ( Hom ` C ) a ) } )
38 2 adantr 
 |-  ( ( ph /\ ( C e. _V /\ D e. _V ) ) -> ( comf ` C ) = ( comf ` D ) )
39 simprl 
 |-  ( ( ph /\ ( C e. _V /\ D e. _V ) ) -> C e. _V )
40 simprr 
 |-  ( ( ph /\ ( C e. _V /\ D e. _V ) ) -> D e. _V )
41 14 38 39 40 catpropd 
 |-  ( ( ph /\ ( C e. _V /\ D e. _V ) ) -> ( C e. Cat <-> D e. Cat ) )
42 41 biimpa 
 |-  ( ( ( ph /\ ( C e. _V /\ D e. _V ) ) /\ C e. Cat ) -> D e. Cat )
43 eqid 
 |-  ( Base ` D ) = ( Base ` D )
44 42 43 17 termoval 
 |-  ( ( ( ph /\ ( C e. _V /\ D e. _V ) ) /\ C e. Cat ) -> ( TermO ` D ) = { a e. ( Base ` D ) | A. b e. ( Base ` D ) E! h h e. ( b ( Hom ` D ) a ) } )
45 34 37 44 3eqtr4d 
 |-  ( ( ( ph /\ ( C e. _V /\ D e. _V ) ) /\ C e. Cat ) -> ( TermO ` C ) = ( TermO ` D ) )
46 41 pm5.32i 
 |-  ( ( ( ph /\ ( C e. _V /\ D e. _V ) ) /\ C e. Cat ) <-> ( ( ph /\ ( C e. _V /\ D e. _V ) ) /\ D e. Cat ) )
47 46 45 sylbir 
 |-  ( ( ( ph /\ ( C e. _V /\ D e. _V ) ) /\ D e. Cat ) -> ( TermO ` C ) = ( TermO ` D ) )
48 termofn 
 |-  TermO Fn Cat
49 48 fndmi 
 |-  dom TermO = Cat
50 49 eleq2i 
 |-  ( C e. dom TermO <-> C e. Cat )
51 ndmfv 
 |-  ( -. C e. dom TermO -> ( TermO ` C ) = (/) )
52 50 51 sylnbir 
 |-  ( -. C e. Cat -> ( TermO ` C ) = (/) )
53 52 ad2antrl 
 |-  ( ( ( ph /\ ( C e. _V /\ D e. _V ) ) /\ ( -. C e. Cat /\ -. D e. Cat ) ) -> ( TermO ` C ) = (/) )
54 49 eleq2i 
 |-  ( D e. dom TermO <-> D e. Cat )
55 ndmfv 
 |-  ( -. D e. dom TermO -> ( TermO ` D ) = (/) )
56 54 55 sylnbir 
 |-  ( -. D e. Cat -> ( TermO ` D ) = (/) )
57 56 ad2antll 
 |-  ( ( ( ph /\ ( C e. _V /\ D e. _V ) ) /\ ( -. C e. Cat /\ -. D e. Cat ) ) -> ( TermO ` D ) = (/) )
58 53 57 eqtr4d 
 |-  ( ( ( ph /\ ( C e. _V /\ D e. _V ) ) /\ ( -. C e. Cat /\ -. D e. Cat ) ) -> ( TermO ` C ) = ( TermO ` D ) )
59 45 47 58 pm2.61ddan 
 |-  ( ( ph /\ ( C e. _V /\ D e. _V ) ) -> ( TermO ` C ) = ( TermO ` D ) )
60 6 13 59 pm2.61dda 
 |-  ( ph -> ( TermO ` C ) = ( TermO ` D ) )