oppccofval

Description: Composition in the opposite category. (Contributed by Mario Carneiro, 2-Jan-2017)

	Ref	Expression
Hypotheses	oppcco.b	$⊢ B = {Base}_{C}$
	oppcco.c	$⊢ \underset{˙}{\cdot} = comp (C)$
	oppcco.o	$⊢ O = oppCat (C)$
	oppcco.x	$⊢ φ \to X \in B$
	oppcco.y	$⊢ φ \to Y \in B$
	oppcco.z	$⊢ φ \to Z \in B$
Assertion	oppccofval	$⊢ φ \to ⟨X, Y⟩ comp (O) Z = tpos (⟨Z, Y⟩ \underset{˙}{\cdot} X)$

Proof

Step	Hyp	Ref	Expression
1		oppcco.b	$⊢ B = {Base}_{C}$
2		oppcco.c	$⊢ \underset{˙}{\cdot} = comp (C)$
3		oppcco.o	$⊢ O = oppCat (C)$
4		oppcco.x	$⊢ φ \to X \in B$
5		oppcco.y	$⊢ φ \to Y \in B$
6		oppcco.z	$⊢ φ \to Z \in B$
7		elfvex	$⊢ X \in {Base}_{C} \to C \in V$
8	7 1	eleq2s	$⊢ X \in B \to C \in V$
9		eqid	$⊢ Hom (C) = Hom (C)$
10	1 9 2 3	oppcval	$⊢ C \in V \to O = (C sSet ⟨Hom (ndx), tpos Hom (C)⟩) sSet ⟨comp (ndx), (u \in (B \times B), z \in B ⟼ tpos (⟨z, 2^{nd} (u)⟩ \underset{˙}{\cdot} 1^{st} (u)))⟩$
11	4 8 10	3syl	$⊢ φ \to O = (C sSet ⟨Hom (ndx), tpos Hom (C)⟩) sSet ⟨comp (ndx), (u \in (B \times B), z \in B ⟼ tpos (⟨z, 2^{nd} (u)⟩ \underset{˙}{\cdot} 1^{st} (u)))⟩$
12	11	fveq2d	$⊢ φ \to comp (O) = comp ((C sSet ⟨Hom (ndx), tpos Hom (C)⟩) sSet ⟨comp (ndx), (u \in (B \times B), z \in B ⟼ tpos (⟨z, 2^{nd} (u)⟩ \underset{˙}{\cdot} 1^{st} (u)))⟩)$
13		ovex	$⊢ C sSet ⟨Hom (ndx), tpos Hom (C)⟩ \in V$
14	1	fvexi	$⊢ B \in V$
15	14 14	xpex	$⊢ B \times B \in V$
16	15 14	mpoex	$⊢ (u \in (B \times B), z \in B ⟼ tpos (⟨z, 2^{nd} (u)⟩ \underset{˙}{\cdot} 1^{st} (u))) \in V$
17		ccoid	$⊢ comp = Slot comp (ndx)$
18	17	setsid	$⊢ (C sSet ⟨Hom (ndx), tpos Hom (C)⟩ \in V \land (u \in (B \times B), z \in B ⟼ tpos (⟨z, 2^{nd} (u)⟩ \underset{˙}{\cdot} 1^{st} (u))) \in V) \to (u \in (B \times B), z \in B ⟼ tpos (⟨z, 2^{nd} (u)⟩ \underset{˙}{\cdot} 1^{st} (u))) = comp ((C sSet ⟨Hom (ndx), tpos Hom (C)⟩) sSet ⟨comp (ndx), (u \in (B \times B), z \in B ⟼ tpos (⟨z, 2^{nd} (u)⟩ \underset{˙}{\cdot} 1^{st} (u)))⟩)$
19	13 16 18	mp2an	$⊢ (u \in (B \times B), z \in B ⟼ tpos (⟨z, 2^{nd} (u)⟩ \underset{˙}{\cdot} 1^{st} (u))) = comp ((C sSet ⟨Hom (ndx), tpos Hom (C)⟩) sSet ⟨comp (ndx), (u \in (B \times B), z \in B ⟼ tpos (⟨z, 2^{nd} (u)⟩ \underset{˙}{\cdot} 1^{st} (u)))⟩)$
20	12 19	eqtr4di	$⊢ φ \to comp (O) = (u \in (B \times B), z \in B ⟼ tpos (⟨z, 2^{nd} (u)⟩ \underset{˙}{\cdot} 1^{st} (u)))$
21		simprr	$⊢ (φ \land (u = ⟨X, Y⟩ \land z = Z)) \to z = Z$
22		simprl	$⊢ (φ \land (u = ⟨X, Y⟩ \land z = Z)) \to u = ⟨X, Y⟩$
23	22	fveq2d	$⊢ (φ \land (u = ⟨X, Y⟩ \land z = Z)) \to 2^{nd} (u) = 2^{nd} (⟨X, Y⟩)$
24	5	adantr	$⊢ (φ \land (u = ⟨X, Y⟩ \land z = Z)) \to Y \in B$
25		op2ndg	$⊢ (X \in B \land Y \in B) \to 2^{nd} (⟨X, Y⟩) = Y$
26	4 24 25	syl2an2r	$⊢ (φ \land (u = ⟨X, Y⟩ \land z = Z)) \to 2^{nd} (⟨X, Y⟩) = Y$
27	23 26	eqtrd	$⊢ (φ \land (u = ⟨X, Y⟩ \land z = Z)) \to 2^{nd} (u) = Y$
28	21 27	opeq12d	$⊢ (φ \land (u = ⟨X, Y⟩ \land z = Z)) \to ⟨z, 2^{nd} (u)⟩ = ⟨Z, Y⟩$
29	22	fveq2d	$⊢ (φ \land (u = ⟨X, Y⟩ \land z = Z)) \to 1^{st} (u) = 1^{st} (⟨X, Y⟩)$
30		op1stg	$⊢ (X \in B \land Y \in B) \to 1^{st} (⟨X, Y⟩) = X$
31	4 24 30	syl2an2r	$⊢ (φ \land (u = ⟨X, Y⟩ \land z = Z)) \to 1^{st} (⟨X, Y⟩) = X$
32	29 31	eqtrd	$⊢ (φ \land (u = ⟨X, Y⟩ \land z = Z)) \to 1^{st} (u) = X$
33	28 32	oveq12d	$⊢ (φ \land (u = ⟨X, Y⟩ \land z = Z)) \to ⟨z, 2^{nd} (u)⟩ \underset{˙}{\cdot} 1^{st} (u) = ⟨Z, Y⟩ \underset{˙}{\cdot} X$
34	33	tposeqd	$⊢ (φ \land (u = ⟨X, Y⟩ \land z = Z)) \to tpos (⟨z, 2^{nd} (u)⟩ \underset{˙}{\cdot} 1^{st} (u)) = tpos (⟨Z, Y⟩ \underset{˙}{\cdot} X)$
35	4 5	opelxpd	$⊢ φ \to ⟨X, Y⟩ \in (B \times B)$
36		ovex	$⊢ ⟨Z, Y⟩ \underset{˙}{\cdot} X \in V$
37	36	tposex	$⊢ tpos (⟨Z, Y⟩ \underset{˙}{\cdot} X) \in V$
38	37	a1i	$⊢ φ \to tpos (⟨Z, Y⟩ \underset{˙}{\cdot} X) \in V$
39	20 34 35 6 38	ovmpod	$⊢ φ \to ⟨X, Y⟩ comp (O) Z = tpos (⟨Z, Y⟩ \underset{˙}{\cdot} X)$

Metamath Proof Explorer

Theorem oppccofval

Proof