Description: Lemma for trlsegvdeg . (Contributed by AV, 21-Feb-2021)
Ref | Expression | ||
---|---|---|---|
Hypotheses | 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 | trlsegvdeglem7 | ⊢ ( 𝜑 → dom ( iEdg ‘ 𝑌 ) ∈ Fin ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | trlsegvdeg.v | ⊢ 𝑉 = ( Vtx ‘ 𝐺 ) | |
2 | trlsegvdeg.i | ⊢ 𝐼 = ( iEdg ‘ 𝐺 ) | |
3 | trlsegvdeg.f | ⊢ ( 𝜑 → Fun 𝐼 ) | |
4 | trlsegvdeg.n | ⊢ ( 𝜑 → 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) | |
5 | trlsegvdeg.u | ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 ) | |
6 | trlsegvdeg.w | ⊢ ( 𝜑 → 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ) | |
7 | trlsegvdeg.vx | ⊢ ( 𝜑 → ( Vtx ‘ 𝑋 ) = 𝑉 ) | |
8 | trlsegvdeg.vy | ⊢ ( 𝜑 → ( Vtx ‘ 𝑌 ) = 𝑉 ) | |
9 | trlsegvdeg.vz | ⊢ ( 𝜑 → ( Vtx ‘ 𝑍 ) = 𝑉 ) | |
10 | trlsegvdeg.ix | ⊢ ( 𝜑 → ( iEdg ‘ 𝑋 ) = ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ) ) | |
11 | trlsegvdeg.iy | ⊢ ( 𝜑 → ( iEdg ‘ 𝑌 ) = { 〈 ( 𝐹 ‘ 𝑁 ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑁 ) ) 〉 } ) | |
12 | trlsegvdeg.iz | ⊢ ( 𝜑 → ( iEdg ‘ 𝑍 ) = ( 𝐼 ↾ ( 𝐹 “ ( 0 ... 𝑁 ) ) ) ) | |
13 | 1 2 3 4 5 6 7 8 9 10 11 12 | trlsegvdeglem5 | ⊢ ( 𝜑 → dom ( iEdg ‘ 𝑌 ) = { ( 𝐹 ‘ 𝑁 ) } ) |
14 | snfi | ⊢ { ( 𝐹 ‘ 𝑁 ) } ∈ Fin | |
15 | 13 14 | eqeltrdi | ⊢ ( 𝜑 → dom ( iEdg ‘ 𝑌 ) ∈ Fin ) |