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

Theorem trlsegvdeglem2 29474
Description: Lemma for trlsegvdeg 29480. (Contributed by AV, 20-Feb-2021.)
Hypotheses
Ref Expression
trlsegvdeg.v 𝑉 = (Vtxβ€˜πΊ)
trlsegvdeg.i 𝐼 = (iEdgβ€˜πΊ)
trlsegvdeg.f (πœ‘ β†’ Fun 𝐼)
trlsegvdeg.n (πœ‘ β†’ 𝑁 ∈ (0..^(β™―β€˜πΉ)))
trlsegvdeg.u (πœ‘ β†’ π‘ˆ ∈ 𝑉)
trlsegvdeg.w (πœ‘ β†’ 𝐹(Trailsβ€˜πΊ)𝑃)
trlsegvdeg.vx (πœ‘ β†’ (Vtxβ€˜π‘‹) = 𝑉)
trlsegvdeg.vy (πœ‘ β†’ (Vtxβ€˜π‘Œ) = 𝑉)
trlsegvdeg.vz (πœ‘ β†’ (Vtxβ€˜π‘) = 𝑉)
trlsegvdeg.ix (πœ‘ β†’ (iEdgβ€˜π‘‹) = (𝐼 β†Ύ (𝐹 β€œ (0..^𝑁))))
trlsegvdeg.iy (πœ‘ β†’ (iEdgβ€˜π‘Œ) = {⟨(πΉβ€˜π‘), (πΌβ€˜(πΉβ€˜π‘))⟩})
trlsegvdeg.iz (πœ‘ β†’ (iEdgβ€˜π‘) = (𝐼 β†Ύ (𝐹 β€œ (0...𝑁))))
Assertion
Ref Expression
trlsegvdeglem2 (πœ‘ β†’ Fun (iEdgβ€˜π‘‹))

Proof of Theorem trlsegvdeglem2
StepHypRef Expression
1 trlsegvdeg.f . . 3 (πœ‘ β†’ Fun 𝐼)
21funresd 6592 . 2 (πœ‘ β†’ Fun (𝐼 β†Ύ (𝐹 β€œ (0..^𝑁))))
3 trlsegvdeg.ix . . 3 (πœ‘ β†’ (iEdgβ€˜π‘‹) = (𝐼 β†Ύ (𝐹 β€œ (0..^𝑁))))
43funeqd 6571 . 2 (πœ‘ β†’ (Fun (iEdgβ€˜π‘‹) ↔ Fun (𝐼 β†Ύ (𝐹 β€œ (0..^𝑁)))))
52, 4mpbird 257 1 (πœ‘ β†’ Fun (iEdgβ€˜π‘‹))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   = wceq 1542   ∈ wcel 2107  {csn 4629  βŸ¨cop 4635   class class class wbr 5149   β†Ύ cres 5679   β€œ cima 5680  Fun wfun 6538  β€˜cfv 6544  (class class class)co 7409  0cc0 11110  ...cfz 13484  ..^cfzo 13627  β™―chash 14290  Vtxcvtx 28256  iEdgciedg 28257  Trailsctrls 28947
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966  df-br 5150  df-opab 5212  df-rel 5684  df-cnv 5685  df-co 5686  df-res 5689  df-fun 6546
This theorem is referenced by:  trlsegvdeg  29480
  Copyright terms: Public domain W3C validator