Theorem cicref

Description: Isomorphism is reflexive. (Contributed by AV, 5-Apr-2020)

	Ref	Expression
Assertion	cicref	⊢ ( ( 𝐶 ∈ Cat ∧ 𝑂 ∈ ( Base ‘ 𝐶 ) ) → 𝑂 ( ≃𝑐 ‘ 𝐶 ) 𝑂 )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( Iso ‘ 𝐶 ) = ( Iso ‘ 𝐶 )
2		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
3		simpl	⊢ ( ( 𝐶 ∈ Cat ∧ 𝑂 ∈ ( Base ‘ 𝐶 ) ) → 𝐶 ∈ Cat )
4		simpr	⊢ ( ( 𝐶 ∈ Cat ∧ 𝑂 ∈ ( Base ‘ 𝐶 ) ) → 𝑂 ∈ ( Base ‘ 𝐶 ) )
5		eqid	⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
6	2 5 3 4	idiso	⊢ ( ( 𝐶 ∈ Cat ∧ 𝑂 ∈ ( Base ‘ 𝐶 ) ) → ( ( Id ‘ 𝐶 ) ‘ 𝑂 ) ∈ ( 𝑂 ( Iso ‘ 𝐶 ) 𝑂 ) )
7	1 2 3 4 4 6	brcici	⊢ ( ( 𝐶 ∈ Cat ∧ 𝑂 ∈ ( Base ‘ 𝐶 ) ) → 𝑂 ( ≃𝑐 ‘ 𝐶 ) 𝑂 )