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

Metamath Proof Explorer

Theorem cicrcl2

Description: Isomorphism implies the structure being a category. (Contributed by Zhi Wang, 26-Oct-2025)

Ref Expression
Assertion cicrcl2 ⊢ R ≃ 𝑐 ⁡ C S → C ∈ Cat

Proof

Step Hyp Ref Expression
1 df-br ⊢ R ≃ 𝑐 ⁡ C S ↔ R S ∈ ≃ 𝑐 ⁡ C
2 elfvdm ⊢ R S ∈ ≃ 𝑐 ⁡ C → C ∈ dom ⁡ ≃ 𝑐
3 cicfn ⊢ ≃ 𝑐 Fn Cat
4 3 fndmi ⊢ dom ⁡ ≃ 𝑐 = Cat
5 2 4 eleqtrdi ⊢ R S ∈ ≃ 𝑐 ⁡ C → C ∈ Cat
6 1 5 sylbi ⊢ R ≃ 𝑐 ⁡ C S → C ∈ Cat