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

Metamath Proof Explorer

Theorem comfffn

Description: The functionalized composition operation is a function. (Contributed by Mario Carneiro, 4-Jan-2017)

Ref Expression
Hypotheses comfffn.o ⊢ 𝑂 = ( compf ‘ 𝐶 )
comfffn.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
Assertion comfffn 𝑂 Fn ( ( 𝐵 × 𝐵 ) × 𝐵 )

Proof

Step Hyp Ref Expression
1 comfffn.o ⊢ 𝑂 = ( compf ‘ 𝐶 )
2 comfffn.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
3 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
4 eqid ⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
5 1 2 3 4 comfffval ⊢ 𝑂 = ( 𝑥 ∈ ( 𝐵 × 𝐵 ) , 𝑦 ∈ 𝐵 ↦ ( 𝑔 ∈ ( ( 2nd ‘ 𝑥 ) ( Hom ‘ 𝐶 ) 𝑦 ) , 𝑓 ∈ ( ( Hom ‘ 𝐶 ) ‘ 𝑥 ) ↦ ( 𝑔 ( 𝑥 ( comp ‘ 𝐶 ) 𝑦 ) 𝑓 ) ) )
6 ovex ⊢ ( ( 2nd ‘ 𝑥 ) ( Hom ‘ 𝐶 ) 𝑦 ) ∈ V
7 fvex ⊢ ( ( Hom ‘ 𝐶 ) ‘ 𝑥 ) ∈ V
8 6 7 mpoex ⊢ ( 𝑔 ∈ ( ( 2nd ‘ 𝑥 ) ( Hom ‘ 𝐶 ) 𝑦 ) , 𝑓 ∈ ( ( Hom ‘ 𝐶 ) ‘ 𝑥 ) ↦ ( 𝑔 ( 𝑥 ( comp ‘ 𝐶 ) 𝑦 ) 𝑓 ) ) ∈ V
9 5 8 fnmpoi ⊢ 𝑂 Fn ( ( 𝐵 × 𝐵 ) × 𝐵 )