Metamath Proof Explorer

Theorem clwlkclwwlklem1

Description: Lemma 1 for clwlkclwwlk . (Contributed by Alexander van der Vekens, 22-Jun-2018) (Revised by AV, 11-Apr-2021)

Ref Expression
Assertion clwlkclwwlklem1 ⊢E:dom⁡E⟶1-1R∧P∈WordV∧2≤P→lastS⁡P=P⁡0∧∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E→∃ff∈Worddom⁡E∧P:0…f⟶V∧∀i∈0..^fE⁡f⁡i=P⁡iP⁡i+1∧P⁡0=P⁡f

Proof

Step Hyp Ref Expression
1 ovex ⊢0..^P−1∈V
2 mptexg ⊢0..^P−1∈V→x∈0..^P−1⟼ifx<P−2E-1⁡P⁡xP⁡x+1E-1⁡P⁡xP⁡0∈V
3 1 2 mp1i ⊢E:dom⁡E⟶1-1R∧P∈WordV∧2≤P→x∈0..^P−1⟼ifx<P−2E-1⁡P⁡xP⁡x+1E-1⁡P⁡xP⁡0∈V
4 eqid ⊢x∈0..^P−1⟼ifx<P−2E-1⁡P⁡xP⁡x+1E-1⁡P⁡xP⁡0=x∈0..^P−1⟼ifx<P−2E-1⁡P⁡xP⁡x+1E-1⁡P⁡xP⁡0
5 4 clwlkclwwlklem2a ⊢E:dom⁡E⟶1-1R∧P∈WordV∧2≤P→lastS⁡P=P⁡0∧∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E→x∈0..^P−1⟼ifx<P−2E-1⁡P⁡xP⁡x+1E-1⁡P⁡xP⁡0∈Worddom⁡E∧P:0…x∈0..^P−1⟼ifx<P−2E-1⁡P⁡xP⁡x+1E-1⁡P⁡xP⁡0⟶V∧∀i∈0..^x∈0..^P−1⟼ifx<P−2E-1⁡P⁡xP⁡x+1E-1⁡P⁡xP⁡0E⁡x∈0..^P−1⟼ifx<P−2E-1⁡P⁡xP⁡x+1E-1⁡P⁡xP⁡0⁡i=P⁡iP⁡i+1∧P⁡0=P⁡x∈0..^P−1⟼ifx<P−2E-1⁡P⁡xP⁡x+1E-1⁡P⁡xP⁡0
6 5 adantr ⊢E:dom⁡E⟶1-1R∧P∈WordV∧2≤P∧f=x∈0..^P−1⟼ifx<P−2E-1⁡P⁡xP⁡x+1E-1⁡P⁡xP⁡0→lastS⁡P=P⁡0∧∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E→x∈0..^P−1⟼ifx<P−2E-1⁡P⁡xP⁡x+1E-1⁡P⁡xP⁡0∈Worddom⁡E∧P:0…x∈0..^P−1⟼ifx<P−2E-1⁡P⁡xP⁡x+1E-1⁡P⁡xP⁡0⟶V∧∀i∈0..^x∈0..^P−1⟼ifx<P−2E-1⁡P⁡xP⁡x+1E-1⁡P⁡xP⁡0E⁡x∈0..^P−1⟼ifx<P−2E-1⁡P⁡xP⁡x+1E-1⁡P⁡xP⁡0⁡i=P⁡iP⁡i+1∧P⁡0=P⁡x∈0..^P−1⟼ifx<P−2E-1⁡P⁡xP⁡x+1E-1⁡P⁡xP⁡0
7 eleq1 ⊢f=x∈0..^P−1⟼ifx<P−2E-1⁡P⁡xP⁡x+1E-1⁡P⁡xP⁡0→f∈Worddom⁡E↔x∈0..^P−1⟼ifx<P−2E-1⁡P⁡xP⁡x+1E-1⁡P⁡xP⁡0∈Worddom⁡E
8 fveq2 ⊢f=x∈0..^P−1⟼ifx<P−2E-1⁡P⁡xP⁡x+1E-1⁡P⁡xP⁡0→f=x∈0..^P−1⟼ifx<P−2E-1⁡P⁡xP⁡x+1E-1⁡P⁡xP⁡0
9 8 oveq2d ⊢f=x∈0..^P−1⟼ifx<P−2E-1⁡P⁡xP⁡x+1E-1⁡P⁡xP⁡0→0…f=0…x∈0..^P−1⟼ifx<P−2E-1⁡P⁡xP⁡x+1E-1⁡P⁡xP⁡0
10 9 feq2d ⊢f=x∈0..^P−1⟼ifx<P−2E-1⁡P⁡xP⁡x+1E-1⁡P⁡xP⁡0→P:0…f⟶V↔P:0…x∈0..^P−1⟼ifx<P−2E-1⁡P⁡xP⁡x+1E-1⁡P⁡xP⁡0⟶V
11 8 oveq2d ⊢f=x∈0..^P−1⟼ifx<P−2E-1⁡P⁡xP⁡x+1E-1⁡P⁡xP⁡0→0..^f=0..^x∈0..^P−1⟼ifx<P−2E-1⁡P⁡xP⁡x+1E-1⁡P⁡xP⁡0
12 fveq1 ⊢f=x∈0..^P−1⟼ifx<P−2E-1⁡P⁡xP⁡x+1E-1⁡P⁡xP⁡0→f⁡i=x∈0..^P−1⟼ifx<P−2E-1⁡P⁡xP⁡x+1E-1⁡P⁡xP⁡0⁡i
13 12 fveqeq2d ⊢f=x∈0..^P−1⟼ifx<P−2E-1⁡P⁡xP⁡x+1E-1⁡P⁡xP⁡0→E⁡f⁡i=P⁡iP⁡i+1↔E⁡x∈0..^P−1⟼ifx<P−2E-1⁡P⁡xP⁡x+1E-1⁡P⁡xP⁡0⁡i=P⁡iP⁡i+1
14 11 13 raleqbidv ⊢f=x∈0..^P−1⟼ifx<P−2E-1⁡P⁡xP⁡x+1E-1⁡P⁡xP⁡0→∀i∈0..^fE⁡f⁡i=P⁡iP⁡i+1↔∀i∈0..^x∈0..^P−1⟼ifx<P−2E-1⁡P⁡xP⁡x+1E-1⁡P⁡xP⁡0E⁡x∈0..^P−1⟼ifx<P−2E-1⁡P⁡xP⁡x+1E-1⁡P⁡xP⁡0⁡i=P⁡iP⁡i+1
15 7 10 14 3anbi123d ⊢f=x∈0..^P−1⟼ifx<P−2E-1⁡P⁡xP⁡x+1E-1⁡P⁡xP⁡0→f∈Worddom⁡E∧P:0…f⟶V∧∀i∈0..^fE⁡f⁡i=P⁡iP⁡i+1↔x∈0..^P−1⟼ifx<P−2E-1⁡P⁡xP⁡x+1E-1⁡P⁡xP⁡0∈Worddom⁡E∧P:0…x∈0..^P−1⟼ifx<P−2E-1⁡P⁡xP⁡x+1E-1⁡P⁡xP⁡0⟶V∧∀i∈0..^x∈0..^P−1⟼ifx<P−2E-1⁡P⁡xP⁡x+1E-1⁡P⁡xP⁡0E⁡x∈0..^P−1⟼ifx<P−2E-1⁡P⁡xP⁡x+1E-1⁡P⁡xP⁡0⁡i=P⁡iP⁡i+1
16 2fveq3 ⊢f=x∈0..^P−1⟼ifx<P−2E-1⁡P⁡xP⁡x+1E-1⁡P⁡xP⁡0→P⁡f=P⁡x∈0..^P−1⟼ifx<P−2E-1⁡P⁡xP⁡x+1E-1⁡P⁡xP⁡0
17 16 eqeq2d ⊢f=x∈0..^P−1⟼ifx<P−2E-1⁡P⁡xP⁡x+1E-1⁡P⁡xP⁡0→P⁡0=P⁡f↔P⁡0=P⁡x∈0..^P−1⟼ifx<P−2E-1⁡P⁡xP⁡x+1E-1⁡P⁡xP⁡0
18 15 17 anbi12d ⊢f=x∈0..^P−1⟼ifx<P−2E-1⁡P⁡xP⁡x+1E-1⁡P⁡xP⁡0→f∈Worddom⁡E∧P:0…f⟶V∧∀i∈0..^fE⁡f⁡i=P⁡iP⁡i+1∧P⁡0=P⁡f↔x∈0..^P−1⟼ifx<P−2E-1⁡P⁡xP⁡x+1E-1⁡P⁡xP⁡0∈Worddom⁡E∧P:0…x∈0..^P−1⟼ifx<P−2E-1⁡P⁡xP⁡x+1E-1⁡P⁡xP⁡0⟶V∧∀i∈0..^x∈0..^P−1⟼ifx<P−2E-1⁡P⁡xP⁡x+1E-1⁡P⁡xP⁡0E⁡x∈0..^P−1⟼ifx<P−2E-1⁡P⁡xP⁡x+1E-1⁡P⁡xP⁡0⁡i=P⁡iP⁡i+1∧P⁡0=P⁡x∈0..^P−1⟼ifx<P−2E-1⁡P⁡xP⁡x+1E-1⁡P⁡xP⁡0
19 18 imbi2d ⊢f=x∈0..^P−1⟼ifx<P−2E-1⁡P⁡xP⁡x+1E-1⁡P⁡xP⁡0→lastS⁡P=P⁡0∧∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E→f∈Worddom⁡E∧P:0…f⟶V∧∀i∈0..^fE⁡f⁡i=P⁡iP⁡i+1∧P⁡0=P⁡f↔lastS⁡P=P⁡0∧∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E→x∈0..^P−1⟼ifx<P−2E-1⁡P⁡xP⁡x+1E-1⁡P⁡xP⁡0∈Worddom⁡E∧P:0…x∈0..^P−1⟼ifx<P−2E-1⁡P⁡xP⁡x+1E-1⁡P⁡xP⁡0⟶V∧∀i∈0..^x∈0..^P−1⟼ifx<P−2E-1⁡P⁡xP⁡x+1E-1⁡P⁡xP⁡0E⁡x∈0..^P−1⟼ifx<P−2E-1⁡P⁡xP⁡x+1E-1⁡P⁡xP⁡0⁡i=P⁡iP⁡i+1∧P⁡0=P⁡x∈0..^P−1⟼ifx<P−2E-1⁡P⁡xP⁡x+1E-1⁡P⁡xP⁡0
20 19 adantl ⊢E:dom⁡E⟶1-1R∧P∈WordV∧2≤P∧f=x∈0..^P−1⟼ifx<P−2E-1⁡P⁡xP⁡x+1E-1⁡P⁡xP⁡0→lastS⁡P=P⁡0∧∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E→f∈Worddom⁡E∧P:0…f⟶V∧∀i∈0..^fE⁡f⁡i=P⁡iP⁡i+1∧P⁡0=P⁡f↔lastS⁡P=P⁡0∧∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E→x∈0..^P−1⟼ifx<P−2E-1⁡P⁡xP⁡x+1E-1⁡P⁡xP⁡0∈Worddom⁡E∧P:0…x∈0..^P−1⟼ifx<P−2E-1⁡P⁡xP⁡x+1E-1⁡P⁡xP⁡0⟶V∧∀i∈0..^x∈0..^P−1⟼ifx<P−2E-1⁡P⁡xP⁡x+1E-1⁡P⁡xP⁡0E⁡x∈0..^P−1⟼ifx<P−2E-1⁡P⁡xP⁡x+1E-1⁡P⁡xP⁡0⁡i=P⁡iP⁡i+1∧P⁡0=P⁡x∈0..^P−1⟼ifx<P−2E-1⁡P⁡xP⁡x+1E-1⁡P⁡xP⁡0
21 6 20 mpbird ⊢E:dom⁡E⟶1-1R∧P∈WordV∧2≤P∧f=x∈0..^P−1⟼ifx<P−2E-1⁡P⁡xP⁡x+1E-1⁡P⁡xP⁡0→lastS⁡P=P⁡0∧∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E→f∈Worddom⁡E∧P:0…f⟶V∧∀i∈0..^fE⁡f⁡i=P⁡iP⁡i+1∧P⁡0=P⁡f
22 3 21 spcimedv ⊢E:dom⁡E⟶1-1R∧P∈WordV∧2≤P→lastS⁡P=P⁡0∧∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E→∃ff∈Worddom⁡E∧P:0…f⟶V∧∀i∈0..^fE⁡f⁡i=P⁡iP⁡i+1∧P⁡0=P⁡f