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 ) )