Metamath Proof Explorer

Theorem 3pthdlem1

Description: Lemma 1 for 3pthd . (Contributed by AV, 9-Feb-2021)

Ref Expression
Hypotheses 3wlkd.p 
|- P = <" A B C D ">
3wlkd.f 
|- F = <" J K L ">
3wlkd.s 
|- ( ph -> ( ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) )
3wlkd.n 
|- ( ph -> ( ( A =/= B /\ A =/= C ) /\ ( B =/= C /\ B =/= D ) /\ C =/= D ) )
Assertion 3pthdlem1 
|- ( ph -> A. k e. ( 0 ..^ ( # ` P ) ) A. j e. ( 1 ..^ ( # ` F ) ) ( k =/= j -> ( P ` k ) =/= ( P ` j ) ) )

Proof

Step Hyp Ref Expression
1 3wlkd.p 
 |-  P = <" A B C D ">
2 3wlkd.f 
 |-  F = <" J K L ">
3 3wlkd.s 
 |-  ( ph -> ( ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) )
4 3wlkd.n 
 |-  ( ph -> ( ( A =/= B /\ A =/= C ) /\ ( B =/= C /\ B =/= D ) /\ C =/= D ) )
5 1 2 3 3wlkdlem3 
 |-  ( ph -> ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B ) /\ ( ( P ` 2 ) = C /\ ( P ` 3 ) = D ) ) )
6 simpr1l 
 |-  ( ( ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B ) /\ ( ( P ` 2 ) = C /\ ( P ` 3 ) = D ) ) /\ ( ( A =/= B /\ A =/= C ) /\ ( B =/= C /\ B =/= D ) /\ C =/= D ) ) -> A =/= B )
7 simpl 
 |-  ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B ) -> ( P ` 0 ) = A )
8 7 adantr 
 |-  ( ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B ) /\ ( ( P ` 2 ) = C /\ ( P ` 3 ) = D ) ) -> ( P ` 0 ) = A )
9 simpr 
 |-  ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B ) -> ( P ` 1 ) = B )
10 9 adantr 
 |-  ( ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B ) /\ ( ( P ` 2 ) = C /\ ( P ` 3 ) = D ) ) -> ( P ` 1 ) = B )
11 8 10 neeq12d 
 |-  ( ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B ) /\ ( ( P ` 2 ) = C /\ ( P ` 3 ) = D ) ) -> ( ( P ` 0 ) =/= ( P ` 1 ) <-> A =/= B ) )
12 11 adantr 
 |-  ( ( ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B ) /\ ( ( P ` 2 ) = C /\ ( P ` 3 ) = D ) ) /\ ( ( A =/= B /\ A =/= C ) /\ ( B =/= C /\ B =/= D ) /\ C =/= D ) ) -> ( ( P ` 0 ) =/= ( P ` 1 ) <-> A =/= B ) )
13 6 12 mpbird 
 |-  ( ( ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B ) /\ ( ( P ` 2 ) = C /\ ( P ` 3 ) = D ) ) /\ ( ( A =/= B /\ A =/= C ) /\ ( B =/= C /\ B =/= D ) /\ C =/= D ) ) -> ( P ` 0 ) =/= ( P ` 1 ) )
14 13 a1d 
 |-  ( ( ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B ) /\ ( ( P ` 2 ) = C /\ ( P ` 3 ) = D ) ) /\ ( ( A =/= B /\ A =/= C ) /\ ( B =/= C /\ B =/= D ) /\ C =/= D ) ) -> ( 0 =/= 1 -> ( P ` 0 ) =/= ( P ` 1 ) ) )
15 simpr1r 
 |-  ( ( ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B ) /\ ( ( P ` 2 ) = C /\ ( P ` 3 ) = D ) ) /\ ( ( A =/= B /\ A =/= C ) /\ ( B =/= C /\ B =/= D ) /\ C =/= D ) ) -> A =/= C )
16 simpl 
 |-  ( ( ( P ` 2 ) = C /\ ( P ` 3 ) = D ) -> ( P ` 2 ) = C )
17 16 adantl 
 |-  ( ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B ) /\ ( ( P ` 2 ) = C /\ ( P ` 3 ) = D ) ) -> ( P ` 2 ) = C )
18 8 17 neeq12d 
 |-  ( ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B ) /\ ( ( P ` 2 ) = C /\ ( P ` 3 ) = D ) ) -> ( ( P ` 0 ) =/= ( P ` 2 ) <-> A =/= C ) )
19 18 adantr 
 |-  ( ( ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B ) /\ ( ( P ` 2 ) = C /\ ( P ` 3 ) = D ) ) /\ ( ( A =/= B /\ A =/= C ) /\ ( B =/= C /\ B =/= D ) /\ C =/= D ) ) -> ( ( P ` 0 ) =/= ( P ` 2 ) <-> A =/= C ) )
20 15 19 mpbird 
 |-  ( ( ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B ) /\ ( ( P ` 2 ) = C /\ ( P ` 3 ) = D ) ) /\ ( ( A =/= B /\ A =/= C ) /\ ( B =/= C /\ B =/= D ) /\ C =/= D ) ) -> ( P ` 0 ) =/= ( P ` 2 ) )
21 20 a1d 
 |-  ( ( ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B ) /\ ( ( P ` 2 ) = C /\ ( P ` 3 ) = D ) ) /\ ( ( A =/= B /\ A =/= C ) /\ ( B =/= C /\ B =/= D ) /\ C =/= D ) ) -> ( 0 =/= 2 -> ( P ` 0 ) =/= ( P ` 2 ) ) )
22 14 21 jca 
 |-  ( ( ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B ) /\ ( ( P ` 2 ) = C /\ ( P ` 3 ) = D ) ) /\ ( ( A =/= B /\ A =/= C ) /\ ( B =/= C /\ B =/= D ) /\ C =/= D ) ) -> ( ( 0 =/= 1 -> ( P ` 0 ) =/= ( P ` 1 ) ) /\ ( 0 =/= 2 -> ( P ` 0 ) =/= ( P ` 2 ) ) ) )
23 eqid 
 |-  1 = 1
24 23 2a1i 
 |-  ( ( ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B ) /\ ( ( P ` 2 ) = C /\ ( P ` 3 ) = D ) ) /\ ( ( A =/= B /\ A =/= C ) /\ ( B =/= C /\ B =/= D ) /\ C =/= D ) ) -> ( ( P ` 1 ) = ( P ` 1 ) -> 1 = 1 ) )
25 24 necon3d 
 |-  ( ( ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B ) /\ ( ( P ` 2 ) = C /\ ( P ` 3 ) = D ) ) /\ ( ( A =/= B /\ A =/= C ) /\ ( B =/= C /\ B =/= D ) /\ C =/= D ) ) -> ( 1 =/= 1 -> ( P ` 1 ) =/= ( P ` 1 ) ) )
26 simpr2l 
 |-  ( ( ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B ) /\ ( ( P ` 2 ) = C /\ ( P ` 3 ) = D ) ) /\ ( ( A =/= B /\ A =/= C ) /\ ( B =/= C /\ B =/= D ) /\ C =/= D ) ) -> B =/= C )
27 10 17 neeq12d 
 |-  ( ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B ) /\ ( ( P ` 2 ) = C /\ ( P ` 3 ) = D ) ) -> ( ( P ` 1 ) =/= ( P ` 2 ) <-> B =/= C ) )
28 27 adantr 
 |-  ( ( ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B ) /\ ( ( P ` 2 ) = C /\ ( P ` 3 ) = D ) ) /\ ( ( A =/= B /\ A =/= C ) /\ ( B =/= C /\ B =/= D ) /\ C =/= D ) ) -> ( ( P ` 1 ) =/= ( P ` 2 ) <-> B =/= C ) )
29 26 28 mpbird 
 |-  ( ( ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B ) /\ ( ( P ` 2 ) = C /\ ( P ` 3 ) = D ) ) /\ ( ( A =/= B /\ A =/= C ) /\ ( B =/= C /\ B =/= D ) /\ C =/= D ) ) -> ( P ` 1 ) =/= ( P ` 2 ) )
30 29 a1d 
 |-  ( ( ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B ) /\ ( ( P ` 2 ) = C /\ ( P ` 3 ) = D ) ) /\ ( ( A =/= B /\ A =/= C ) /\ ( B =/= C /\ B =/= D ) /\ C =/= D ) ) -> ( 1 =/= 2 -> ( P ` 1 ) =/= ( P ` 2 ) ) )
31 25 30 jca 
 |-  ( ( ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B ) /\ ( ( P ` 2 ) = C /\ ( P ` 3 ) = D ) ) /\ ( ( A =/= B /\ A =/= C ) /\ ( B =/= C /\ B =/= D ) /\ C =/= D ) ) -> ( ( 1 =/= 1 -> ( P ` 1 ) =/= ( P ` 1 ) ) /\ ( 1 =/= 2 -> ( P ` 1 ) =/= ( P ` 2 ) ) ) )
32 29 necomd 
 |-  ( ( ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B ) /\ ( ( P ` 2 ) = C /\ ( P ` 3 ) = D ) ) /\ ( ( A =/= B /\ A =/= C ) /\ ( B =/= C /\ B =/= D ) /\ C =/= D ) ) -> ( P ` 2 ) =/= ( P ` 1 ) )
33 32 a1d 
 |-  ( ( ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B ) /\ ( ( P ` 2 ) = C /\ ( P ` 3 ) = D ) ) /\ ( ( A =/= B /\ A =/= C ) /\ ( B =/= C /\ B =/= D ) /\ C =/= D ) ) -> ( 2 =/= 1 -> ( P ` 2 ) =/= ( P ` 1 ) ) )
34 eqid 
 |-  2 = 2
35 34 2a1i 
 |-  ( ( ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B ) /\ ( ( P ` 2 ) = C /\ ( P ` 3 ) = D ) ) /\ ( ( A =/= B /\ A =/= C ) /\ ( B =/= C /\ B =/= D ) /\ C =/= D ) ) -> ( ( P ` 2 ) = ( P ` 2 ) -> 2 = 2 ) )
36 35 necon3d 
 |-  ( ( ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B ) /\ ( ( P ` 2 ) = C /\ ( P ` 3 ) = D ) ) /\ ( ( A =/= B /\ A =/= C ) /\ ( B =/= C /\ B =/= D ) /\ C =/= D ) ) -> ( 2 =/= 2 -> ( P ` 2 ) =/= ( P ` 2 ) ) )
37 simpr2r 
 |-  ( ( ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B ) /\ ( ( P ` 2 ) = C /\ ( P ` 3 ) = D ) ) /\ ( ( A =/= B /\ A =/= C ) /\ ( B =/= C /\ B =/= D ) /\ C =/= D ) ) -> B =/= D )
38 simpr 
 |-  ( ( ( P ` 2 ) = C /\ ( P ` 3 ) = D ) -> ( P ` 3 ) = D )
39 38 adantl 
 |-  ( ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B ) /\ ( ( P ` 2 ) = C /\ ( P ` 3 ) = D ) ) -> ( P ` 3 ) = D )
40 10 39 neeq12d 
 |-  ( ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B ) /\ ( ( P ` 2 ) = C /\ ( P ` 3 ) = D ) ) -> ( ( P ` 1 ) =/= ( P ` 3 ) <-> B =/= D ) )
41 40 adantr 
 |-  ( ( ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B ) /\ ( ( P ` 2 ) = C /\ ( P ` 3 ) = D ) ) /\ ( ( A =/= B /\ A =/= C ) /\ ( B =/= C /\ B =/= D ) /\ C =/= D ) ) -> ( ( P ` 1 ) =/= ( P ` 3 ) <-> B =/= D ) )
42 37 41 mpbird 
 |-  ( ( ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B ) /\ ( ( P ` 2 ) = C /\ ( P ` 3 ) = D ) ) /\ ( ( A =/= B /\ A =/= C ) /\ ( B =/= C /\ B =/= D ) /\ C =/= D ) ) -> ( P ` 1 ) =/= ( P ` 3 ) )
43 42 necomd 
 |-  ( ( ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B ) /\ ( ( P ` 2 ) = C /\ ( P ` 3 ) = D ) ) /\ ( ( A =/= B /\ A =/= C ) /\ ( B =/= C /\ B =/= D ) /\ C =/= D ) ) -> ( P ` 3 ) =/= ( P ` 1 ) )
44 43 a1d 
 |-  ( ( ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B ) /\ ( ( P ` 2 ) = C /\ ( P ` 3 ) = D ) ) /\ ( ( A =/= B /\ A =/= C ) /\ ( B =/= C /\ B =/= D ) /\ C =/= D ) ) -> ( 3 =/= 1 -> ( P ` 3 ) =/= ( P ` 1 ) ) )
45 simp3 
 |-  ( ( ( A =/= B /\ A =/= C ) /\ ( B =/= C /\ B =/= D ) /\ C =/= D ) -> C =/= D )
46 45 necomd 
 |-  ( ( ( A =/= B /\ A =/= C ) /\ ( B =/= C /\ B =/= D ) /\ C =/= D ) -> D =/= C )
47 46 adantl 
 |-  ( ( ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B ) /\ ( ( P ` 2 ) = C /\ ( P ` 3 ) = D ) ) /\ ( ( A =/= B /\ A =/= C ) /\ ( B =/= C /\ B =/= D ) /\ C =/= D ) ) -> D =/= C )
48 simpl 
 |-  ( ( ( P ` 3 ) = D /\ ( P ` 2 ) = C ) -> ( P ` 3 ) = D )
49 simpr 
 |-  ( ( ( P ` 3 ) = D /\ ( P ` 2 ) = C ) -> ( P ` 2 ) = C )
50 48 49 neeq12d 
 |-  ( ( ( P ` 3 ) = D /\ ( P ` 2 ) = C ) -> ( ( P ` 3 ) =/= ( P ` 2 ) <-> D =/= C ) )
51 50 ancoms 
 |-  ( ( ( P ` 2 ) = C /\ ( P ` 3 ) = D ) -> ( ( P ` 3 ) =/= ( P ` 2 ) <-> D =/= C ) )
52 51 adantl 
 |-  ( ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B ) /\ ( ( P ` 2 ) = C /\ ( P ` 3 ) = D ) ) -> ( ( P ` 3 ) =/= ( P ` 2 ) <-> D =/= C ) )
53 52 adantr 
 |-  ( ( ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B ) /\ ( ( P ` 2 ) = C /\ ( P ` 3 ) = D ) ) /\ ( ( A =/= B /\ A =/= C ) /\ ( B =/= C /\ B =/= D ) /\ C =/= D ) ) -> ( ( P ` 3 ) =/= ( P ` 2 ) <-> D =/= C ) )
54 47 53 mpbird 
 |-  ( ( ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B ) /\ ( ( P ` 2 ) = C /\ ( P ` 3 ) = D ) ) /\ ( ( A =/= B /\ A =/= C ) /\ ( B =/= C /\ B =/= D ) /\ C =/= D ) ) -> ( P ` 3 ) =/= ( P ` 2 ) )
55 54 a1d 
 |-  ( ( ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B ) /\ ( ( P ` 2 ) = C /\ ( P ` 3 ) = D ) ) /\ ( ( A =/= B /\ A =/= C ) /\ ( B =/= C /\ B =/= D ) /\ C =/= D ) ) -> ( 3 =/= 2 -> ( P ` 3 ) =/= ( P ` 2 ) ) )
56 44 55 jca 
 |-  ( ( ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B ) /\ ( ( P ` 2 ) = C /\ ( P ` 3 ) = D ) ) /\ ( ( A =/= B /\ A =/= C ) /\ ( B =/= C /\ B =/= D ) /\ C =/= D ) ) -> ( ( 3 =/= 1 -> ( P ` 3 ) =/= ( P ` 1 ) ) /\ ( 3 =/= 2 -> ( P ` 3 ) =/= ( P ` 2 ) ) ) )
57 33 36 56 jca31 
 |-  ( ( ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B ) /\ ( ( P ` 2 ) = C /\ ( P ` 3 ) = D ) ) /\ ( ( A =/= B /\ A =/= C ) /\ ( B =/= C /\ B =/= D ) /\ C =/= D ) ) -> ( ( ( 2 =/= 1 -> ( P ` 2 ) =/= ( P ` 1 ) ) /\ ( 2 =/= 2 -> ( P ` 2 ) =/= ( P ` 2 ) ) ) /\ ( ( 3 =/= 1 -> ( P ` 3 ) =/= ( P ` 1 ) ) /\ ( 3 =/= 2 -> ( P ` 3 ) =/= ( P ` 2 ) ) ) ) )
58 22 31 57 jca31 
 |-  ( ( ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B ) /\ ( ( P ` 2 ) = C /\ ( P ` 3 ) = D ) ) /\ ( ( A =/= B /\ A =/= C ) /\ ( B =/= C /\ B =/= D ) /\ C =/= D ) ) -> ( ( ( ( 0 =/= 1 -> ( P ` 0 ) =/= ( P ` 1 ) ) /\ ( 0 =/= 2 -> ( P ` 0 ) =/= ( P ` 2 ) ) ) /\ ( ( 1 =/= 1 -> ( P ` 1 ) =/= ( P ` 1 ) ) /\ ( 1 =/= 2 -> ( P ` 1 ) =/= ( P ` 2 ) ) ) ) /\ ( ( ( 2 =/= 1 -> ( P ` 2 ) =/= ( P ` 1 ) ) /\ ( 2 =/= 2 -> ( P ` 2 ) =/= ( P ` 2 ) ) ) /\ ( ( 3 =/= 1 -> ( P ` 3 ) =/= ( P ` 1 ) ) /\ ( 3 =/= 2 -> ( P ` 3 ) =/= ( P ` 2 ) ) ) ) ) )
59 5 4 58 syl2anc 
 |-  ( ph -> ( ( ( ( 0 =/= 1 -> ( P ` 0 ) =/= ( P ` 1 ) ) /\ ( 0 =/= 2 -> ( P ` 0 ) =/= ( P ` 2 ) ) ) /\ ( ( 1 =/= 1 -> ( P ` 1 ) =/= ( P ` 1 ) ) /\ ( 1 =/= 2 -> ( P ` 1 ) =/= ( P ` 2 ) ) ) ) /\ ( ( ( 2 =/= 1 -> ( P ` 2 ) =/= ( P ` 1 ) ) /\ ( 2 =/= 2 -> ( P ` 2 ) =/= ( P ` 2 ) ) ) /\ ( ( 3 =/= 1 -> ( P ` 3 ) =/= ( P ` 1 ) ) /\ ( 3 =/= 2 -> ( P ` 3 ) =/= ( P ` 2 ) ) ) ) ) )
60 1 fveq2i 
 |-  ( # ` P ) = ( # ` <" A B C D "> )
61 s4len 
 |-  ( # ` <" A B C D "> ) = 4
62 60 61 eqtri 
 |-  ( # ` P ) = 4
63 62 oveq2i 
 |-  ( 0 ..^ ( # ` P ) ) = ( 0 ..^ 4 )
64 fzo0to42pr 
 |-  ( 0 ..^ 4 ) = ( { 0 , 1 } u. { 2 , 3 } )
65 63 64 eqtri 
 |-  ( 0 ..^ ( # ` P ) ) = ( { 0 , 1 } u. { 2 , 3 } )
66 65 raleqi 
 |-  ( A. k e. ( 0 ..^ ( # ` P ) ) ( ( k =/= 1 -> ( P ` k ) =/= ( P ` 1 ) ) /\ ( k =/= 2 -> ( P ` k ) =/= ( P ` 2 ) ) ) <-> A. k e. ( { 0 , 1 } u. { 2 , 3 } ) ( ( k =/= 1 -> ( P ` k ) =/= ( P ` 1 ) ) /\ ( k =/= 2 -> ( P ` k ) =/= ( P ` 2 ) ) ) )
67 ralunb 
 |-  ( A. k e. ( { 0 , 1 } u. { 2 , 3 } ) ( ( k =/= 1 -> ( P ` k ) =/= ( P ` 1 ) ) /\ ( k =/= 2 -> ( P ` k ) =/= ( P ` 2 ) ) ) <-> ( A. k e. { 0 , 1 } ( ( k =/= 1 -> ( P ` k ) =/= ( P ` 1 ) ) /\ ( k =/= 2 -> ( P ` k ) =/= ( P ` 2 ) ) ) /\ A. k e. { 2 , 3 } ( ( k =/= 1 -> ( P ` k ) =/= ( P ` 1 ) ) /\ ( k =/= 2 -> ( P ` k ) =/= ( P ` 2 ) ) ) ) )
68 c0ex 
 |-  0 e. _V
69 1ex 
 |-  1 e. _V
70 neeq1 
 |-  ( k = 0 -> ( k =/= 1 <-> 0 =/= 1 ) )
71 fveq2 
 |-  ( k = 0 -> ( P ` k ) = ( P ` 0 ) )
72 71 neeq1d 
 |-  ( k = 0 -> ( ( P ` k ) =/= ( P ` 1 ) <-> ( P ` 0 ) =/= ( P ` 1 ) ) )
73 70 72 imbi12d 
 |-  ( k = 0 -> ( ( k =/= 1 -> ( P ` k ) =/= ( P ` 1 ) ) <-> ( 0 =/= 1 -> ( P ` 0 ) =/= ( P ` 1 ) ) ) )
74 neeq1 
 |-  ( k = 0 -> ( k =/= 2 <-> 0 =/= 2 ) )
75 71 neeq1d 
 |-  ( k = 0 -> ( ( P ` k ) =/= ( P ` 2 ) <-> ( P ` 0 ) =/= ( P ` 2 ) ) )
76 74 75 imbi12d 
 |-  ( k = 0 -> ( ( k =/= 2 -> ( P ` k ) =/= ( P ` 2 ) ) <-> ( 0 =/= 2 -> ( P ` 0 ) =/= ( P ` 2 ) ) ) )
77 73 76 anbi12d 
 |-  ( k = 0 -> ( ( ( k =/= 1 -> ( P ` k ) =/= ( P ` 1 ) ) /\ ( k =/= 2 -> ( P ` k ) =/= ( P ` 2 ) ) ) <-> ( ( 0 =/= 1 -> ( P ` 0 ) =/= ( P ` 1 ) ) /\ ( 0 =/= 2 -> ( P ` 0 ) =/= ( P ` 2 ) ) ) ) )
78 neeq1 
 |-  ( k = 1 -> ( k =/= 1 <-> 1 =/= 1 ) )
79 fveq2 
 |-  ( k = 1 -> ( P ` k ) = ( P ` 1 ) )
80 79 neeq1d 
 |-  ( k = 1 -> ( ( P ` k ) =/= ( P ` 1 ) <-> ( P ` 1 ) =/= ( P ` 1 ) ) )
81 78 80 imbi12d 
 |-  ( k = 1 -> ( ( k =/= 1 -> ( P ` k ) =/= ( P ` 1 ) ) <-> ( 1 =/= 1 -> ( P ` 1 ) =/= ( P ` 1 ) ) ) )
82 neeq1 
 |-  ( k = 1 -> ( k =/= 2 <-> 1 =/= 2 ) )
83 79 neeq1d 
 |-  ( k = 1 -> ( ( P ` k ) =/= ( P ` 2 ) <-> ( P ` 1 ) =/= ( P ` 2 ) ) )
84 82 83 imbi12d 
 |-  ( k = 1 -> ( ( k =/= 2 -> ( P ` k ) =/= ( P ` 2 ) ) <-> ( 1 =/= 2 -> ( P ` 1 ) =/= ( P ` 2 ) ) ) )
85 81 84 anbi12d 
 |-  ( k = 1 -> ( ( ( k =/= 1 -> ( P ` k ) =/= ( P ` 1 ) ) /\ ( k =/= 2 -> ( P ` k ) =/= ( P ` 2 ) ) ) <-> ( ( 1 =/= 1 -> ( P ` 1 ) =/= ( P ` 1 ) ) /\ ( 1 =/= 2 -> ( P ` 1 ) =/= ( P ` 2 ) ) ) ) )
86 68 69 77 85 ralpr 
 |-  ( A. k e. { 0 , 1 } ( ( k =/= 1 -> ( P ` k ) =/= ( P ` 1 ) ) /\ ( k =/= 2 -> ( P ` k ) =/= ( P ` 2 ) ) ) <-> ( ( ( 0 =/= 1 -> ( P ` 0 ) =/= ( P ` 1 ) ) /\ ( 0 =/= 2 -> ( P ` 0 ) =/= ( P ` 2 ) ) ) /\ ( ( 1 =/= 1 -> ( P ` 1 ) =/= ( P ` 1 ) ) /\ ( 1 =/= 2 -> ( P ` 1 ) =/= ( P ` 2 ) ) ) ) )
87 2ex 
 |-  2 e. _V
88 3ex 
 |-  3 e. _V
89 neeq1 
 |-  ( k = 2 -> ( k =/= 1 <-> 2 =/= 1 ) )
90 fveq2 
 |-  ( k = 2 -> ( P ` k ) = ( P ` 2 ) )
91 90 neeq1d 
 |-  ( k = 2 -> ( ( P ` k ) =/= ( P ` 1 ) <-> ( P ` 2 ) =/= ( P ` 1 ) ) )
92 89 91 imbi12d 
 |-  ( k = 2 -> ( ( k =/= 1 -> ( P ` k ) =/= ( P ` 1 ) ) <-> ( 2 =/= 1 -> ( P ` 2 ) =/= ( P ` 1 ) ) ) )
93 neeq1 
 |-  ( k = 2 -> ( k =/= 2 <-> 2 =/= 2 ) )
94 90 neeq1d 
 |-  ( k = 2 -> ( ( P ` k ) =/= ( P ` 2 ) <-> ( P ` 2 ) =/= ( P ` 2 ) ) )
95 93 94 imbi12d 
 |-  ( k = 2 -> ( ( k =/= 2 -> ( P ` k ) =/= ( P ` 2 ) ) <-> ( 2 =/= 2 -> ( P ` 2 ) =/= ( P ` 2 ) ) ) )
96 92 95 anbi12d 
 |-  ( k = 2 -> ( ( ( k =/= 1 -> ( P ` k ) =/= ( P ` 1 ) ) /\ ( k =/= 2 -> ( P ` k ) =/= ( P ` 2 ) ) ) <-> ( ( 2 =/= 1 -> ( P ` 2 ) =/= ( P ` 1 ) ) /\ ( 2 =/= 2 -> ( P ` 2 ) =/= ( P ` 2 ) ) ) ) )
97 neeq1 
 |-  ( k = 3 -> ( k =/= 1 <-> 3 =/= 1 ) )
98 fveq2 
 |-  ( k = 3 -> ( P ` k ) = ( P ` 3 ) )
99 98 neeq1d 
 |-  ( k = 3 -> ( ( P ` k ) =/= ( P ` 1 ) <-> ( P ` 3 ) =/= ( P ` 1 ) ) )
100 97 99 imbi12d 
 |-  ( k = 3 -> ( ( k =/= 1 -> ( P ` k ) =/= ( P ` 1 ) ) <-> ( 3 =/= 1 -> ( P ` 3 ) =/= ( P ` 1 ) ) ) )
101 neeq1 
 |-  ( k = 3 -> ( k =/= 2 <-> 3 =/= 2 ) )
102 98 neeq1d 
 |-  ( k = 3 -> ( ( P ` k ) =/= ( P ` 2 ) <-> ( P ` 3 ) =/= ( P ` 2 ) ) )
103 101 102 imbi12d 
 |-  ( k = 3 -> ( ( k =/= 2 -> ( P ` k ) =/= ( P ` 2 ) ) <-> ( 3 =/= 2 -> ( P ` 3 ) =/= ( P ` 2 ) ) ) )
104 100 103 anbi12d 
 |-  ( k = 3 -> ( ( ( k =/= 1 -> ( P ` k ) =/= ( P ` 1 ) ) /\ ( k =/= 2 -> ( P ` k ) =/= ( P ` 2 ) ) ) <-> ( ( 3 =/= 1 -> ( P ` 3 ) =/= ( P ` 1 ) ) /\ ( 3 =/= 2 -> ( P ` 3 ) =/= ( P ` 2 ) ) ) ) )
105 87 88 96 104 ralpr 
 |-  ( A. k e. { 2 , 3 } ( ( k =/= 1 -> ( P ` k ) =/= ( P ` 1 ) ) /\ ( k =/= 2 -> ( P ` k ) =/= ( P ` 2 ) ) ) <-> ( ( ( 2 =/= 1 -> ( P ` 2 ) =/= ( P ` 1 ) ) /\ ( 2 =/= 2 -> ( P ` 2 ) =/= ( P ` 2 ) ) ) /\ ( ( 3 =/= 1 -> ( P ` 3 ) =/= ( P ` 1 ) ) /\ ( 3 =/= 2 -> ( P ` 3 ) =/= ( P ` 2 ) ) ) ) )
106 86 105 anbi12i 
 |-  ( ( A. k e. { 0 , 1 } ( ( k =/= 1 -> ( P ` k ) =/= ( P ` 1 ) ) /\ ( k =/= 2 -> ( P ` k ) =/= ( P ` 2 ) ) ) /\ A. k e. { 2 , 3 } ( ( k =/= 1 -> ( P ` k ) =/= ( P ` 1 ) ) /\ ( k =/= 2 -> ( P ` k ) =/= ( P ` 2 ) ) ) ) <-> ( ( ( ( 0 =/= 1 -> ( P ` 0 ) =/= ( P ` 1 ) ) /\ ( 0 =/= 2 -> ( P ` 0 ) =/= ( P ` 2 ) ) ) /\ ( ( 1 =/= 1 -> ( P ` 1 ) =/= ( P ` 1 ) ) /\ ( 1 =/= 2 -> ( P ` 1 ) =/= ( P ` 2 ) ) ) ) /\ ( ( ( 2 =/= 1 -> ( P ` 2 ) =/= ( P ` 1 ) ) /\ ( 2 =/= 2 -> ( P ` 2 ) =/= ( P ` 2 ) ) ) /\ ( ( 3 =/= 1 -> ( P ` 3 ) =/= ( P ` 1 ) ) /\ ( 3 =/= 2 -> ( P ` 3 ) =/= ( P ` 2 ) ) ) ) ) )
107 66 67 106 3bitri 
 |-  ( A. k e. ( 0 ..^ ( # ` P ) ) ( ( k =/= 1 -> ( P ` k ) =/= ( P ` 1 ) ) /\ ( k =/= 2 -> ( P ` k ) =/= ( P ` 2 ) ) ) <-> ( ( ( ( 0 =/= 1 -> ( P ` 0 ) =/= ( P ` 1 ) ) /\ ( 0 =/= 2 -> ( P ` 0 ) =/= ( P ` 2 ) ) ) /\ ( ( 1 =/= 1 -> ( P ` 1 ) =/= ( P ` 1 ) ) /\ ( 1 =/= 2 -> ( P ` 1 ) =/= ( P ` 2 ) ) ) ) /\ ( ( ( 2 =/= 1 -> ( P ` 2 ) =/= ( P ` 1 ) ) /\ ( 2 =/= 2 -> ( P ` 2 ) =/= ( P ` 2 ) ) ) /\ ( ( 3 =/= 1 -> ( P ` 3 ) =/= ( P ` 1 ) ) /\ ( 3 =/= 2 -> ( P ` 3 ) =/= ( P ` 2 ) ) ) ) ) )
108 59 107 sylibr 
 |-  ( ph -> A. k e. ( 0 ..^ ( # ` P ) ) ( ( k =/= 1 -> ( P ` k ) =/= ( P ` 1 ) ) /\ ( k =/= 2 -> ( P ` k ) =/= ( P ` 2 ) ) ) )
109 2 fveq2i 
 |-  ( # ` F ) = ( # ` <" J K L "> )
110 s3len 
 |-  ( # ` <" J K L "> ) = 3
111 109 110 eqtri 
 |-  ( # ` F ) = 3
112 111 oveq2i 
 |-  ( 1 ..^ ( # ` F ) ) = ( 1 ..^ 3 )
113 fzo13pr 
 |-  ( 1 ..^ 3 ) = { 1 , 2 }
114 112 113 eqtri 
 |-  ( 1 ..^ ( # ` F ) ) = { 1 , 2 }
115 114 raleqi 
 |-  ( A. j e. ( 1 ..^ ( # ` F ) ) ( k =/= j -> ( P ` k ) =/= ( P ` j ) ) <-> A. j e. { 1 , 2 } ( k =/= j -> ( P ` k ) =/= ( P ` j ) ) )
116 neeq2 
 |-  ( j = 1 -> ( k =/= j <-> k =/= 1 ) )
117 fveq2 
 |-  ( j = 1 -> ( P ` j ) = ( P ` 1 ) )
118 117 neeq2d 
 |-  ( j = 1 -> ( ( P ` k ) =/= ( P ` j ) <-> ( P ` k ) =/= ( P ` 1 ) ) )
119 116 118 imbi12d 
 |-  ( j = 1 -> ( ( k =/= j -> ( P ` k ) =/= ( P ` j ) ) <-> ( k =/= 1 -> ( P ` k ) =/= ( P ` 1 ) ) ) )
120 neeq2 
 |-  ( j = 2 -> ( k =/= j <-> k =/= 2 ) )
121 fveq2 
 |-  ( j = 2 -> ( P ` j ) = ( P ` 2 ) )
122 121 neeq2d 
 |-  ( j = 2 -> ( ( P ` k ) =/= ( P ` j ) <-> ( P ` k ) =/= ( P ` 2 ) ) )
123 120 122 imbi12d 
 |-  ( j = 2 -> ( ( k =/= j -> ( P ` k ) =/= ( P ` j ) ) <-> ( k =/= 2 -> ( P ` k ) =/= ( P ` 2 ) ) ) )
124 69 87 119 123 ralpr 
 |-  ( A. j e. { 1 , 2 } ( k =/= j -> ( P ` k ) =/= ( P ` j ) ) <-> ( ( k =/= 1 -> ( P ` k ) =/= ( P ` 1 ) ) /\ ( k =/= 2 -> ( P ` k ) =/= ( P ` 2 ) ) ) )
125 115 124 bitri 
 |-  ( A. j e. ( 1 ..^ ( # ` F ) ) ( k =/= j -> ( P ` k ) =/= ( P ` j ) ) <-> ( ( k =/= 1 -> ( P ` k ) =/= ( P ` 1 ) ) /\ ( k =/= 2 -> ( P ` k ) =/= ( P ` 2 ) ) ) )
126 125 ralbii 
 |-  ( A. k e. ( 0 ..^ ( # ` P ) ) A. j e. ( 1 ..^ ( # ` F ) ) ( k =/= j -> ( P ` k ) =/= ( P ` j ) ) <-> A. k e. ( 0 ..^ ( # ` P ) ) ( ( k =/= 1 -> ( P ` k ) =/= ( P ` 1 ) ) /\ ( k =/= 2 -> ( P ` k ) =/= ( P ` 2 ) ) ) )
127 108 126 sylibr 
 |-  ( ph -> A. k e. ( 0 ..^ ( # ` P ) ) A. j e. ( 1 ..^ ( # ` F ) ) ( k =/= j -> ( P ` k ) =/= ( P ` j ) ) )