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

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 2 uspgrf1oedg ⊢G∈USHGraph→E:dom⁡E⟶1-1 ontoEdg⁡G
4 2 rneqi ⊢ran⁡E=ran⁡iEdg⁡G
5 edgval ⊢Edg⁡G=ran⁡iEdg⁡G
6 4 5 eqtr4i ⊢ran⁡E=Edg⁡G
7 6 a1i ⊢G∈USHGraph→ran⁡E=Edg⁡G
8 7 f1oeq3d ⊢G∈USHGraph→E:dom⁡E⟶1-1 ontoran⁡E↔E:dom⁡E⟶1-1 ontoEdg⁡G
9 3 8 mpbird ⊢G∈USHGraph→E:dom⁡E⟶1-1 ontoran⁡E
10 9 3ad2ant1 ⊢G∈USHGraph∧P∈WordV∧1≤P→E:dom⁡E⟶1-1 ontoran⁡E
11 10 ad2antrr ⊢G∈USHGraph∧P∈WordV∧1≤P∧∀i∈0..^P−1P⁡iP⁡i+1∈ran⁡E∧x∈0..^P−1→E:dom⁡E⟶1-1 ontoran⁡E
12 simpr ⊢G∈USHGraph∧P∈WordV∧1≤P∧x∈0..^P−1→x∈0..^P−1
13 fveq2 ⊢i=x→P⁡i=P⁡x
14 fvoveq1 ⊢i=x→P⁡i+1=P⁡x+1
15 13 14 preq12d ⊢i=x→P⁡iP⁡i+1=P⁡xP⁡x+1
16 15 eleq1d ⊢i=x→P⁡iP⁡i+1∈ran⁡E↔P⁡xP⁡x+1∈ran⁡E
17 16 adantl ⊢G∈USHGraph∧P∈WordV∧1≤P∧x∈0..^P−1∧i=x→P⁡iP⁡i+1∈ran⁡E↔P⁡xP⁡x+1∈ran⁡E
18 12 17 rspcdv ⊢G∈USHGraph∧P∈WordV∧1≤P∧x∈0..^P−1→∀i∈0..^P−1P⁡iP⁡i+1∈ran⁡E→P⁡xP⁡x+1∈ran⁡E
19 18 impancom ⊢G∈USHGraph∧P∈WordV∧1≤P∧∀i∈0..^P−1P⁡iP⁡i+1∈ran⁡E→x∈0..^P−1→P⁡xP⁡x+1∈ran⁡E
20 19 imp ⊢G∈USHGraph∧P∈WordV∧1≤P∧∀i∈0..^P−1P⁡iP⁡i+1∈ran⁡E∧x∈0..^P−1→P⁡xP⁡x+1∈ran⁡E
21 f1ocnvdm ⊢E:dom⁡E⟶1-1 ontoran⁡E∧P⁡xP⁡x+1∈ran⁡E→E-1⁡P⁡xP⁡x+1∈dom⁡E
22 11 20 21 syl2anc ⊢G∈USHGraph∧P∈WordV∧1≤P∧∀i∈0..^P−1P⁡iP⁡i+1∈ran⁡E∧x∈0..^P−1→E-1⁡P⁡xP⁡x+1∈dom⁡E
23 22 1 fmptd ⊢G∈USHGraph∧P∈WordV∧1≤P∧∀i∈0..^P−1P⁡iP⁡i+1∈ran⁡E→F:0..^P−1⟶dom⁡E
24 iswrdi ⊢F:0..^P−1⟶dom⁡E→F∈Worddom⁡E
25 23 24 syl ⊢G∈USHGraph∧P∈WordV∧1≤P∧∀i∈0..^P−1P⁡iP⁡i+1∈ran⁡E→F∈Worddom⁡E
26 25 ex ⊢G∈USHGraph∧P∈WordV∧1≤P→∀i∈0..^P−1P⁡iP⁡i+1∈ran⁡E→F∈Worddom⁡E