Metamath Proof Explorer


Theorem wlkiswwlks2lem6

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

Ref Expression
Hypotheses wlkiswwlks2lem.f F=x0..^P1E-1PxPx+1
wlkiswwlks2lem.e E=iEdgG
Assertion wlkiswwlks2lem6 GUSHGraphPWordV1Pi0..^P1PiPi+1ranEFWorddomEP:0FVi0..^FEFi=PiPi+1

Proof

Step Hyp Ref Expression
1 wlkiswwlks2lem.f F=x0..^P1E-1PxPx+1
2 wlkiswwlks2lem.e E=iEdgG
3 1 2 wlkiswwlks2lem5 GUSHGraphPWordV1Pi0..^P1PiPi+1ranEFWorddomE
4 3 imp GUSHGraphPWordV1Pi0..^P1PiPi+1ranEFWorddomE
5 1 wlkiswwlks2lem3 PWordV1PP:0FV
6 5 3adant1 GUSHGraphPWordV1PP:0FV
7 6 adantr GUSHGraphPWordV1Pi0..^P1PiPi+1ranEP:0FV
8 1 2 wlkiswwlks2lem4 GUSHGraphPWordV1Pi0..^P1PiPi+1ranEi0..^FEFi=PiPi+1
9 8 imp GUSHGraphPWordV1Pi0..^P1PiPi+1ranEi0..^FEFi=PiPi+1
10 4 7 9 3jca GUSHGraphPWordV1Pi0..^P1PiPi+1ranEFWorddomEP:0FVi0..^FEFi=PiPi+1
11 10 ex GUSHGraphPWordV1Pi0..^P1PiPi+1ranEFWorddomEP:0FVi0..^FEFi=PiPi+1