Metamath Proof Explorer

Theorem coafval

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

Ref Expression
Hypotheses coafval.o ⊢·˙=compa⁡C
coafval.a ⊢A=Arrow⁡C
coafval.x ⊢∙˙=comp⁡C
Assertion coafval ⊢·˙=g∈A,f∈h∈A|coda⁡h=doma⁡g⟼doma⁡fcoda⁡g2nd⁡gdoma⁡fdoma⁡g∙˙coda⁡g2nd⁡f

Proof

Step Hyp Ref Expression
1 coafval.o ⊢·˙=compa⁡C
2 coafval.a ⊢A=Arrow⁡C
3 coafval.x ⊢∙˙=comp⁡C
4 fveq2 ⊢c=C→Arrow⁡c=Arrow⁡C
5 4 2 eqtr4di ⊢c=C→Arrow⁡c=A
6 5 rabeqdv ⊢c=C→h∈Arrow⁡c|coda⁡h=doma⁡g=h∈A|coda⁡h=doma⁡g
7 fveq2 ⊢c=C→comp⁡c=comp⁡C
8 7 3 eqtr4di ⊢c=C→comp⁡c=∙˙
9 8 oveqd ⊢c=C→doma⁡fdoma⁡gcomp⁡ccoda⁡g=doma⁡fdoma⁡g∙˙coda⁡g
10 9 oveqd ⊢c=C→2nd⁡gdoma⁡fdoma⁡gcomp⁡ccoda⁡g2nd⁡f=2nd⁡gdoma⁡fdoma⁡g∙˙coda⁡g2nd⁡f
11 10 oteq3d ⊢c=C→doma⁡fcoda⁡g2nd⁡gdoma⁡fdoma⁡gcomp⁡ccoda⁡g2nd⁡f=doma⁡fcoda⁡g2nd⁡gdoma⁡fdoma⁡g∙˙coda⁡g2nd⁡f
12 5 6 11 mpoeq123dv ⊢c=C→g∈Arrow⁡c,f∈h∈Arrow⁡c|coda⁡h=doma⁡g⟼doma⁡fcoda⁡g2nd⁡gdoma⁡fdoma⁡gcomp⁡ccoda⁡g2nd⁡f=g∈A,f∈h∈A|coda⁡h=doma⁡g⟼doma⁡fcoda⁡g2nd⁡gdoma⁡fdoma⁡g∙˙coda⁡g2nd⁡f
13 df-coa ⊢compa=c∈Cat⟼g∈Arrow⁡c,f∈h∈Arrow⁡c|coda⁡h=doma⁡g⟼doma⁡fcoda⁡g2nd⁡gdoma⁡fdoma⁡gcomp⁡ccoda⁡g2nd⁡f
14 2 fvexi ⊢A∈V
15 14 rabex ⊢h∈A|coda⁡h=doma⁡g∈V
16 14 15 mpoex ⊢g∈A,f∈h∈A|coda⁡h=doma⁡g⟼doma⁡fcoda⁡g2nd⁡gdoma⁡fdoma⁡g∙˙coda⁡g2nd⁡f∈V
17 12 13 16 fvmpt ⊢C∈Cat→compa⁡C=g∈A,f∈h∈A|coda⁡h=doma⁡g⟼doma⁡fcoda⁡g2nd⁡gdoma⁡fdoma⁡g∙˙coda⁡g2nd⁡f
18 13 fvmptndm ⊢¬C∈Cat→compa⁡C=∅
19 2 arwrcl ⊢f∈A→C∈Cat
20 19 con3i ⊢¬C∈Cat→¬f∈A
21 20 eq0rdv ⊢¬C∈Cat→A=∅
22 eqidd ⊢¬C∈Cat→h∈A|coda⁡h=doma⁡g=h∈A|coda⁡h=doma⁡g
23 eqidd ⊢¬C∈Cat→doma⁡fcoda⁡g2nd⁡gdoma⁡fdoma⁡g∙˙coda⁡g2nd⁡f=doma⁡fcoda⁡g2nd⁡gdoma⁡fdoma⁡g∙˙coda⁡g2nd⁡f
24 21 22 23 mpoeq123dv ⊢¬C∈Cat→g∈A,f∈h∈A|coda⁡h=doma⁡g⟼doma⁡fcoda⁡g2nd⁡gdoma⁡fdoma⁡g∙˙coda⁡g2nd⁡f=g∈∅,f∈h∈A|coda⁡h=doma⁡g⟼doma⁡fcoda⁡g2nd⁡gdoma⁡fdoma⁡g∙˙coda⁡g2nd⁡f
25 mpo0 ⊢g∈∅,f∈h∈A|coda⁡h=doma⁡g⟼doma⁡fcoda⁡g2nd⁡gdoma⁡fdoma⁡g∙˙coda⁡g2nd⁡f=∅
26 24 25 eqtrdi ⊢¬C∈Cat→g∈A,f∈h∈A|coda⁡h=doma⁡g⟼doma⁡fcoda⁡g2nd⁡gdoma⁡fdoma⁡g∙˙coda⁡g2nd⁡f=∅
27 18 26 eqtr4d ⊢¬C∈Cat→compa⁡C=g∈A,f∈h∈A|coda⁡h=doma⁡g⟼doma⁡fcoda⁡g2nd⁡gdoma⁡fdoma⁡g∙˙coda⁡g2nd⁡f
28 17 27 pm2.61i ⊢compa⁡C=g∈A,f∈h∈A|coda⁡h=doma⁡g⟼doma⁡fcoda⁡g2nd⁡gdoma⁡fdoma⁡g∙˙coda⁡g2nd⁡f
29 1 28 eqtri ⊢·˙=g∈A,f∈h∈A|coda⁡h=doma⁡g⟼doma⁡fcoda⁡g2nd⁡gdoma⁡fdoma⁡g∙˙coda⁡g2nd⁡f