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=x∈0..^P−1⟼E-1⁡P⁡xP⁡x+1
wlkiswwlks2lem.e ⊢E=iEdg⁡G
Assertion wlkiswwlks2lem6 ⊢G∈USHGraph∧P∈WordV∧1≤P→∀i∈0..^P−1P⁡iP⁡i+1∈ran⁡E→F∈Worddom⁡E∧P:0…F⟶V∧∀i∈0..^FE⁡F⁡i=P⁡iP⁡i+1

Proof

Step Hyp Ref Expression
1 wlkiswwlks2lem.f ⊢F=x∈0..^P−1⟼E-1⁡P⁡xP⁡x+1
2 wlkiswwlks2lem.e ⊢E=iEdg⁡G
3 1 2 wlkiswwlks2lem5 ⊢G∈USHGraph∧P∈WordV∧1≤P→∀i∈0..^P−1P⁡iP⁡i+1∈ran⁡E→F∈Worddom⁡E
4 3 imp ⊢G∈USHGraph∧P∈WordV∧1≤P∧∀i∈0..^P−1P⁡iP⁡i+1∈ran⁡E→F∈Worddom⁡E
5 1 wlkiswwlks2lem3 ⊢P∈WordV∧1≤P→P:0…F⟶V
6 5 3adant1 ⊢G∈USHGraph∧P∈WordV∧1≤P→P:0…F⟶V
7 6 adantr ⊢G∈USHGraph∧P∈WordV∧1≤P∧∀i∈0..^P−1P⁡iP⁡i+1∈ran⁡E→P:0…F⟶V
8 1 2 wlkiswwlks2lem4 ⊢G∈USHGraph∧P∈WordV∧1≤P→∀i∈0..^P−1P⁡iP⁡i+1∈ran⁡E→∀i∈0..^FE⁡F⁡i=P⁡iP⁡i+1
9 8 imp ⊢G∈USHGraph∧P∈WordV∧1≤P∧∀i∈0..^P−1P⁡iP⁡i+1∈ran⁡E→∀i∈0..^FE⁡F⁡i=P⁡iP⁡i+1
10 4 7 9 3jca ⊢G∈USHGraph∧P∈WordV∧1≤P∧∀i∈0..^P−1P⁡iP⁡i+1∈ran⁡E→F∈Worddom⁡E∧P:0…F⟶V∧∀i∈0..^FE⁡F⁡i=P⁡iP⁡i+1
11 10 ex ⊢G∈USHGraph∧P∈WordV∧1≤P→∀i∈0..^P−1P⁡iP⁡i+1∈ran⁡E→F∈Worddom⁡E∧P:0…F⟶V∧∀i∈0..^FE⁡F⁡i=P⁡iP⁡i+1