Metamath Proof Explorer

Theorem wlkdlem4

Description: Lemma 4 for wlkd . (Contributed by Alexander van der Vekens, 1-Feb-2018) (Revised by AV, 23-Jan-2021)

Ref Expression
Hypotheses wlkd.p 
|- ( ph -> P e. Word _V )
wlkd.f 
|- ( ph -> F e. Word _V )
wlkd.l 
|- ( ph -> ( # ` P ) = ( ( # ` F ) + 1 ) )
wlkd.e 
|- ( ph -> A. k e. ( 0 ..^ ( # ` F ) ) { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) )
wlkd.n 
|- ( ph -> A. k e. ( 0 ..^ ( # ` F ) ) ( P ` k ) =/= ( P ` ( k + 1 ) ) )
Assertion wlkdlem4 
|- ( ph -> A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) )

Proof

Step Hyp Ref Expression
1 wlkd.p 
 |-  ( ph -> P e. Word _V )
2 wlkd.f 
 |-  ( ph -> F e. Word _V )
3 wlkd.l 
 |-  ( ph -> ( # ` P ) = ( ( # ` F ) + 1 ) )
4 wlkd.e 
 |-  ( ph -> A. k e. ( 0 ..^ ( # ` F ) ) { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) )
5 wlkd.n 
 |-  ( ph -> A. k e. ( 0 ..^ ( # ` F ) ) ( P ` k ) =/= ( P ` ( k + 1 ) ) )
6 r19.26 
 |-  ( A. k e. ( 0 ..^ ( # ` F ) ) ( { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) /\ ( P ` k ) =/= ( P ` ( k + 1 ) ) ) <-> ( A. k e. ( 0 ..^ ( # ` F ) ) { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) /\ A. k e. ( 0 ..^ ( # ` F ) ) ( P ` k ) =/= ( P ` ( k + 1 ) ) ) )
7 df-ne 
 |-  ( ( P ` k ) =/= ( P ` ( k + 1 ) ) <-> -. ( P ` k ) = ( P ` ( k + 1 ) ) )
8 ifpfal 
 |-  ( -. ( P ` k ) = ( P ` ( k + 1 ) ) -> ( if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) <-> { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) )
9 7 8 sylbi 
 |-  ( ( P ` k ) =/= ( P ` ( k + 1 ) ) -> ( if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) <-> { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) )
10 9 biimparc 
 |-  ( ( { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) /\ ( P ` k ) =/= ( P ` ( k + 1 ) ) ) -> if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) )
11 10 ralimi 
 |-  ( A. k e. ( 0 ..^ ( # ` F ) ) ( { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) /\ ( P ` k ) =/= ( P ` ( k + 1 ) ) ) -> A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) )
12 6 11 sylbir 
 |-  ( ( A. k e. ( 0 ..^ ( # ` F ) ) { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) /\ A. k e. ( 0 ..^ ( # ` F ) ) ( P ` k ) =/= ( P ` ( k + 1 ) ) ) -> A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) )
13 4 5 12 syl2anc 
 |-  ( ph -> A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) )