oppcval

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

	Ref	Expression
Hypotheses	oppcval.b	$⊢ B = {Base}_{C}$
	oppcval.h	$⊢ H = Hom (C)$
	oppcval.x	$⊢ \underset{˙}{\cdot} = comp (C)$
	oppcval.o	$⊢ O = oppCat (C)$
Assertion	oppcval	$⊢ C \in V \to O = (C sSet ⟨Hom (ndx), tpos H⟩) sSet ⟨comp (ndx), (u \in (B \times B), z \in B ⟼ tpos (⟨z, 2^{nd} (u)⟩ \underset{˙}{\cdot} 1^{st} (u)))⟩$

Proof

Step	Hyp	Ref	Expression
1		oppcval.b	$⊢ B = {Base}_{C}$
2		oppcval.h	$⊢ H = Hom (C)$
3		oppcval.x	$⊢ \underset{˙}{\cdot} = comp (C)$
4		oppcval.o	$⊢ O = oppCat (C)$
5		elex	$⊢ C \in V \to C \in V$
6		id	$⊢ c = C \to c = C$
7		fveq2	$⊢ c = C \to Hom (c) = Hom (C)$
8	7 2	syl6eqr	$⊢ c = C \to Hom (c) = H$
9	8	tposeqd	$⊢ c = C \to tpos Hom (c) = tpos H$
10	9	opeq2d	$⊢ c = C \to ⟨Hom (ndx), tpos Hom (c)⟩ = ⟨Hom (ndx), tpos H⟩$
11	6 10	oveq12d	$⊢ c = C \to c sSet ⟨Hom (ndx), tpos Hom (c)⟩ = C sSet ⟨Hom (ndx), tpos H⟩$
12		fveq2	$⊢ c = C \to {Base}_{c} = {Base}_{C}$
13	12 1	syl6eqr	$⊢ c = C \to {Base}_{c} = B$
14	13	sqxpeqd	$⊢ c = C \to {Base}_{c} \times {Base}_{c} = B \times B$
15		fveq2	$⊢ c = C \to comp (c) = comp (C)$
16	15 3	syl6eqr	$⊢ c = C \to comp (c) = \underset{˙}{\cdot}$
17	16	oveqd	$⊢ c = C \to ⟨z, 2^{nd} (u)⟩ comp (c) 1^{st} (u) = ⟨z, 2^{nd} (u)⟩ \underset{˙}{\cdot} 1^{st} (u)$
18	17	tposeqd	$⊢ c = C \to tpos (⟨z, 2^{nd} (u)⟩ comp (c) 1^{st} (u)) = tpos (⟨z, 2^{nd} (u)⟩ \underset{˙}{\cdot} 1^{st} (u))$
19	14 13 18	mpoeq123dv	$⊢ c = C \to (u \in ({Base}_{c} \times {Base}_{c}), z \in {Base}_{c} ⟼ tpos (⟨z, 2^{nd} (u)⟩ comp (c) 1^{st} (u))) = (u \in (B \times B), z \in B ⟼ tpos (⟨z, 2^{nd} (u)⟩ \underset{˙}{\cdot} 1^{st} (u)))$
20	19	opeq2d	$⊢ c = C \to ⟨comp (ndx), (u \in ({Base}_{c} \times {Base}_{c}), z \in {Base}_{c} ⟼ tpos (⟨z, 2^{nd} (u)⟩ comp (c) 1^{st} (u)))⟩ = ⟨comp (ndx), (u \in (B \times B), z \in B ⟼ tpos (⟨z, 2^{nd} (u)⟩ \underset{˙}{\cdot} 1^{st} (u)))⟩$
21	11 20	oveq12d	$⊢ c = C \to (c sSet ⟨Hom (ndx), tpos Hom (c)⟩) sSet ⟨comp (ndx), (u \in ({Base}_{c} \times {Base}_{c}), z \in {Base}_{c} ⟼ tpos (⟨z, 2^{nd} (u)⟩ comp (c) 1^{st} (u)))⟩ = (C sSet ⟨Hom (ndx), tpos H⟩) sSet ⟨comp (ndx), (u \in (B \times B), z \in B ⟼ tpos (⟨z, 2^{nd} (u)⟩ \underset{˙}{\cdot} 1^{st} (u)))⟩$
22		df-oppc	$⊢ oppCat = (c \in V ⟼ (c sSet ⟨Hom (ndx), tpos Hom (c)⟩) sSet ⟨comp (ndx), (u \in ({Base}_{c} \times {Base}_{c}), z \in {Base}_{c} ⟼ tpos (⟨z, 2^{nd} (u)⟩ comp (c) 1^{st} (u)))⟩)$
23		ovex	$⊢ (C sSet ⟨Hom (ndx), tpos H⟩) sSet ⟨comp (ndx), (u \in (B \times B), z \in B ⟼ tpos (⟨z, 2^{nd} (u)⟩ \underset{˙}{\cdot} 1^{st} (u)))⟩ \in V$
24	21 22 23	fvmpt	$⊢ C \in V \to oppCat (C) = (C sSet ⟨Hom (ndx), tpos H⟩) sSet ⟨comp (ndx), (u \in (B \times B), z \in B ⟼ tpos (⟨z, 2^{nd} (u)⟩ \underset{˙}{\cdot} 1^{st} (u)))⟩$
25	5 24	syl	$⊢ C \in V \to oppCat (C) = (C sSet ⟨Hom (ndx), tpos H⟩) sSet ⟨comp (ndx), (u \in (B \times B), z \in B ⟼ tpos (⟨z, 2^{nd} (u)⟩ \underset{˙}{\cdot} 1^{st} (u)))⟩$
26	4 25	syl5eq	$⊢ C \in V \to O = (C sSet ⟨Hom (ndx), tpos H⟩) sSet ⟨comp (ndx), (u \in (B \times B), z \in B ⟼ tpos (⟨z, 2^{nd} (u)⟩ \underset{˙}{\cdot} 1^{st} (u)))⟩$

Metamath Proof Explorer

Theorem oppcval

Proof