Metamath Proof Explorer


Theorem wlkiswwlks2lem5

Description: Lemma 5 for wlkiswwlks2 . (Contributed by Alexander van der Vekens, 21-Jul-2018) (Revised by AV, 10-Apr-2021)

Ref Expression
Hypotheses wlkiswwlks2lem.f 𝐹 = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ ( 𝐸 ‘ { ( 𝑃𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) )
wlkiswwlks2lem.e 𝐸 = ( iEdg ‘ 𝐺 )
Assertion wlkiswwlks2lem5 ( ( 𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ ( ♯ ‘ 𝑃 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸𝐹 ∈ Word dom 𝐸 ) )

Proof

Step Hyp Ref Expression
1 wlkiswwlks2lem.f 𝐹 = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ ( 𝐸 ‘ { ( 𝑃𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) )
2 wlkiswwlks2lem.e 𝐸 = ( iEdg ‘ 𝐺 )
3 2 uspgrf1oedg ( 𝐺 ∈ USPGraph → 𝐸 : dom 𝐸1-1-onto→ ( Edg ‘ 𝐺 ) )
4 2 rneqi ran 𝐸 = ran ( iEdg ‘ 𝐺 )
5 edgval ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 )
6 4 5 eqtr4i ran 𝐸 = ( Edg ‘ 𝐺 )
7 6 a1i ( 𝐺 ∈ USPGraph → ran 𝐸 = ( Edg ‘ 𝐺 ) )
8 7 f1oeq3d ( 𝐺 ∈ USPGraph → ( 𝐸 : dom 𝐸1-1-onto→ ran 𝐸𝐸 : dom 𝐸1-1-onto→ ( Edg ‘ 𝐺 ) ) )
9 3 8 mpbird ( 𝐺 ∈ USPGraph → 𝐸 : dom 𝐸1-1-onto→ ran 𝐸 )
10 9 3ad2ant1 ( ( 𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ ( ♯ ‘ 𝑃 ) ) → 𝐸 : dom 𝐸1-1-onto→ ran 𝐸 )
11 10 ad2antrr ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ ( ♯ ‘ 𝑃 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) → 𝐸 : dom 𝐸1-1-onto→ ran 𝐸 )
12 simpr ( ( ( 𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) → 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) )
13 fveq2 ( 𝑖 = 𝑥 → ( 𝑃𝑖 ) = ( 𝑃𝑥 ) )
14 fvoveq1 ( 𝑖 = 𝑥 → ( 𝑃 ‘ ( 𝑖 + 1 ) ) = ( 𝑃 ‘ ( 𝑥 + 1 ) ) )
15 13 14 preq12d ( 𝑖 = 𝑥 → { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } = { ( 𝑃𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } )
16 15 eleq1d ( 𝑖 = 𝑥 → ( { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ↔ { ( 𝑃𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ∈ ran 𝐸 ) )
17 16 adantl ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) ∧ 𝑖 = 𝑥 ) → ( { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ↔ { ( 𝑃𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ∈ ran 𝐸 ) )
18 12 17 rspcdv ( ( ( 𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 → { ( 𝑃𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ∈ ran 𝐸 ) )
19 18 impancom ( ( ( 𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ ( ♯ ‘ 𝑃 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ) → ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) → { ( 𝑃𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ∈ ran 𝐸 ) )
20 19 imp ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ ( ♯ ‘ 𝑃 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) → { ( 𝑃𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ∈ ran 𝐸 )
21 f1ocnvdm ( ( 𝐸 : dom 𝐸1-1-onto→ ran 𝐸 ∧ { ( 𝑃𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ∈ ran 𝐸 ) → ( 𝐸 ‘ { ( 𝑃𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) ∈ dom 𝐸 )
22 11 20 21 syl2anc ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ ( ♯ ‘ 𝑃 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) → ( 𝐸 ‘ { ( 𝑃𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) ∈ dom 𝐸 )
23 22 1 fmptd ( ( ( 𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ ( ♯ ‘ 𝑃 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ) → 𝐹 : ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ⟶ dom 𝐸 )
24 iswrdi ( 𝐹 : ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ⟶ dom 𝐸𝐹 ∈ Word dom 𝐸 )
25 23 24 syl ( ( ( 𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ ( ♯ ‘ 𝑃 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ) → 𝐹 ∈ Word dom 𝐸 )
26 25 ex ( ( 𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ ( ♯ ‘ 𝑃 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸𝐹 ∈ Word dom 𝐸 ) )