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

Metamath Proof Explorer

Theorem setccat

Description: The category of sets is a category. (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Hypothesis setccat.c ⊢ C = SetCat ⁡ U
Assertion setccat ⊢ U ∈ V → C ∈ Cat

Proof

Step Hyp Ref Expression
1 setccat.c ⊢ C = SetCat ⁡ U
2 1 setccatid ⊢ U ∈ V → C ∈ Cat ∧ Id ⁡ C = x ∈ U ⟼ I ↾ x
3 2 simpld ⊢ U ∈ V → C ∈ Cat