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

Metamath Proof Explorer

Theorem setcbas

Description: Set of objects of the category of sets (in a universe). (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Hypotheses setcbas.c ⊢ C = SetCat ⁡ U
setcbas.u ⊢ φ → U ∈ V
Assertion setcbas ⊢ φ → U = Base C

Proof

Step Hyp Ref Expression
1 setcbas.c ⊢ C = SetCat ⁡ U
2 setcbas.u ⊢ φ → U ∈ V
3 catstr ⊢ Base ndx U Hom ⁡ ndx x ∈ U , y ∈ U ⟼ y x comp ⁡ ndx v ∈ U × U , z ∈ U ⟼ g ∈ z 2 nd ⁡ v , f ∈ 2 nd ⁡ v 1 st ⁡ v ⟼ g ∘ f Struct 1 15
4 baseid ⊢ Base = Slot Base ndx
5 snsstp1 ⊢ Base ndx U ⊆ Base ndx U Hom ⁡ ndx x ∈ U , y ∈ U ⟼ y x comp ⁡ ndx v ∈ U × U , z ∈ U ⟼ g ∈ z 2 nd ⁡ v , f ∈ 2 nd ⁡ v 1 st ⁡ v ⟼ g ∘ f
6 3 4 5 strfv ⊢ U ∈ V → U = Base Base ndx U Hom ⁡ ndx x ∈ U , y ∈ U ⟼ y x comp ⁡ ndx v ∈ U × U , z ∈ U ⟼ g ∈ z 2 nd ⁡ v , f ∈ 2 nd ⁡ v 1 st ⁡ v ⟼ g ∘ f
7 2 6 syl ⊢ φ → U = Base Base ndx U Hom ⁡ ndx x ∈ U , y ∈ U ⟼ y x comp ⁡ ndx v ∈ U × U , z ∈ U ⟼ g ∈ z 2 nd ⁡ v , f ∈ 2 nd ⁡ v 1 st ⁡ v ⟼ g ∘ f
8 eqidd ⊢ φ → x ∈ U , y ∈ U ⟼ y x = x ∈ U , y ∈ U ⟼ y x
9 eqidd ⊢ φ → v ∈ U × U , z ∈ U ⟼ g ∈ z 2 nd ⁡ v , f ∈ 2 nd ⁡ v 1 st ⁡ v ⟼ g ∘ f = v ∈ U × U , z ∈ U ⟼ g ∈ z 2 nd ⁡ v , f ∈ 2 nd ⁡ v 1 st ⁡ v ⟼ g ∘ f
10 1 2 8 9 setcval ⊢ φ → C = Base ndx U Hom ⁡ ndx x ∈ U , y ∈ U ⟼ y x comp ⁡ ndx v ∈ U × U , z ∈ U ⟼ g ∈ z 2 nd ⁡ v , f ∈ 2 nd ⁡ v 1 st ⁡ v ⟼ g ∘ f
11 10 fveq2d ⊢ φ → Base C = Base Base ndx U Hom ⁡ ndx x ∈ U , y ∈ U ⟼ y x comp ⁡ ndx v ∈ U × U , z ∈ U ⟼ g ∈ z 2 nd ⁡ v , f ∈ 2 nd ⁡ v 1 st ⁡ v ⟼ g ∘ f
12 7 11 eqtr4d ⊢ φ → U = Base C