Metamath Proof Explorer

Theorem 1wlkdlem4

Description: Lemma 4 for 1wlkd . (Contributed by AV, 22-Jan-2021)

Ref Expression
Hypotheses 1wlkd.p 
|- P = <" X Y ">
1wlkd.f 
|- F = <" J ">
1wlkd.x 
|- ( ph -> X e. V )
1wlkd.y 
|- ( ph -> Y e. V )
1wlkd.l 
|- ( ( ph /\ X = Y ) -> ( I ` J ) = { X } )
1wlkd.j 
|- ( ( ph /\ X =/= Y ) -> { X , Y } C_ ( I ` J ) )
Assertion 1wlkdlem4 
|- ( 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 1wlkd.p 
 |-  P = <" X Y ">
2 1wlkd.f 
 |-  F = <" J ">
3 1wlkd.x 
 |-  ( ph -> X e. V )
4 1wlkd.y 
 |-  ( ph -> Y e. V )
5 1wlkd.l 
 |-  ( ( ph /\ X = Y ) -> ( I ` J ) = { X } )
6 1wlkd.j 
 |-  ( ( ph /\ X =/= Y ) -> { X , Y } C_ ( I ` J ) )
7 2 fveq1i 
 |-  ( F ` 0 ) = ( <" J "> ` 0 )
8 1 2 3 4 5 6 1wlkdlem2 
 |-  ( ph -> X e. ( I ` J ) )
9 8 elfvexd 
 |-  ( ph -> J e. _V )
10 s1fv 
 |-  ( J e. _V -> ( <" J "> ` 0 ) = J )
11 9 10 syl 
 |-  ( ph -> ( <" J "> ` 0 ) = J )
12 7 11 syl5eq 
 |-  ( ph -> ( F ` 0 ) = J )
13 12 fveq2d 
 |-  ( ph -> ( I ` ( F ` 0 ) ) = ( I ` J ) )
14 13 adantr 
 |-  ( ( ph /\ X = Y ) -> ( I ` ( F ` 0 ) ) = ( I ` J ) )
15 14 5 eqtrd 
 |-  ( ( ph /\ X = Y ) -> ( I ` ( F ` 0 ) ) = { X } )
16 df-ne 
 |-  ( X =/= Y <-> -. X = Y )
17 16 6 sylan2br 
 |-  ( ( ph /\ -. X = Y ) -> { X , Y } C_ ( I ` J ) )
18 13 adantr 
 |-  ( ( ph /\ -. X = Y ) -> ( I ` ( F ` 0 ) ) = ( I ` J ) )
19 17 18 sseqtrrd 
 |-  ( ( ph /\ -. X = Y ) -> { X , Y } C_ ( I ` ( F ` 0 ) ) )
20 15 19 ifpimpda 
 |-  ( ph -> if- ( X = Y , ( I ` ( F ` 0 ) ) = { X } , { X , Y } C_ ( I ` ( F ` 0 ) ) ) )
21 1 fveq1i 
 |-  ( P ` 0 ) = ( <" X Y "> ` 0 )
22 s2fv0 
 |-  ( X e. V -> ( <" X Y "> ` 0 ) = X )
23 3 22 syl 
 |-  ( ph -> ( <" X Y "> ` 0 ) = X )
24 21 23 syl5eq 
 |-  ( ph -> ( P ` 0 ) = X )
25 1 fveq1i 
 |-  ( P ` 1 ) = ( <" X Y "> ` 1 )
26 s2fv1 
 |-  ( Y e. V -> ( <" X Y "> ` 1 ) = Y )
27 4 26 syl 
 |-  ( ph -> ( <" X Y "> ` 1 ) = Y )
28 25 27 syl5eq 
 |-  ( ph -> ( P ` 1 ) = Y )
29 eqeq12 
 |-  ( ( ( P ` 0 ) = X /\ ( P ` 1 ) = Y ) -> ( ( P ` 0 ) = ( P ` 1 ) <-> X = Y ) )
30 sneq 
 |-  ( ( P ` 0 ) = X -> { ( P ` 0 ) } = { X } )
31 30 adantr 
 |-  ( ( ( P ` 0 ) = X /\ ( P ` 1 ) = Y ) -> { ( P ` 0 ) } = { X } )
32 31 eqeq2d 
 |-  ( ( ( P ` 0 ) = X /\ ( P ` 1 ) = Y ) -> ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) } <-> ( I ` ( F ` 0 ) ) = { X } ) )
33 preq12 
 |-  ( ( ( P ` 0 ) = X /\ ( P ` 1 ) = Y ) -> { ( P ` 0 ) , ( P ` 1 ) } = { X , Y } )
34 33 sseq1d 
 |-  ( ( ( P ` 0 ) = X /\ ( P ` 1 ) = Y ) -> ( { ( P ` 0 ) , ( P ` 1 ) } C_ ( I ` ( F ` 0 ) ) <-> { X , Y } C_ ( I ` ( F ` 0 ) ) ) )
35 29 32 34 ifpbi123d 
 |-  ( ( ( P ` 0 ) = X /\ ( P ` 1 ) = Y ) -> ( if- ( ( P ` 0 ) = ( P ` 1 ) , ( I ` ( F ` 0 ) ) = { ( P ` 0 ) } , { ( P ` 0 ) , ( P ` 1 ) } C_ ( I ` ( F ` 0 ) ) ) <-> if- ( X = Y , ( I ` ( F ` 0 ) ) = { X } , { X , Y } C_ ( I ` ( F ` 0 ) ) ) ) )
36 24 28 35 syl2anc 
 |-  ( ph -> ( if- ( ( P ` 0 ) = ( P ` 1 ) , ( I ` ( F ` 0 ) ) = { ( P ` 0 ) } , { ( P ` 0 ) , ( P ` 1 ) } C_ ( I ` ( F ` 0 ) ) ) <-> if- ( X = Y , ( I ` ( F ` 0 ) ) = { X } , { X , Y } C_ ( I ` ( F ` 0 ) ) ) ) )
37 20 36 mpbird 
 |-  ( ph -> if- ( ( P ` 0 ) = ( P ` 1 ) , ( I ` ( F ` 0 ) ) = { ( P ` 0 ) } , { ( P ` 0 ) , ( P ` 1 ) } C_ ( I ` ( F ` 0 ) ) ) )
38 c0ex 
 |-  0 e. _V
39 oveq1 
 |-  ( k = 0 -> ( k + 1 ) = ( 0 + 1 ) )
40 0p1e1 
 |-  ( 0 + 1 ) = 1
41 39 40 eqtrdi 
 |-  ( k = 0 -> ( k + 1 ) = 1 )
42 wkslem2 
 |-  ( ( k = 0 /\ ( k + 1 ) = 1 ) -> ( if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) <-> if- ( ( P ` 0 ) = ( P ` 1 ) , ( I ` ( F ` 0 ) ) = { ( P ` 0 ) } , { ( P ` 0 ) , ( P ` 1 ) } C_ ( I ` ( F ` 0 ) ) ) ) )
43 41 42 mpdan 
 |-  ( k = 0 -> ( if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) <-> if- ( ( P ` 0 ) = ( P ` 1 ) , ( I ` ( F ` 0 ) ) = { ( P ` 0 ) } , { ( P ` 0 ) , ( P ` 1 ) } C_ ( I ` ( F ` 0 ) ) ) ) )
44 38 43 ralsn 
 |-  ( A. k e. { 0 } if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) <-> if- ( ( P ` 0 ) = ( P ` 1 ) , ( I ` ( F ` 0 ) ) = { ( P ` 0 ) } , { ( P ` 0 ) , ( P ` 1 ) } C_ ( I ` ( F ` 0 ) ) ) )
45 37 44 sylibr 
 |-  ( ph -> A. k e. { 0 } if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) )
46 2 fveq2i 
 |-  ( # ` F ) = ( # ` <" J "> )
47 s1len 
 |-  ( # ` <" J "> ) = 1
48 46 47 eqtri 
 |-  ( # ` F ) = 1
49 48 oveq2i 
 |-  ( 0 ..^ ( # ` F ) ) = ( 0 ..^ 1 )
50 fzo01 
 |-  ( 0 ..^ 1 ) = { 0 }
51 49 50 eqtri 
 |-  ( 0 ..^ ( # ` F ) ) = { 0 }
52 51 a1i 
 |-  ( ph -> ( 0 ..^ ( # ` F ) ) = { 0 } )
53 52 raleqdv 
 |-  ( 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 ) ) ) <-> A. k e. { 0 } if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) ) )
54 45 53 mpbird 
 |-  ( 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 ) ) ) )