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 𝐶 = ( SetCat ‘ 𝑈 )
setcbas.u ( 𝜑𝑈𝑉 )
setchomfval.h 𝐻 = ( Hom ‘ 𝐶 )
Assertion setchomfval ( 𝜑𝐻 = ( 𝑥𝑈 , 𝑦𝑈 ↦ ( 𝑦m 𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 setcbas.c 𝐶 = ( SetCat ‘ 𝑈 )
2 setcbas.u ( 𝜑𝑈𝑉 )
3 setchomfval.h 𝐻 = ( Hom ‘ 𝐶 )
4 eqidd ( 𝜑 → ( 𝑥𝑈 , 𝑦𝑈 ↦ ( 𝑦m 𝑥 ) ) = ( 𝑥𝑈 , 𝑦𝑈 ↦ ( 𝑦m 𝑥 ) ) )
5 eqidd ( 𝜑 → ( 𝑣 ∈ ( 𝑈 × 𝑈 ) , 𝑧𝑈 ↦ ( 𝑔 ∈ ( 𝑧m ( 2nd𝑣 ) ) , 𝑓 ∈ ( ( 2nd𝑣 ) ↑m ( 1st𝑣 ) ) ↦ ( 𝑔𝑓 ) ) ) = ( 𝑣 ∈ ( 𝑈 × 𝑈 ) , 𝑧𝑈 ↦ ( 𝑔 ∈ ( 𝑧m ( 2nd𝑣 ) ) , 𝑓 ∈ ( ( 2nd𝑣 ) ↑m ( 1st𝑣 ) ) ↦ ( 𝑔𝑓 ) ) ) )
6 1 2 4 5 setcval ( 𝜑𝐶 = { ⟨ ( Base ‘ ndx ) , 𝑈 ⟩ , ⟨ ( Hom ‘ ndx ) , ( 𝑥𝑈 , 𝑦𝑈 ↦ ( 𝑦m 𝑥 ) ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( 𝑈 × 𝑈 ) , 𝑧𝑈 ↦ ( 𝑔 ∈ ( 𝑧m ( 2nd𝑣 ) ) , 𝑓 ∈ ( ( 2nd𝑣 ) ↑m ( 1st𝑣 ) ) ↦ ( 𝑔𝑓 ) ) ) ⟩ } )
7 catstr { ⟨ ( Base ‘ ndx ) , 𝑈 ⟩ , ⟨ ( Hom ‘ ndx ) , ( 𝑥𝑈 , 𝑦𝑈 ↦ ( 𝑦m 𝑥 ) ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( 𝑈 × 𝑈 ) , 𝑧𝑈 ↦ ( 𝑔 ∈ ( 𝑧m ( 2nd𝑣 ) ) , 𝑓 ∈ ( ( 2nd𝑣 ) ↑m ( 1st𝑣 ) ) ↦ ( 𝑔𝑓 ) ) ) ⟩ } Struct ⟨ 1 , 1 5 ⟩
8 homid Hom = Slot ( Hom ‘ ndx )
9 snsstp2 { ⟨ ( Hom ‘ ndx ) , ( 𝑥𝑈 , 𝑦𝑈 ↦ ( 𝑦m 𝑥 ) ) ⟩ } ⊆ { ⟨ ( Base ‘ ndx ) , 𝑈 ⟩ , ⟨ ( Hom ‘ ndx ) , ( 𝑥𝑈 , 𝑦𝑈 ↦ ( 𝑦m 𝑥 ) ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( 𝑈 × 𝑈 ) , 𝑧𝑈 ↦ ( 𝑔 ∈ ( 𝑧m ( 2nd𝑣 ) ) , 𝑓 ∈ ( ( 2nd𝑣 ) ↑m ( 1st𝑣 ) ) ↦ ( 𝑔𝑓 ) ) ) ⟩ }
10 mpoexga ( ( 𝑈𝑉𝑈𝑉 ) → ( 𝑥𝑈 , 𝑦𝑈 ↦ ( 𝑦m 𝑥 ) ) ∈ V )
11 2 2 10 syl2anc ( 𝜑 → ( 𝑥𝑈 , 𝑦𝑈 ↦ ( 𝑦m 𝑥 ) ) ∈ V )
12 6 7 8 9 11 3 strfv3 ( 𝜑𝐻 = ( 𝑥𝑈 , 𝑦𝑈 ↦ ( 𝑦m 𝑥 ) ) )