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 ⊢ 𝑂 = ( oppCat ‘ 𝐶 )
oppcthinco.c ⊢ ( 𝜑 → 𝐶 ∈ ThinCat )
oppcthinendc.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
oppcthinendc.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
oppcthinendc.1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ≠ 𝑦 → ( 𝑥 𝐻 𝑦 ) = ∅ ) )
Assertion oppcthinendcALT ( 𝜑 → ( compf ‘ 𝐶 ) = ( compf ‘ 𝑂 ) )

Proof

Step Hyp Ref Expression
1 oppcthinco.o ⊢ 𝑂 = ( oppCat ‘ 𝐶 )
2 oppcthinco.c ⊢ ( 𝜑 → 𝐶 ∈ ThinCat )
3 oppcthinendc.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
4 oppcthinendc.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
5 oppcthinendc.1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ≠ 𝑦 → ( 𝑥 𝐻 𝑦 ) = ∅ ) )
6 eqid ⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
7 simplr1 ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → 𝑥 ∈ 𝐵 )
8 simplr2 ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → 𝑦 ∈ 𝐵 )
9 simplr3 ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → 𝑧 ∈ 𝐵 )
10 3 6 1 7 8 9 oppcco ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑂 ) 𝑧 ) 𝑓 ) = ( 𝑓 ( ⟨ 𝑧 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑔 ) )
11 simpll ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → 𝜑 )
12 7 8 jca ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) )
13 simprl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) )
14 13 ne0d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → ( 𝑥 𝐻 𝑦 ) ≠ ∅ )
15 5 necon1d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝑥 𝐻 𝑦 ) ≠ ∅ → 𝑥 = 𝑦 ) )
16 15 imp ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( 𝑥 𝐻 𝑦 ) ≠ ∅ ) → 𝑥 = 𝑦 )
17 11 12 14 16 syl21anc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → 𝑥 = 𝑦 )
18 simprr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) )
19 18 ne0d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → ( 𝑦 𝐻 𝑧 ) ≠ ∅ )
20 neeq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ≠ 𝑧 ↔ 𝑦 ≠ 𝑧 ) )
21 oveq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 𝐻 𝑧 ) = ( 𝑦 𝐻 𝑧 ) )
22 21 eqeq1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 𝐻 𝑧 ) = ∅ ↔ ( 𝑦 𝐻 𝑧 ) = ∅ ) )
23 20 22 imbi12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ≠ 𝑧 → ( 𝑥 𝐻 𝑧 ) = ∅ ) ↔ ( 𝑦 ≠ 𝑧 → ( 𝑦 𝐻 𝑧 ) = ∅ ) ) )
24 neeq2 ⊢ ( 𝑦 = 𝑧 → ( 𝑥 ≠ 𝑦 ↔ 𝑥 ≠ 𝑧 ) )
25 oveq2 ⊢ ( 𝑦 = 𝑧 → ( 𝑥 𝐻 𝑦 ) = ( 𝑥 𝐻 𝑧 ) )
26 25 eqeq1d ⊢ ( 𝑦 = 𝑧 → ( ( 𝑥 𝐻 𝑦 ) = ∅ ↔ ( 𝑥 𝐻 𝑧 ) = ∅ ) )
27 24 26 imbi12d ⊢ ( 𝑦 = 𝑧 → ( ( 𝑥 ≠ 𝑦 → ( 𝑥 𝐻 𝑦 ) = ∅ ) ↔ ( 𝑥 ≠ 𝑧 → ( 𝑥 𝐻 𝑧 ) = ∅ ) ) )
28 5 anassrs ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ≠ 𝑦 → ( 𝑥 𝐻 𝑦 ) = ∅ ) )
29 28 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≠ 𝑦 → ( 𝑥 𝐻 𝑦 ) = ∅ ) )
30 29 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≠ 𝑦 → ( 𝑥 𝐻 𝑦 ) = ∅ ) )
31 simplr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → 𝑧 ∈ 𝐵 )
32 27 30 31 rspcdva ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ≠ 𝑧 → ( 𝑥 𝐻 𝑧 ) = ∅ ) )
33 32 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → ∀ 𝑥 ∈ 𝐵 ( 𝑥 ≠ 𝑧 → ( 𝑥 𝐻 𝑧 ) = ∅ ) )
34 11 9 33 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → ∀ 𝑥 ∈ 𝐵 ( 𝑥 ≠ 𝑧 → ( 𝑥 𝐻 𝑧 ) = ∅ ) )
35 23 34 8 rspcdva ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → ( 𝑦 ≠ 𝑧 → ( 𝑦 𝐻 𝑧 ) = ∅ ) )
36 35 necon1d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → ( ( 𝑦 𝐻 𝑧 ) ≠ ∅ → 𝑦 = 𝑧 ) )
37 19 36 mpd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → 𝑦 = 𝑧 )
38 17 37 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → 𝑥 = 𝑧 )
39 38 equcomd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → 𝑧 = 𝑥 )
40 39 opeq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → ⟨ 𝑧 , 𝑦 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ )
41 40 38 oveq12d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → ( ⟨ 𝑧 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) = ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) )
42 17 oveq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → ( 𝑥 𝐻 𝑦 ) = ( 𝑦 𝐻 𝑦 ) )
43 13 42 eleqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → 𝑓 ∈ ( 𝑦 𝐻 𝑦 ) )
44 37 oveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → ( 𝑦 𝐻 𝑦 ) = ( 𝑦 𝐻 𝑧 ) )
45 18 44 eleqtrrd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → 𝑔 ∈ ( 𝑦 𝐻 𝑦 ) )
46 11 2 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → 𝐶 ∈ ThinCat )
47 8 8 43 45 3 4 46 thincmo2 ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → 𝑓 = 𝑔 )
48 47 equcomd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → 𝑔 = 𝑓 )
49 41 47 48 oveq123d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → ( 𝑓 ( ⟨ 𝑧 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑔 ) = ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) )
50 10 49 eqtr2d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑂 ) 𝑧 ) 𝑓 ) )
51 50 ralrimivva ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑂 ) 𝑧 ) 𝑓 ) )
52 51 ralrimivvva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑂 ) 𝑧 ) 𝑓 ) )
53 eqid ⊢ ( comp ‘ 𝑂 ) = ( comp ‘ 𝑂 )
54 3 a1i ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐶 ) )
55 1 3 oppcbas ⊢ 𝐵 = ( Base ‘ 𝑂 )
56 55 a1i ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑂 ) )
57 1 3 4 5 oppcendc ⊢ ( 𝜑 → ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝑂 ) )
58 6 53 4 54 56 57 comfeq ⊢ ( 𝜑 → ( ( compf ‘ 𝐶 ) = ( compf ‘ 𝑂 ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑂 ) 𝑧 ) 𝑓 ) ) )
59 52 58 mpbird ⊢ ( 𝜑 → ( compf ‘ 𝐶 ) = ( compf ‘ 𝑂 ) )