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

Metamath Proof Explorer

Theorem 2oppcbas

Description: The double opposite category has the same objects as the original category. Intended for use with property lemmas such as monpropd . (Contributed by Mario Carneiro, 3-Jan-2017)

	Ref	Expression
Hypotheses	oppcbas.1	$⊢ O = oppCat (C)$
	2oppcco.2	$⊢ B = {Base}_{C}$
Assertion	2oppcbas	$⊢ B = {Base}_{oppCat (O)}$

Proof

Step	Hyp	Ref	Expression
1		oppcbas.1	$⊢ O = oppCat (C)$
2		2oppcco.2	$⊢ B = {Base}_{C}$
3		eqid	$⊢ oppCat (O) = oppCat (O)$
4	1 2	oppcbas	$⊢ B = {Base}_{O}$
5	3 4	oppcbas	$⊢ B = {Base}_{oppCat (O)}$