Metamath Proof Explorer

Theorem setchomfval

Description: Set of arrows 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
setchomfval.h ⊢ H = Hom ⁡ C
Assertion setchomfval ⊢ φ → H = x ∈ U , y ∈ U ⟼ y x

Proof

Step Hyp Ref Expression
1 setcbas.c ⊢ C = SetCat ⁡ U
2 setcbas.u ⊢ φ → U ∈ V
3 setchomfval.h ⊢ H = Hom ⁡ C
4 eqidd ⊢ φ → x ∈ U , y ∈ U ⟼ y x = x ∈ U , y ∈ U ⟼ y x
5 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
6 1 2 4 5 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
7 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
8 homid ⊢ Hom = Slot Hom ⁡ ndx
9 snsstp2 ⊢ Hom ⁡ ndx x ∈ U , y ∈ U ⟼ y x ⊆ 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
10 mpoexga ⊢ U ∈ V ∧ U ∈ V → x ∈ U , y ∈ U ⟼ y x ∈ V
11 2 2 10 syl2anc ⊢ φ → x ∈ U , y ∈ U ⟼ y x ∈ V
12 6 7 8 9 11 3 strfv3 ⊢ φ → H = x ∈ U , y ∈ U ⟼ y x