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	$⊢ φ \to C \in ThinCat$
	oppcthinendc.b	$⊢ B = {Base}_{C}$
	oppcthinendc.h	$⊢ H = Hom (C)$
	oppcthinendc.1	$⊢ (φ \land (x \in B \land y \in B)) \to (x \neq y \to x H y = \emptyset)$
Assertion	oppcthinendcALT	$⊢ φ \to {comp}_{𝑓} (C) = {comp}_{𝑓} (O)$

Proof

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

Metamath Proof Explorer

Theorem oppcthinendcALT

Proof