Metamath Proof Explorer

Theorem setccofval

Description: Composition in the category of sets. (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Hypotheses setcbas.c ⊢ C = SetCat ⁡ U
setcbas.u ⊢ φ → U ∈ V
setcco.o ⊢ · ˙ = comp ⁡ C
Assertion setccofval ⊢ φ → · ˙ = v ∈ U × U , z ∈ U ⟼ g ∈ z 2 nd ⁡ v , f ∈ 2 nd ⁡ v 1 st ⁡ v ⟼ g ∘ f

Proof

Step Hyp Ref Expression
1 setcbas.c ⊢ C = SetCat ⁡ U
2 setcbas.u ⊢ φ → U ∈ V
3 setcco.o ⊢ · ˙ = comp ⁡ C
4 eqid ⊢ Hom ⁡ C = Hom ⁡ C
5 1 2 4 setchomfval ⊢ φ → Hom ⁡ C = x ∈ U , y ∈ U ⟼ y x
6 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
7 1 2 5 6 setcval ⊢ φ → C = Base ndx U Hom ⁡ ndx Hom ⁡ C comp ⁡ ndx v ∈ U × U , z ∈ U ⟼ g ∈ z 2 nd ⁡ v , f ∈ 2 nd ⁡ v 1 st ⁡ v ⟼ g ∘ f
8 catstr ⊢ Base ndx U Hom ⁡ ndx Hom ⁡ C comp ⁡ ndx v ∈ U × U , z ∈ U ⟼ g ∈ z 2 nd ⁡ v , f ∈ 2 nd ⁡ v 1 st ⁡ v ⟼ g ∘ f Struct 1 15
9 ccoid ⊢ comp = Slot comp ⁡ ndx
10 snsstp3 ⊢ comp ⁡ ndx v ∈ U × U , z ∈ U ⟼ g ∈ z 2 nd ⁡ v , f ∈ 2 nd ⁡ v 1 st ⁡ v ⟼ g ∘ f ⊆ Base ndx U Hom ⁡ ndx Hom ⁡ C comp ⁡ ndx v ∈ U × U , z ∈ U ⟼ g ∈ z 2 nd ⁡ v , f ∈ 2 nd ⁡ v 1 st ⁡ v ⟼ g ∘ f
11 2 2 xpexd ⊢ φ → U × U ∈ V
12 mpoexga ⊢ U × U ∈ V ∧ U ∈ V → v ∈ U × U , z ∈ U ⟼ g ∈ z 2 nd ⁡ v , f ∈ 2 nd ⁡ v 1 st ⁡ v ⟼ g ∘ f ∈ V
13 11 2 12 syl2anc ⊢ φ → v ∈ U × U , z ∈ U ⟼ g ∈ z 2 nd ⁡ v , f ∈ 2 nd ⁡ v 1 st ⁡ v ⟼ g ∘ f ∈ V
14 7 8 9 10 13 3 strfv3 ⊢ φ → · ˙ = v ∈ U × U , z ∈ U ⟼ g ∈ z 2 nd ⁡ v , f ∈ 2 nd ⁡ v 1 st ⁡ v ⟼ g ∘ f