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 ⊢ · ˙ = comp a ⁡ C
coafval.a ⊢ A = Arrow ⁡ C
coafval.x ⊢ ∙ ˙ = comp ⁡ C
Assertion coafval ⊢ · ˙ = g ∈ A , f ∈ h ∈ A | cod a ⁡ h = dom a ⁡ g ⟼ dom a ⁡ f cod a ⁡ g 2 nd ⁡ g dom a ⁡ f dom a ⁡ g ∙ ˙ cod a ⁡ g 2 nd ⁡ f

Proof

Step Hyp Ref Expression
1 coafval.o ⊢ · ˙ = comp a ⁡ 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 | cod a ⁡ h = dom a ⁡ g = h ∈ A | cod a ⁡ h = dom a ⁡ g
7 fveq2 ⊢ c = C → comp ⁡ c = comp ⁡ C
8 7 3 eqtr4di ⊢ c = C → comp ⁡ c = ∙ ˙
9 8 oveqd ⊢ c = C → dom a ⁡ f dom a ⁡ g comp ⁡ c cod a ⁡ g = dom a ⁡ f dom a ⁡ g ∙ ˙ cod a ⁡ g
10 9 oveqd ⊢ c = C → 2 nd ⁡ g dom a ⁡ f dom a ⁡ g comp ⁡ c cod a ⁡ g 2 nd ⁡ f = 2 nd ⁡ g dom a ⁡ f dom a ⁡ g ∙ ˙ cod a ⁡ g 2 nd ⁡ f
11 10 oteq3d ⊢ c = C → dom a ⁡ f cod a ⁡ g 2 nd ⁡ g dom a ⁡ f dom a ⁡ g comp ⁡ c cod a ⁡ g 2 nd ⁡ f = dom a ⁡ f cod a ⁡ g 2 nd ⁡ g dom a ⁡ f dom a ⁡ g ∙ ˙ cod a ⁡ g 2 nd ⁡ f
12 5 6 11 mpoeq123dv ⊢ c = C → g ∈ Arrow ⁡ c , f ∈ h ∈ Arrow ⁡ c | cod a ⁡ h = dom a ⁡ g ⟼ dom a ⁡ f cod a ⁡ g 2 nd ⁡ g dom a ⁡ f dom a ⁡ g comp ⁡ c cod a ⁡ g 2 nd ⁡ f = g ∈ A , f ∈ h ∈ A | cod a ⁡ h = dom a ⁡ g ⟼ dom a ⁡ f cod a ⁡ g 2 nd ⁡ g dom a ⁡ f dom a ⁡ g ∙ ˙ cod a ⁡ g 2 nd ⁡ f
13 df-coa ⊢ comp a = c ∈ Cat ⟼ g ∈ Arrow ⁡ c , f ∈ h ∈ Arrow ⁡ c | cod a ⁡ h = dom a ⁡ g ⟼ dom a ⁡ f cod a ⁡ g 2 nd ⁡ g dom a ⁡ f dom a ⁡ g comp ⁡ c cod a ⁡ g 2 nd ⁡ f
14 2 fvexi ⊢ A ∈ V
15 14 rabex ⊢ h ∈ A | cod a ⁡ h = dom a ⁡ g ∈ V
16 14 15 mpoex ⊢ g ∈ A , f ∈ h ∈ A | cod a ⁡ h = dom a ⁡ g ⟼ dom a ⁡ f cod a ⁡ g 2 nd ⁡ g dom a ⁡ f dom a ⁡ g ∙ ˙ cod a ⁡ g 2 nd ⁡ f ∈ V
17 12 13 16 fvmpt ⊢ C ∈ Cat → comp a ⁡ C = g ∈ A , f ∈ h ∈ A | cod a ⁡ h = dom a ⁡ g ⟼ dom a ⁡ f cod a ⁡ g 2 nd ⁡ g dom a ⁡ f dom a ⁡ g ∙ ˙ cod a ⁡ g 2 nd ⁡ f
18 13 fvmptndm ⊢ ¬ C ∈ Cat → comp a ⁡ 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 | cod a ⁡ h = dom a ⁡ g = h ∈ A | cod a ⁡ h = dom a ⁡ g
23 eqidd ⊢ ¬ C ∈ Cat → dom a ⁡ f cod a ⁡ g 2 nd ⁡ g dom a ⁡ f dom a ⁡ g ∙ ˙ cod a ⁡ g 2 nd ⁡ f = dom a ⁡ f cod a ⁡ g 2 nd ⁡ g dom a ⁡ f dom a ⁡ g ∙ ˙ cod a ⁡ g 2 nd ⁡ f
24 21 22 23 mpoeq123dv ⊢ ¬ C ∈ Cat → g ∈ A , f ∈ h ∈ A | cod a ⁡ h = dom a ⁡ g ⟼ dom a ⁡ f cod a ⁡ g 2 nd ⁡ g dom a ⁡ f dom a ⁡ g ∙ ˙ cod a ⁡ g 2 nd ⁡ f = g ∈ ∅ , f ∈ h ∈ A | cod a ⁡ h = dom a ⁡ g ⟼ dom a ⁡ f cod a ⁡ g 2 nd ⁡ g dom a ⁡ f dom a ⁡ g ∙ ˙ cod a ⁡ g 2 nd ⁡ f
25 mpo0 ⊢ g ∈ ∅ , f ∈ h ∈ A | cod a ⁡ h = dom a ⁡ g ⟼ dom a ⁡ f cod a ⁡ g 2 nd ⁡ g dom a ⁡ f dom a ⁡ g ∙ ˙ cod a ⁡ g 2 nd ⁡ f = ∅
26 24 25 eqtrdi ⊢ ¬ C ∈ Cat → g ∈ A , f ∈ h ∈ A | cod a ⁡ h = dom a ⁡ g ⟼ dom a ⁡ f cod a ⁡ g 2 nd ⁡ g dom a ⁡ f dom a ⁡ g ∙ ˙ cod a ⁡ g 2 nd ⁡ f = ∅
27 18 26 eqtr4d ⊢ ¬ C ∈ Cat → comp a ⁡ C = g ∈ A , f ∈ h ∈ A | cod a ⁡ h = dom a ⁡ g ⟼ dom a ⁡ f cod a ⁡ g 2 nd ⁡ g dom a ⁡ f dom a ⁡ g ∙ ˙ cod a ⁡ g 2 nd ⁡ f
28 17 27 pm2.61i ⊢ comp a ⁡ C = g ∈ A , f ∈ h ∈ A | cod a ⁡ h = dom a ⁡ g ⟼ dom a ⁡ f cod a ⁡ g 2 nd ⁡ g dom a ⁡ f dom a ⁡ g ∙ ˙ cod a ⁡ g 2 nd ⁡ f
29 1 28 eqtri ⊢ · ˙ = g ∈ A , f ∈ h ∈ A | cod a ⁡ h = dom a ⁡ g ⟼ dom a ⁡ f cod a ⁡ g 2 nd ⁡ g dom a ⁡ f dom a ⁡ g ∙ ˙ cod a ⁡ g 2 nd ⁡ f