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

Metamath Proof Explorer

Theorem initopropd

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

Ref Expression
Hypotheses initopropd.1 
|- ( ph -> ( Homf ` C ) = ( Homf ` D ) )
initopropd.2 
|- ( ph -> ( comf ` C ) = ( comf ` D ) )
Assertion initopropd 
|- ( ph -> ( InitO ` C ) = ( InitO ` 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 initopropdlem 
 |-  ( ( ph /\ -. C e. _V ) -> ( InitO ` C ) = ( InitO ` 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 initopropdlem 
 |-  ( ( ph /\ -. D e. _V ) -> ( InitO ` D ) = ( InitO ` C ) )
13 12 eqcomd 
 |-  ( ( ph /\ -. D e. _V ) -> ( InitO ` C ) = ( InitO ` 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. a e. ( Base ` C ) A. b e. ( Base ` C ) ( a ( Hom ` C ) b ) = ( a ( Hom ` D ) b ) ) )
21 15 20 mpbid 
 |-  ( ( ( ph /\ ( C e. _V /\ D e. _V ) ) /\ C e. Cat ) -> A. a e. ( Base ` C ) A. b e. ( Base ` C ) ( a ( Hom ` C ) b ) = ( a ( Hom ` D ) b ) )
22 21 r19.21bi 
 |-  ( ( ( ( ph /\ ( C e. _V /\ D e. _V ) ) /\ C e. Cat ) /\ a e. ( Base ` C ) ) -> A. b e. ( Base ` C ) ( a ( Hom ` C ) b ) = ( a ( Hom ` D ) b ) )
23 22 r19.21bi 
 |-  ( ( ( ( ( ph /\ ( C e. _V /\ D e. _V ) ) /\ C e. Cat ) /\ a e. ( Base ` C ) ) /\ b e. ( Base ` C ) ) -> ( a ( Hom ` C ) b ) = ( a ( Hom ` D ) b ) )
24 23 eleq2d 
 |-  ( ( ( ( ( ph /\ ( C e. _V /\ D e. _V ) ) /\ C e. Cat ) /\ a e. ( Base ` C ) ) /\ b e. ( Base ` C ) ) -> ( h e. ( a ( Hom ` C ) b ) <-> h e. ( a ( Hom ` D ) b ) ) )
25 24 eubidv 
 |-  ( ( ( ( ( ph /\ ( C e. _V /\ D e. _V ) ) /\ C e. Cat ) /\ a e. ( Base ` C ) ) /\ b e. ( Base ` C ) ) -> ( E! h h e. ( a ( Hom ` C ) b ) <-> E! h h e. ( a ( Hom ` D ) b ) ) )
26 25 ralbidva 
 |-  ( ( ( ( ph /\ ( C e. _V /\ D e. _V ) ) /\ C e. Cat ) /\ a e. ( Base ` C ) ) -> ( A. b e. ( Base ` C ) E! h h e. ( a ( Hom ` C ) b ) <-> A. b e. ( Base ` C ) E! h h e. ( a ( Hom ` D ) b ) ) )
27 26 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. ( a ( Hom ` C ) b ) ) <-> ( a e. ( Base ` C ) /\ A. b e. ( Base ` C ) E! h h e. ( a ( Hom ` D ) b ) ) ) )
28 19 eleq2d 
 |-  ( ( ( ph /\ ( C e. _V /\ D e. _V ) ) /\ C e. Cat ) -> ( a e. ( Base ` C ) <-> a e. ( Base ` D ) ) )
29 19 raleqdv 
 |-  ( ( ( ph /\ ( C e. _V /\ D e. _V ) ) /\ C e. Cat ) -> ( A. b e. ( Base ` C ) E! h h e. ( a ( Hom ` D ) b ) <-> A. b e. ( Base ` D ) E! h h e. ( a ( Hom ` D ) b ) ) )
30 28 29 anbi12d 
 |-  ( ( ( ph /\ ( C e. _V /\ D e. _V ) ) /\ C e. Cat ) -> ( ( a e. ( Base ` C ) /\ A. b e. ( Base ` C ) E! h h e. ( a ( Hom ` D ) b ) ) <-> ( a e. ( Base ` D ) /\ A. b e. ( Base ` D ) E! h h e. ( a ( Hom ` D ) b ) ) ) )
31 27 30 bitrd 
 |-  ( ( ( ph /\ ( C e. _V /\ D e. _V ) ) /\ C e. Cat ) -> ( ( a e. ( Base ` C ) /\ A. b e. ( Base ` C ) E! h h e. ( a ( Hom ` C ) b ) ) <-> ( a e. ( Base ` D ) /\ A. b e. ( Base ` D ) E! h h e. ( a ( Hom ` D ) b ) ) ) )
32 31 rabbidva2 
 |-  ( ( ( ph /\ ( C e. _V /\ D e. _V ) ) /\ C e. Cat ) -> { a e. ( Base ` C ) | A. b e. ( Base ` C ) E! h h e. ( a ( Hom ` C ) b ) } = { a e. ( Base ` D ) | A. b e. ( Base ` D ) E! h h e. ( a ( Hom ` D ) b ) } )
33 simpr 
 |-  ( ( ( ph /\ ( C e. _V /\ D e. _V ) ) /\ C e. Cat ) -> C e. Cat )
34 eqid 
 |-  ( Base ` C ) = ( Base ` C )
35 33 34 16 initoval 
 |-  ( ( ( ph /\ ( C e. _V /\ D e. _V ) ) /\ C e. Cat ) -> ( InitO ` C ) = { a e. ( Base ` C ) | A. b e. ( Base ` C ) E! h h e. ( a ( Hom ` C ) b ) } )
36 2 adantr 
 |-  ( ( ph /\ ( C e. _V /\ D e. _V ) ) -> ( comf ` C ) = ( comf ` D ) )
37 simprl 
 |-  ( ( ph /\ ( C e. _V /\ D e. _V ) ) -> C e. _V )
38 simprr 
 |-  ( ( ph /\ ( C e. _V /\ D e. _V ) ) -> D e. _V )
39 14 36 37 38 catpropd 
 |-  ( ( ph /\ ( C e. _V /\ D e. _V ) ) -> ( C e. Cat <-> D e. Cat ) )
40 39 biimpa 
 |-  ( ( ( ph /\ ( C e. _V /\ D e. _V ) ) /\ C e. Cat ) -> D e. Cat )
41 eqid 
 |-  ( Base ` D ) = ( Base ` D )
42 40 41 17 initoval 
 |-  ( ( ( ph /\ ( C e. _V /\ D e. _V ) ) /\ C e. Cat ) -> ( InitO ` D ) = { a e. ( Base ` D ) | A. b e. ( Base ` D ) E! h h e. ( a ( Hom ` D ) b ) } )
43 32 35 42 3eqtr4d 
 |-  ( ( ( ph /\ ( C e. _V /\ D e. _V ) ) /\ C e. Cat ) -> ( InitO ` C ) = ( InitO ` D ) )
44 39 pm5.32i 
 |-  ( ( ( ph /\ ( C e. _V /\ D e. _V ) ) /\ C e. Cat ) <-> ( ( ph /\ ( C e. _V /\ D e. _V ) ) /\ D e. Cat ) )
45 44 43 sylbir 
 |-  ( ( ( ph /\ ( C e. _V /\ D e. _V ) ) /\ D e. Cat ) -> ( InitO ` C ) = ( InitO ` D ) )
46 initofn 
 |-  InitO Fn Cat
47 46 fndmi 
 |-  dom InitO = Cat
48 47 eleq2i 
 |-  ( C e. dom InitO <-> C e. Cat )
49 ndmfv 
 |-  ( -. C e. dom InitO -> ( InitO ` C ) = (/) )
50 48 49 sylnbir 
 |-  ( -. C e. Cat -> ( InitO ` C ) = (/) )
51 50 ad2antrl 
 |-  ( ( ( ph /\ ( C e. _V /\ D e. _V ) ) /\ ( -. C e. Cat /\ -. D e. Cat ) ) -> ( InitO ` C ) = (/) )
52 47 eleq2i 
 |-  ( D e. dom InitO <-> D e. Cat )
53 ndmfv 
 |-  ( -. D e. dom InitO -> ( InitO ` D ) = (/) )
54 52 53 sylnbir 
 |-  ( -. D e. Cat -> ( InitO ` D ) = (/) )
55 54 ad2antll 
 |-  ( ( ( ph /\ ( C e. _V /\ D e. _V ) ) /\ ( -. C e. Cat /\ -. D e. Cat ) ) -> ( InitO ` D ) = (/) )
56 51 55 eqtr4d 
 |-  ( ( ( ph /\ ( C e. _V /\ D e. _V ) ) /\ ( -. C e. Cat /\ -. D e. Cat ) ) -> ( InitO ` C ) = ( InitO ` D ) )
57 43 45 56 pm2.61ddan 
 |-  ( ( ph /\ ( C e. _V /\ D e. _V ) ) -> ( InitO ` C ) = ( InitO ` D ) )
58 6 13 57 pm2.61dda 
 |-  ( ph -> ( InitO ` C ) = ( InitO ` D ) )