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

Metamath Proof Explorer

Theorem catchomfval

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

Ref Expression
Hypotheses catcbas.c ⊢ 𝐶 = ( CatCat ‘ 𝑈 )
catcbas.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
catcbas.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
catchomfval.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
Assertion catchomfval ( 𝜑 → 𝐻 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 Func 𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 catcbas.c ⊢ 𝐶 = ( CatCat ‘ 𝑈 )
2 catcbas.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
3 catcbas.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
4 catchomfval.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
5 1 2 3 catcbas ⊢ ( 𝜑 → 𝐵 = ( 𝑈 ∩ Cat ) )
6 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 Func 𝑦 ) ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 Func 𝑦 ) ) )
7 eqidd ⊢ ( 𝜑 → ( 𝑣 ∈ ( 𝐵 × 𝐵 ) , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( ( 2nd ‘ 𝑣 ) Func 𝑧 ) , 𝑓 ∈ ( Func ‘ 𝑣 ) ↦ ( 𝑔 ∘func 𝑓 ) ) ) = ( 𝑣 ∈ ( 𝐵 × 𝐵 ) , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( ( 2nd ‘ 𝑣 ) Func 𝑧 ) , 𝑓 ∈ ( Func ‘ 𝑣 ) ↦ ( 𝑔 ∘func 𝑓 ) ) ) )
8 1 3 5 6 7 catcval ⊢ ( 𝜑 → 𝐶 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 Func 𝑦 ) ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( 𝐵 × 𝐵 ) , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( ( 2nd ‘ 𝑣 ) Func 𝑧 ) , 𝑓 ∈ ( Func ‘ 𝑣 ) ↦ ( 𝑔 ∘func 𝑓 ) ) ) ⟩ } )
9 8 fveq2d ⊢ ( 𝜑 → ( Hom ‘ 𝐶 ) = ( Hom ‘ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 Func 𝑦 ) ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( 𝐵 × 𝐵 ) , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( ( 2nd ‘ 𝑣 ) Func 𝑧 ) , 𝑓 ∈ ( Func ‘ 𝑣 ) ↦ ( 𝑔 ∘func 𝑓 ) ) ) ⟩ } ) )
10 4 9 eqtrid ⊢ ( 𝜑 → 𝐻 = ( Hom ‘ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 Func 𝑦 ) ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( 𝐵 × 𝐵 ) , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( ( 2nd ‘ 𝑣 ) Func 𝑧 ) , 𝑓 ∈ ( Func ‘ 𝑣 ) ↦ ( 𝑔 ∘func 𝑓 ) ) ) ⟩ } ) )
11 2 fvexi ⊢ 𝐵 ∈ V
12 11 11 mpoex ⊢ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 Func 𝑦 ) ) ∈ V
13 catstr ⊢ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 Func 𝑦 ) ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( 𝐵 × 𝐵 ) , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( ( 2nd ‘ 𝑣 ) Func 𝑧 ) , 𝑓 ∈ ( Func ‘ 𝑣 ) ↦ ( 𝑔 ∘func 𝑓 ) ) ) ⟩ } Struct ⟨ 1 , 1 5 ⟩
14 homid ⊢ Hom = Slot ( Hom ‘ ndx )
15 snsstp2 ⊢ { ⟨ ( Hom ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 Func 𝑦 ) ) ⟩ } ⊆ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 Func 𝑦 ) ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( 𝐵 × 𝐵 ) , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( ( 2nd ‘ 𝑣 ) Func 𝑧 ) , 𝑓 ∈ ( Func ‘ 𝑣 ) ↦ ( 𝑔 ∘func 𝑓 ) ) ) ⟩ }
16 13 14 15 strfv ⊢ ( ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 Func 𝑦 ) ) ∈ V → ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 Func 𝑦 ) ) = ( Hom ‘ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 Func 𝑦 ) ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( 𝐵 × 𝐵 ) , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( ( 2nd ‘ 𝑣 ) Func 𝑧 ) , 𝑓 ∈ ( Func ‘ 𝑣 ) ↦ ( 𝑔 ∘func 𝑓 ) ) ) ⟩ } ) )
17 12 16 mp1i ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 Func 𝑦 ) ) = ( Hom ‘ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 Func 𝑦 ) ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( 𝐵 × 𝐵 ) , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( ( 2nd ‘ 𝑣 ) Func 𝑧 ) , 𝑓 ∈ ( Func ‘ 𝑣 ) ↦ ( 𝑔 ∘func 𝑓 ) ) ) ⟩ } ) )
18 10 17 eqtr4d ⊢ ( 𝜑 → 𝐻 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 Func 𝑦 ) ) )