Theorem trlsegvdeglem2 30837

Description: Lemma for trlsegvdeg 30843. (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

Step	Hyp	Ref	Expression
1		trlsegvdeg.f	. . 3 ⊢ (𝜑 → Fun 𝐼)
2	1	funresd 6592	. 2 ⊢ (𝜑 → Fun (𝐼 ↾ (𝐹 “ (0..^𝑁))))
3		trlsegvdeg.ix	. . 3 ⊢ (𝜑 → (iEdg‘𝑋) = (𝐼 ↾ (𝐹 “ (0..^𝑁))))
4	3	funeqd 6570	. 2 ⊢ (𝜑 → (Fun (iEdg‘𝑋) ↔ Fun (𝐼 ↾ (𝐹 “ (0..^𝑁)))))
5	2, 4	mpbird 260	1 ⊢ (𝜑 → Fun (iEdg‘𝑋))

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2146  {csn 4588  ⟨cop 4838   class class class wbr 5106   ↾ cres 5657   “ cima 5658  Fun wfun 6541  ‘cfv 6547  (class class class)co 7430  0cc0 11213  ...cfz 13652  ..^cfzo 13801  ♯chash 14487  Vtxcvtx 29589  iEdgciedg 29590  Trailsctrls 30288

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-in 4094  df-br 5107  df-opab 5171  df-rel 5662  df-cnv 5663  df-co 5664  df-res 5667  df-fun 6549

This theorem is used by:  trlsegvdeg  30843