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

Metamath Proof Explorer

Theorem oppcthinendcALT

Description: Alternate proof of oppcthinendc . (Contributed by Zhi Wang, 16-Oct-2025) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses oppcthinco.o 
|- O = ( oppCat ` C )
oppcthinco.c 
|- ( ph -> C e. ThinCat )
oppcthinendc.b 
|- B = ( Base ` C )
oppcthinendc.h 
|- H = ( Hom ` C )
oppcthinendc.1 
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x =/= y -> ( x H y ) = (/) ) )
Assertion oppcthinendcALT 
|- ( ph -> ( comf ` C ) = ( comf ` O ) )

Proof

Step Hyp Ref Expression
1 oppcthinco.o 
 |-  O = ( oppCat ` C )
2 oppcthinco.c 
 |-  ( ph -> C e. ThinCat )
3 oppcthinendc.b 
 |-  B = ( Base ` C )
4 oppcthinendc.h 
 |-  H = ( Hom ` C )
5 oppcthinendc.1 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x =/= y -> ( x H y ) = (/) ) )
6 eqid 
 |-  ( comp ` C ) = ( comp ` C )
7 simplr1 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) -> x e. B )
8 simplr2 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) -> y e. B )
9 simplr3 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) -> z e. B )
10 3 6 1 7 8 9 oppcco 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) -> ( g ( <. x , y >. ( comp ` O ) z ) f ) = ( f ( <. z , y >. ( comp ` C ) x ) g ) )
11 simpll 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) -> ph )
12 7 8 jca 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) -> ( x e. B /\ y e. B ) )
13 simprl 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) -> f e. ( x H y ) )
14 13 ne0d 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) -> ( x H y ) =/= (/) )
15 5 necon1d 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( ( x H y ) =/= (/) -> x = y ) )
16 15 imp 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( x H y ) =/= (/) ) -> x = y )
17 11 12 14 16 syl21anc 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) -> x = y )
18 simprr 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) -> g e. ( y H z ) )
19 18 ne0d 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) -> ( y H z ) =/= (/) )
20 neeq1 
 |-  ( x = y -> ( x =/= z <-> y =/= z ) )
21 oveq1 
 |-  ( x = y -> ( x H z ) = ( y H z ) )
22 21 eqeq1d 
 |-  ( x = y -> ( ( x H z ) = (/) <-> ( y H z ) = (/) ) )
23 20 22 imbi12d 
 |-  ( x = y -> ( ( x =/= z -> ( x H z ) = (/) ) <-> ( y =/= z -> ( y H z ) = (/) ) ) )
24 neeq2 
 |-  ( y = z -> ( x =/= y <-> x =/= z ) )
25 oveq2 
 |-  ( y = z -> ( x H y ) = ( x H z ) )
26 25 eqeq1d 
 |-  ( y = z -> ( ( x H y ) = (/) <-> ( x H z ) = (/) ) )
27 24 26 imbi12d 
 |-  ( y = z -> ( ( x =/= y -> ( x H y ) = (/) ) <-> ( x =/= z -> ( x H z ) = (/) ) ) )
28 5 anassrs 
 |-  ( ( ( ph /\ x e. B ) /\ y e. B ) -> ( x =/= y -> ( x H y ) = (/) ) )
29 28 ralrimiva 
 |-  ( ( ph /\ x e. B ) -> A. y e. B ( x =/= y -> ( x H y ) = (/) ) )
30 29 adantlr 
 |-  ( ( ( ph /\ z e. B ) /\ x e. B ) -> A. y e. B ( x =/= y -> ( x H y ) = (/) ) )
31 simplr 
 |-  ( ( ( ph /\ z e. B ) /\ x e. B ) -> z e. B )
32 27 30 31 rspcdva 
 |-  ( ( ( ph /\ z e. B ) /\ x e. B ) -> ( x =/= z -> ( x H z ) = (/) ) )
33 32 ralrimiva 
 |-  ( ( ph /\ z e. B ) -> A. x e. B ( x =/= z -> ( x H z ) = (/) ) )
34 11 9 33 syl2anc 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) -> A. x e. B ( x =/= z -> ( x H z ) = (/) ) )
35 23 34 8 rspcdva 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) -> ( y =/= z -> ( y H z ) = (/) ) )
36 35 necon1d 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) -> ( ( y H z ) =/= (/) -> y = z ) )
37 19 36 mpd 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) -> y = z )
38 17 37 eqtrd 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) -> x = z )
39 38 equcomd 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) -> z = x )
40 39 opeq1d 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) -> <. z , y >. = <. x , y >. )
41 40 38 oveq12d 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) -> ( <. z , y >. ( comp ` C ) x ) = ( <. x , y >. ( comp ` C ) z ) )
42 17 oveq1d 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) -> ( x H y ) = ( y H y ) )
43 13 42 eleqtrd 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) -> f e. ( y H y ) )
44 37 oveq2d 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) -> ( y H y ) = ( y H z ) )
45 18 44 eleqtrrd 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) -> g e. ( y H y ) )
46 11 2 syl 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) -> C e. ThinCat )
47 8 8 43 45 3 4 46 thincmo2 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) -> f = g )
48 47 equcomd 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) -> g = f )
49 41 47 48 oveq123d 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) -> ( f ( <. z , y >. ( comp ` C ) x ) g ) = ( g ( <. x , y >. ( comp ` C ) z ) f ) )
50 10 49 eqtr2d 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) -> ( g ( <. x , y >. ( comp ` C ) z ) f ) = ( g ( <. x , y >. ( comp ` O ) z ) f ) )
51 50 ralrimivva 
 |-  ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) -> A. f e. ( x H y ) A. g e. ( y H z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) = ( g ( <. x , y >. ( comp ` O ) z ) f ) )
52 51 ralrimivvva 
 |-  ( ph -> A. x e. B A. y e. B A. z e. B A. f e. ( x H y ) A. g e. ( y H z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) = ( g ( <. x , y >. ( comp ` O ) z ) f ) )
53 eqid 
 |-  ( comp ` O ) = ( comp ` O )
54 3 a1i 
 |-  ( ph -> B = ( Base ` C ) )
55 1 3 oppcbas 
 |-  B = ( Base ` O )
56 55 a1i 
 |-  ( ph -> B = ( Base ` O ) )
57 1 3 4 5 oppcendc 
 |-  ( ph -> ( Homf ` C ) = ( Homf ` O ) )
58 6 53 4 54 56 57 comfeq 
 |-  ( ph -> ( ( comf ` C ) = ( comf ` O ) <-> A. x e. B A. y e. B A. z e. B A. f e. ( x H y ) A. g e. ( y H z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) = ( g ( <. x , y >. ( comp ` O ) z ) f ) ) )
59 52 58 mpbird 
 |-  ( ph -> ( comf ` C ) = ( comf ` O ) )