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	⊢ 𝑂 = ( oppCat ‘ 𝐶 )
	2oppcco.2	⊢ 𝐵 = ( Base ‘ 𝐶 )
Assertion	2oppcbas	⊢ 𝐵 = ( Base ‘ ( oppCat ‘ 𝑂 ) )

Proof

Step	Hyp	Ref	Expression
1		oppcbas.1	⊢ 𝑂 = ( oppCat ‘ 𝐶 )
2		2oppcco.2	⊢ 𝐵 = ( Base ‘ 𝐶 )
3		eqid	⊢ ( oppCat ‘ 𝑂 ) = ( oppCat ‘ 𝑂 )
4	1 2	oppcbas	⊢ 𝐵 = ( Base ‘ 𝑂 )
5	3 4	oppcbas	⊢ 𝐵 = ( Base ‘ ( oppCat ‘ 𝑂 ) )