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

Metamath Proof Explorer

Theorem comfffval

Description: Value of the functionalized composition operation. (Contributed by Mario Carneiro, 4-Jan-2017) (Proof shortened by AV, 1-Mar-2024)

Ref Expression
Hypotheses comfffval.o ⊢ 𝑂 = ( compf ‘ 𝐶 )
comfffval.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
comfffval.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
comfffval.x ⊢ · = ( comp ‘ 𝐶 )
Assertion comfffval 𝑂 = ( 𝑥 ∈ ( 𝐵 × 𝐵 ) , 𝑦 ∈ 𝐵 ↦ ( 𝑔 ∈ ( ( 2nd ‘ 𝑥 ) 𝐻 𝑦 ) , 𝑓 ∈ ( 𝐻 ‘ 𝑥 ) ↦ ( 𝑔 ( 𝑥 · 𝑦 ) 𝑓 ) ) )

Proof

Step Hyp Ref Expression
1 comfffval.o ⊢ 𝑂 = ( compf ‘ 𝐶 )
2 comfffval.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
3 comfffval.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
4 comfffval.x ⊢ · = ( comp ‘ 𝐶 )
5 fveq2 ⊢ ( 𝑐 = 𝐶 → ( Base ‘ 𝑐 ) = ( Base ‘ 𝐶 ) )
6 5 2 eqtr4di ⊢ ( 𝑐 = 𝐶 → ( Base ‘ 𝑐 ) = 𝐵 )
7 6 sqxpeqd ⊢ ( 𝑐 = 𝐶 → ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑐 ) ) = ( 𝐵 × 𝐵 ) )
8 fveq2 ⊢ ( 𝑐 = 𝐶 → ( Hom ‘ 𝑐 ) = ( Hom ‘ 𝐶 ) )
9 8 3 eqtr4di ⊢ ( 𝑐 = 𝐶 → ( Hom ‘ 𝑐 ) = 𝐻 )
10 9 oveqd ⊢ ( 𝑐 = 𝐶 → ( ( 2nd ‘ 𝑥 ) ( Hom ‘ 𝑐 ) 𝑦 ) = ( ( 2nd ‘ 𝑥 ) 𝐻 𝑦 ) )
11 9 fveq1d ⊢ ( 𝑐 = 𝐶 → ( ( Hom ‘ 𝑐 ) ‘ 𝑥 ) = ( 𝐻 ‘ 𝑥 ) )
12 fveq2 ⊢ ( 𝑐 = 𝐶 → ( comp ‘ 𝑐 ) = ( comp ‘ 𝐶 ) )
13 12 4 eqtr4di ⊢ ( 𝑐 = 𝐶 → ( comp ‘ 𝑐 ) = · )
14 13 oveqd ⊢ ( 𝑐 = 𝐶 → ( 𝑥 ( comp ‘ 𝑐 ) 𝑦 ) = ( 𝑥 · 𝑦 ) )
15 14 oveqd ⊢ ( 𝑐 = 𝐶 → ( 𝑔 ( 𝑥 ( comp ‘ 𝑐 ) 𝑦 ) 𝑓 ) = ( 𝑔 ( 𝑥 · 𝑦 ) 𝑓 ) )
16 10 11 15 mpoeq123dv ⊢ ( 𝑐 = 𝐶 → ( 𝑔 ∈ ( ( 2nd ‘ 𝑥 ) ( Hom ‘ 𝑐 ) 𝑦 ) , 𝑓 ∈ ( ( Hom ‘ 𝑐 ) ‘ 𝑥 ) ↦ ( 𝑔 ( 𝑥 ( comp ‘ 𝑐 ) 𝑦 ) 𝑓 ) ) = ( 𝑔 ∈ ( ( 2nd ‘ 𝑥 ) 𝐻 𝑦 ) , 𝑓 ∈ ( 𝐻 ‘ 𝑥 ) ↦ ( 𝑔 ( 𝑥 · 𝑦 ) 𝑓 ) ) )
17 7 6 16 mpoeq123dv ⊢ ( 𝑐 = 𝐶 → ( 𝑥 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑐 ) ) , 𝑦 ∈ ( Base ‘ 𝑐 ) ↦ ( 𝑔 ∈ ( ( 2nd ‘ 𝑥 ) ( Hom ‘ 𝑐 ) 𝑦 ) , 𝑓 ∈ ( ( Hom ‘ 𝑐 ) ‘ 𝑥 ) ↦ ( 𝑔 ( 𝑥 ( comp ‘ 𝑐 ) 𝑦 ) 𝑓 ) ) ) = ( 𝑥 ∈ ( 𝐵 × 𝐵 ) , 𝑦 ∈ 𝐵 ↦ ( 𝑔 ∈ ( ( 2nd ‘ 𝑥 ) 𝐻 𝑦 ) , 𝑓 ∈ ( 𝐻 ‘ 𝑥 ) ↦ ( 𝑔 ( 𝑥 · 𝑦 ) 𝑓 ) ) ) )
18 df-comf ⊢ compf = ( 𝑐 ∈ V ↦ ( 𝑥 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑐 ) ) , 𝑦 ∈ ( Base ‘ 𝑐 ) ↦ ( 𝑔 ∈ ( ( 2nd ‘ 𝑥 ) ( Hom ‘ 𝑐 ) 𝑦 ) , 𝑓 ∈ ( ( Hom ‘ 𝑐 ) ‘ 𝑥 ) ↦ ( 𝑔 ( 𝑥 ( comp ‘ 𝑐 ) 𝑦 ) 𝑓 ) ) ) )
19 2 fvexi ⊢ 𝐵 ∈ V
20 19 19 xpex ⊢ ( 𝐵 × 𝐵 ) ∈ V
21 20 19 mpoex ⊢ ( 𝑥 ∈ ( 𝐵 × 𝐵 ) , 𝑦 ∈ 𝐵 ↦ ( 𝑔 ∈ ( ( 2nd ‘ 𝑥 ) 𝐻 𝑦 ) , 𝑓 ∈ ( 𝐻 ‘ 𝑥 ) ↦ ( 𝑔 ( 𝑥 · 𝑦 ) 𝑓 ) ) ) ∈ V
22 17 18 21 fvmpt ⊢ ( 𝐶 ∈ V → ( compf ‘ 𝐶 ) = ( 𝑥 ∈ ( 𝐵 × 𝐵 ) , 𝑦 ∈ 𝐵 ↦ ( 𝑔 ∈ ( ( 2nd ‘ 𝑥 ) 𝐻 𝑦 ) , 𝑓 ∈ ( 𝐻 ‘ 𝑥 ) ↦ ( 𝑔 ( 𝑥 · 𝑦 ) 𝑓 ) ) ) )
23 fvprc ⊢ ( ¬ 𝐶 ∈ V → ( compf ‘ 𝐶 ) = ∅ )
24 fvprc ⊢ ( ¬ 𝐶 ∈ V → ( Base ‘ 𝐶 ) = ∅ )
25 2 24 eqtrid ⊢ ( ¬ 𝐶 ∈ V → 𝐵 = ∅ )
26 25 olcd ⊢ ( ¬ 𝐶 ∈ V → ( ( 𝐵 × 𝐵 ) = ∅ ∨ 𝐵 = ∅ ) )
27 0mpo0 ⊢ ( ( ( 𝐵 × 𝐵 ) = ∅ ∨ 𝐵 = ∅ ) → ( 𝑥 ∈ ( 𝐵 × 𝐵 ) , 𝑦 ∈ 𝐵 ↦ ( 𝑔 ∈ ( ( 2nd ‘ 𝑥 ) 𝐻 𝑦 ) , 𝑓 ∈ ( 𝐻 ‘ 𝑥 ) ↦ ( 𝑔 ( 𝑥 · 𝑦 ) 𝑓 ) ) ) = ∅ )
28 26 27 syl ⊢ ( ¬ 𝐶 ∈ V → ( 𝑥 ∈ ( 𝐵 × 𝐵 ) , 𝑦 ∈ 𝐵 ↦ ( 𝑔 ∈ ( ( 2nd ‘ 𝑥 ) 𝐻 𝑦 ) , 𝑓 ∈ ( 𝐻 ‘ 𝑥 ) ↦ ( 𝑔 ( 𝑥 · 𝑦 ) 𝑓 ) ) ) = ∅ )
29 23 28 eqtr4d ⊢ ( ¬ 𝐶 ∈ V → ( compf ‘ 𝐶 ) = ( 𝑥 ∈ ( 𝐵 × 𝐵 ) , 𝑦 ∈ 𝐵 ↦ ( 𝑔 ∈ ( ( 2nd ‘ 𝑥 ) 𝐻 𝑦 ) , 𝑓 ∈ ( 𝐻 ‘ 𝑥 ) ↦ ( 𝑔 ( 𝑥 · 𝑦 ) 𝑓 ) ) ) )
30 22 29 pm2.61i ⊢ ( compf ‘ 𝐶 ) = ( 𝑥 ∈ ( 𝐵 × 𝐵 ) , 𝑦 ∈ 𝐵 ↦ ( 𝑔 ∈ ( ( 2nd ‘ 𝑥 ) 𝐻 𝑦 ) , 𝑓 ∈ ( 𝐻 ‘ 𝑥 ) ↦ ( 𝑔 ( 𝑥 · 𝑦 ) 𝑓 ) ) )
31 1 30 eqtri ⊢ 𝑂 = ( 𝑥 ∈ ( 𝐵 × 𝐵 ) , 𝑦 ∈ 𝐵 ↦ ( 𝑔 ∈ ( ( 2nd ‘ 𝑥 ) 𝐻 𝑦 ) , 𝑓 ∈ ( 𝐻 ‘ 𝑥 ) ↦ ( 𝑔 ( 𝑥 · 𝑦 ) 𝑓 ) ) )