coafval

Description: The value of the composition of arrows. (Contributed by Mario Carneiro, 11-Jan-2017)

	Ref	Expression
Hypotheses	coafval.o	⊢ · = ( comp_a ‘ 𝐶 )
	coafval.a	⊢ 𝐴 = ( Arrow ‘ 𝐶 )
	coafval.x	⊢ ∙ = ( comp ‘ 𝐶 )
Assertion	coafval	⊢ · = ( 𝑔 ∈ 𝐴 , 𝑓 ∈ { ℎ ∈ 𝐴 ∣ ( cod_a ‘ ℎ ) = ( dom_a ‘ 𝑔 ) } ↦ ⟨ ( dom_a ‘ 𝑓 ) , ( cod_a ‘ 𝑔 ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( dom_a ‘ 𝑓 ) , ( dom_a ‘ 𝑔 ) ⟩ ∙ ( cod_a ‘ 𝑔 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ )

Proof

Step	Hyp	Ref	Expression
1		coafval.o	⊢ · = ( comp_a ‘ 𝐶 )
2		coafval.a	⊢ 𝐴 = ( Arrow ‘ 𝐶 )
3		coafval.x	⊢ ∙ = ( comp ‘ 𝐶 )
4		fveq2	⊢ ( 𝑐 = 𝐶 → ( Arrow ‘ 𝑐 ) = ( Arrow ‘ 𝐶 ) )
5	4 2	eqtr4di	⊢ ( 𝑐 = 𝐶 → ( Arrow ‘ 𝑐 ) = 𝐴 )
6	5	rabeqdv	⊢ ( 𝑐 = 𝐶 → { ℎ ∈ ( Arrow ‘ 𝑐 ) ∣ ( cod_a ‘ ℎ ) = ( dom_a ‘ 𝑔 ) } = { ℎ ∈ 𝐴 ∣ ( cod_a ‘ ℎ ) = ( dom_a ‘ 𝑔 ) } )
7		fveq2	⊢ ( 𝑐 = 𝐶 → ( comp ‘ 𝑐 ) = ( comp ‘ 𝐶 ) )
8	7 3	eqtr4di	⊢ ( 𝑐 = 𝐶 → ( comp ‘ 𝑐 ) = ∙ )
9	8	oveqd	⊢ ( 𝑐 = 𝐶 → ( ⟨ ( dom_a ‘ 𝑓 ) , ( dom_a ‘ 𝑔 ) ⟩ ( comp ‘ 𝑐 ) ( cod_a ‘ 𝑔 ) ) = ( ⟨ ( dom_a ‘ 𝑓 ) , ( dom_a ‘ 𝑔 ) ⟩ ∙ ( cod_a ‘ 𝑔 ) ) )
10	9	oveqd	⊢ ( 𝑐 = 𝐶 → ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( dom_a ‘ 𝑓 ) , ( dom_a ‘ 𝑔 ) ⟩ ( comp ‘ 𝑐 ) ( cod_a ‘ 𝑔 ) ) ( 2^nd ‘ 𝑓 ) ) = ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( dom_a ‘ 𝑓 ) , ( dom_a ‘ 𝑔 ) ⟩ ∙ ( cod_a ‘ 𝑔 ) ) ( 2^nd ‘ 𝑓 ) ) )
11	10	oteq3d	⊢ ( 𝑐 = 𝐶 → ⟨ ( dom_a ‘ 𝑓 ) , ( cod_a ‘ 𝑔 ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( dom_a ‘ 𝑓 ) , ( dom_a ‘ 𝑔 ) ⟩ ( comp ‘ 𝑐 ) ( cod_a ‘ 𝑔 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ = ⟨ ( dom_a ‘ 𝑓 ) , ( cod_a ‘ 𝑔 ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( dom_a ‘ 𝑓 ) , ( dom_a ‘ 𝑔 ) ⟩ ∙ ( cod_a ‘ 𝑔 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ )
12	5 6 11	mpoeq123dv	⊢ ( 𝑐 = 𝐶 → ( 𝑔 ∈ ( Arrow ‘ 𝑐 ) , 𝑓 ∈ { ℎ ∈ ( Arrow ‘ 𝑐 ) ∣ ( cod_a ‘ ℎ ) = ( dom_a ‘ 𝑔 ) } ↦ ⟨ ( dom_a ‘ 𝑓 ) , ( cod_a ‘ 𝑔 ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( dom_a ‘ 𝑓 ) , ( dom_a ‘ 𝑔 ) ⟩ ( comp ‘ 𝑐 ) ( cod_a ‘ 𝑔 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ ) = ( 𝑔 ∈ 𝐴 , 𝑓 ∈ { ℎ ∈ 𝐴 ∣ ( cod_a ‘ ℎ ) = ( dom_a ‘ 𝑔 ) } ↦ ⟨ ( dom_a ‘ 𝑓 ) , ( cod_a ‘ 𝑔 ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( dom_a ‘ 𝑓 ) , ( dom_a ‘ 𝑔 ) ⟩ ∙ ( cod_a ‘ 𝑔 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ ) )
13		df-coa	⊢ comp_a = ( 𝑐 ∈ Cat ↦ ( 𝑔 ∈ ( Arrow ‘ 𝑐 ) , 𝑓 ∈ { ℎ ∈ ( Arrow ‘ 𝑐 ) ∣ ( cod_a ‘ ℎ ) = ( dom_a ‘ 𝑔 ) } ↦ ⟨ ( dom_a ‘ 𝑓 ) , ( cod_a ‘ 𝑔 ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( dom_a ‘ 𝑓 ) , ( dom_a ‘ 𝑔 ) ⟩ ( comp ‘ 𝑐 ) ( cod_a ‘ 𝑔 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ ) )
14	2	fvexi	⊢ 𝐴 ∈ V
15	14	rabex	⊢ { ℎ ∈ 𝐴 ∣ ( cod_a ‘ ℎ ) = ( dom_a ‘ 𝑔 ) } ∈ V
16	14 15	mpoex	⊢ ( 𝑔 ∈ 𝐴 , 𝑓 ∈ { ℎ ∈ 𝐴 ∣ ( cod_a ‘ ℎ ) = ( dom_a ‘ 𝑔 ) } ↦ ⟨ ( dom_a ‘ 𝑓 ) , ( cod_a ‘ 𝑔 ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( dom_a ‘ 𝑓 ) , ( dom_a ‘ 𝑔 ) ⟩ ∙ ( cod_a ‘ 𝑔 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ ) ∈ V
17	12 13 16	fvmpt	⊢ ( 𝐶 ∈ Cat → ( comp_a ‘ 𝐶 ) = ( 𝑔 ∈ 𝐴 , 𝑓 ∈ { ℎ ∈ 𝐴 ∣ ( cod_a ‘ ℎ ) = ( dom_a ‘ 𝑔 ) } ↦ ⟨ ( dom_a ‘ 𝑓 ) , ( cod_a ‘ 𝑔 ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( dom_a ‘ 𝑓 ) , ( dom_a ‘ 𝑔 ) ⟩ ∙ ( cod_a ‘ 𝑔 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ ) )
18	13	fvmptndm	⊢ ( ¬ 𝐶 ∈ Cat → ( comp_a ‘ 𝐶 ) = ∅ )
19	2	arwrcl	⊢ ( 𝑓 ∈ 𝐴 → 𝐶 ∈ Cat )
20	19	con3i	⊢ ( ¬ 𝐶 ∈ Cat → ¬ 𝑓 ∈ 𝐴 )
21	20	eq0rdv	⊢ ( ¬ 𝐶 ∈ Cat → 𝐴 = ∅ )
22		eqidd	⊢ ( ¬ 𝐶 ∈ Cat → { ℎ ∈ 𝐴 ∣ ( cod_a ‘ ℎ ) = ( dom_a ‘ 𝑔 ) } = { ℎ ∈ 𝐴 ∣ ( cod_a ‘ ℎ ) = ( dom_a ‘ 𝑔 ) } )
23		eqidd	⊢ ( ¬ 𝐶 ∈ Cat → ⟨ ( dom_a ‘ 𝑓 ) , ( cod_a ‘ 𝑔 ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( dom_a ‘ 𝑓 ) , ( dom_a ‘ 𝑔 ) ⟩ ∙ ( cod_a ‘ 𝑔 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ = ⟨ ( dom_a ‘ 𝑓 ) , ( cod_a ‘ 𝑔 ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( dom_a ‘ 𝑓 ) , ( dom_a ‘ 𝑔 ) ⟩ ∙ ( cod_a ‘ 𝑔 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ )
24	21 22 23	mpoeq123dv	⊢ ( ¬ 𝐶 ∈ Cat → ( 𝑔 ∈ 𝐴 , 𝑓 ∈ { ℎ ∈ 𝐴 ∣ ( cod_a ‘ ℎ ) = ( dom_a ‘ 𝑔 ) } ↦ ⟨ ( dom_a ‘ 𝑓 ) , ( cod_a ‘ 𝑔 ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( dom_a ‘ 𝑓 ) , ( dom_a ‘ 𝑔 ) ⟩ ∙ ( cod_a ‘ 𝑔 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ ) = ( 𝑔 ∈ ∅ , 𝑓 ∈ { ℎ ∈ 𝐴 ∣ ( cod_a ‘ ℎ ) = ( dom_a ‘ 𝑔 ) } ↦ ⟨ ( dom_a ‘ 𝑓 ) , ( cod_a ‘ 𝑔 ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( dom_a ‘ 𝑓 ) , ( dom_a ‘ 𝑔 ) ⟩ ∙ ( cod_a ‘ 𝑔 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ ) )
25		mpo0	⊢ ( 𝑔 ∈ ∅ , 𝑓 ∈ { ℎ ∈ 𝐴 ∣ ( cod_a ‘ ℎ ) = ( dom_a ‘ 𝑔 ) } ↦ ⟨ ( dom_a ‘ 𝑓 ) , ( cod_a ‘ 𝑔 ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( dom_a ‘ 𝑓 ) , ( dom_a ‘ 𝑔 ) ⟩ ∙ ( cod_a ‘ 𝑔 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ ) = ∅
26	24 25	eqtrdi	⊢ ( ¬ 𝐶 ∈ Cat → ( 𝑔 ∈ 𝐴 , 𝑓 ∈ { ℎ ∈ 𝐴 ∣ ( cod_a ‘ ℎ ) = ( dom_a ‘ 𝑔 ) } ↦ ⟨ ( dom_a ‘ 𝑓 ) , ( cod_a ‘ 𝑔 ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( dom_a ‘ 𝑓 ) , ( dom_a ‘ 𝑔 ) ⟩ ∙ ( cod_a ‘ 𝑔 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ ) = ∅ )
27	18 26	eqtr4d	⊢ ( ¬ 𝐶 ∈ Cat → ( comp_a ‘ 𝐶 ) = ( 𝑔 ∈ 𝐴 , 𝑓 ∈ { ℎ ∈ 𝐴 ∣ ( cod_a ‘ ℎ ) = ( dom_a ‘ 𝑔 ) } ↦ ⟨ ( dom_a ‘ 𝑓 ) , ( cod_a ‘ 𝑔 ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( dom_a ‘ 𝑓 ) , ( dom_a ‘ 𝑔 ) ⟩ ∙ ( cod_a ‘ 𝑔 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ ) )
28	17 27	pm2.61i	⊢ ( comp_a ‘ 𝐶 ) = ( 𝑔 ∈ 𝐴 , 𝑓 ∈ { ℎ ∈ 𝐴 ∣ ( cod_a ‘ ℎ ) = ( dom_a ‘ 𝑔 ) } ↦ ⟨ ( dom_a ‘ 𝑓 ) , ( cod_a ‘ 𝑔 ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( dom_a ‘ 𝑓 ) , ( dom_a ‘ 𝑔 ) ⟩ ∙ ( cod_a ‘ 𝑔 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ )
29	1 28	eqtri	⊢ · = ( 𝑔 ∈ 𝐴 , 𝑓 ∈ { ℎ ∈ 𝐴 ∣ ( cod_a ‘ ℎ ) = ( dom_a ‘ 𝑔 ) } ↦ ⟨ ( dom_a ‘ 𝑓 ) , ( cod_a ‘ 𝑔 ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( dom_a ‘ 𝑓 ) , ( dom_a ‘ 𝑔 ) ⟩ ∙ ( cod_a ‘ 𝑔 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ )

Metamath Proof Explorer

Theorem coafval

Proof