Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  coafval Structured version   Visualization version   GIF version

Theorem coafval 16886
 Description: The value of the composition of arrows. (Contributed by Mario Carneiro, 11-Jan-2017.)
Hypotheses
Ref Expression
coafval.o · = (compa𝐶)
coafval.a 𝐴 = (Arrow‘𝐶)
coafval.x = (comp‘𝐶)
Assertion
Ref Expression
coafval · = (𝑔𝐴, 𝑓 ∈ {𝐴 ∣ (coda) = (doma𝑔)} ↦ ⟨(doma𝑓), (coda𝑔), ((2nd𝑔)(⟨(doma𝑓), (doma𝑔)⟩ (coda𝑔))(2nd𝑓))⟩)
Distinct variable groups:   𝑓,𝑔,,𝐴   𝐶,𝑓,𝑔,
Allowed substitution hints:   (𝑓,𝑔,)   · (𝑓,𝑔,)

Proof of Theorem coafval
Dummy variable 𝑐 is distinct from all other variables.
StepHypRef Expression
1 coafval.o . 2 · = (compa𝐶)
2 fveq2 6340 . . . . . 6 (𝑐 = 𝐶 → (Arrow‘𝑐) = (Arrow‘𝐶))
3 coafval.a . . . . . 6 𝐴 = (Arrow‘𝐶)
42, 3syl6eqr 2800 . . . . 5 (𝑐 = 𝐶 → (Arrow‘𝑐) = 𝐴)
54rabeqdv 3322 . . . . 5 (𝑐 = 𝐶 → { ∈ (Arrow‘𝑐) ∣ (coda) = (doma𝑔)} = {𝐴 ∣ (coda) = (doma𝑔)})
6 fveq2 6340 . . . . . . . . 9 (𝑐 = 𝐶 → (comp‘𝑐) = (comp‘𝐶))
7 coafval.x . . . . . . . . 9 = (comp‘𝐶)
86, 7syl6eqr 2800 . . . . . . . 8 (𝑐 = 𝐶 → (comp‘𝑐) = )
98oveqd 6818 . . . . . . 7 (𝑐 = 𝐶 → (⟨(doma𝑓), (doma𝑔)⟩(comp‘𝑐)(coda𝑔)) = (⟨(doma𝑓), (doma𝑔)⟩ (coda𝑔)))
109oveqd 6818 . . . . . 6 (𝑐 = 𝐶 → ((2nd𝑔)(⟨(doma𝑓), (doma𝑔)⟩(comp‘𝑐)(coda𝑔))(2nd𝑓)) = ((2nd𝑔)(⟨(doma𝑓), (doma𝑔)⟩ (coda𝑔))(2nd𝑓)))
1110oteq3d 4555 . . . . 5 (𝑐 = 𝐶 → ⟨(doma𝑓), (coda𝑔), ((2nd𝑔)(⟨(doma𝑓), (doma𝑔)⟩(comp‘𝑐)(coda𝑔))(2nd𝑓))⟩ = ⟨(doma𝑓), (coda𝑔), ((2nd𝑔)(⟨(doma𝑓), (doma𝑔)⟩ (coda𝑔))(2nd𝑓))⟩)
124, 5, 11mpt2eq123dv 6870 . . . 4 (𝑐 = 𝐶 → (𝑔 ∈ (Arrow‘𝑐), 𝑓 ∈ { ∈ (Arrow‘𝑐) ∣ (coda) = (doma𝑔)} ↦ ⟨(doma𝑓), (coda𝑔), ((2nd𝑔)(⟨(doma𝑓), (doma𝑔)⟩(comp‘𝑐)(coda𝑔))(2nd𝑓))⟩) = (𝑔𝐴, 𝑓 ∈ {𝐴 ∣ (coda) = (doma𝑔)} ↦ ⟨(doma𝑓), (coda𝑔), ((2nd𝑔)(⟨(doma𝑓), (doma𝑔)⟩ (coda𝑔))(2nd𝑓))⟩))
13 df-coa 16878 . . . 4 compa = (𝑐 ∈ Cat ↦ (𝑔 ∈ (Arrow‘𝑐), 𝑓 ∈ { ∈ (Arrow‘𝑐) ∣ (coda) = (doma𝑔)} ↦ ⟨(doma𝑓), (coda𝑔), ((2nd𝑔)(⟨(doma𝑓), (doma𝑔)⟩(comp‘𝑐)(coda𝑔))(2nd𝑓))⟩))
14 fvex 6350 . . . . . 6 (Arrow‘𝐶) ∈ V
153, 14eqeltri 2823 . . . . 5 𝐴 ∈ V
1615rabex 4952 . . . . 5 {𝐴 ∣ (coda) = (doma𝑔)} ∈ V
1715, 16mpt2ex 7403 . . . 4 (𝑔𝐴, 𝑓 ∈ {𝐴 ∣ (coda) = (doma𝑔)} ↦ ⟨(doma𝑓), (coda𝑔), ((2nd𝑔)(⟨(doma𝑓), (doma𝑔)⟩ (coda𝑔))(2nd𝑓))⟩) ∈ V
1812, 13, 17fvmpt 6432 . . 3 (𝐶 ∈ Cat → (compa𝐶) = (𝑔𝐴, 𝑓 ∈ {𝐴 ∣ (coda) = (doma𝑔)} ↦ ⟨(doma𝑓), (coda𝑔), ((2nd𝑔)(⟨(doma𝑓), (doma𝑔)⟩ (coda𝑔))(2nd𝑓))⟩))
1913dmmptss 5780 . . . . . . 7 dom compa ⊆ Cat
2019sseli 3728 . . . . . 6 (𝐶 ∈ dom compa𝐶 ∈ Cat)
2120con3i 150 . . . . 5 𝐶 ∈ Cat → ¬ 𝐶 ∈ dom compa)
22 ndmfv 6367 . . . . 5 𝐶 ∈ dom compa → (compa𝐶) = ∅)
2321, 22syl 17 . . . 4 𝐶 ∈ Cat → (compa𝐶) = ∅)
243arwrcl 16866 . . . . . . . 8 (𝑓𝐴𝐶 ∈ Cat)
2524con3i 150 . . . . . . 7 𝐶 ∈ Cat → ¬ 𝑓𝐴)
2625eq0rdv 4110 . . . . . 6 𝐶 ∈ Cat → 𝐴 = ∅)
27 eqidd 2749 . . . . . 6 𝐶 ∈ Cat → {𝐴 ∣ (coda) = (doma𝑔)} = {𝐴 ∣ (coda) = (doma𝑔)})
28 eqidd 2749 . . . . . 6 𝐶 ∈ Cat → ⟨(doma𝑓), (coda𝑔), ((2nd𝑔)(⟨(doma𝑓), (doma𝑔)⟩ (coda𝑔))(2nd𝑓))⟩ = ⟨(doma𝑓), (coda𝑔), ((2nd𝑔)(⟨(doma𝑓), (doma𝑔)⟩ (coda𝑔))(2nd𝑓))⟩)
2926, 27, 28mpt2eq123dv 6870 . . . . 5 𝐶 ∈ Cat → (𝑔𝐴, 𝑓 ∈ {𝐴 ∣ (coda) = (doma𝑔)} ↦ ⟨(doma𝑓), (coda𝑔), ((2nd𝑔)(⟨(doma𝑓), (doma𝑔)⟩ (coda𝑔))(2nd𝑓))⟩) = (𝑔 ∈ ∅, 𝑓 ∈ {𝐴 ∣ (coda) = (doma𝑔)} ↦ ⟨(doma𝑓), (coda𝑔), ((2nd𝑔)(⟨(doma𝑓), (doma𝑔)⟩ (coda𝑔))(2nd𝑓))⟩))
30 mpt20 6878 . . . . 5 (𝑔 ∈ ∅, 𝑓 ∈ {𝐴 ∣ (coda) = (doma𝑔)} ↦ ⟨(doma𝑓), (coda𝑔), ((2nd𝑔)(⟨(doma𝑓), (doma𝑔)⟩ (coda𝑔))(2nd𝑓))⟩) = ∅
3129, 30syl6eq 2798 . . . 4 𝐶 ∈ Cat → (𝑔𝐴, 𝑓 ∈ {𝐴 ∣ (coda) = (doma𝑔)} ↦ ⟨(doma𝑓), (coda𝑔), ((2nd𝑔)(⟨(doma𝑓), (doma𝑔)⟩ (coda𝑔))(2nd𝑓))⟩) = ∅)
3223, 31eqtr4d 2785 . . 3 𝐶 ∈ Cat → (compa𝐶) = (𝑔𝐴, 𝑓 ∈ {𝐴 ∣ (coda) = (doma𝑔)} ↦ ⟨(doma𝑓), (coda𝑔), ((2nd𝑔)(⟨(doma𝑓), (doma𝑔)⟩ (coda𝑔))(2nd𝑓))⟩))
3318, 32pm2.61i 176 . 2 (compa𝐶) = (𝑔𝐴, 𝑓 ∈ {𝐴 ∣ (coda) = (doma𝑔)} ↦ ⟨(doma𝑓), (coda𝑔), ((2nd𝑔)(⟨(doma𝑓), (doma𝑔)⟩ (coda𝑔))(2nd𝑓))⟩)
341, 33eqtri 2770 1 · = (𝑔𝐴, 𝑓 ∈ {𝐴 ∣ (coda) = (doma𝑔)} ↦ ⟨(doma𝑓), (coda𝑔), ((2nd𝑔)(⟨(doma𝑓), (doma𝑔)⟩ (coda𝑔))(2nd𝑓))⟩)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   = wceq 1620   ∈ wcel 2127  {crab 3042  Vcvv 3328  ∅c0 4046  ⟨cop 4315  ⟨cotp 4317  dom cdm 5254  ‘cfv 6037  (class class class)co 6801   ↦ cmpt2 6803  2nd c2nd 7320  compcco 16126  Catccat 16497  domacdoma 16842  codaccoda 16843  Arrowcarw 16844  compaccoa 16876 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-8 2129  ax-9 2136  ax-10 2156  ax-11 2171  ax-12 2184  ax-13 2379  ax-ext 2728  ax-rep 4911  ax-sep 4921  ax-nul 4929  ax-pow 4980  ax-pr 5043  ax-un 7102 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1623  df-ex 1842  df-nf 1847  df-sb 2035  df-eu 2599  df-mo 2600  df-clab 2735  df-cleq 2741  df-clel 2744  df-nfc 2879  df-ne 2921  df-ral 3043  df-rex 3044  df-reu 3045  df-rab 3047  df-v 3330  df-sbc 3565  df-csb 3663  df-dif 3706  df-un 3708  df-in 3710  df-ss 3717  df-nul 4047  df-if 4219  df-pw 4292  df-sn 4310  df-pr 4312  df-op 4316  df-ot 4318  df-uni 4577  df-iun 4662  df-br 4793  df-opab 4853  df-mpt 4870  df-id 5162  df-xp 5260  df-rel 5261  df-cnv 5262  df-co 5263  df-dm 5264  df-rn 5265  df-res 5266  df-ima 5267  df-iota 6000  df-fun 6039  df-fn 6040  df-f 6041  df-f1 6042  df-fo 6043  df-f1o 6044  df-fv 6045  df-ov 6804  df-oprab 6805  df-mpt2 6806  df-1st 7321  df-2nd 7322  df-arw 16849  df-coa 16878 This theorem is referenced by:  eldmcoa  16887  dmcoass  16888  coaval  16890  coapm  16893
 Copyright terms: Public domain W3C validator