Metamath Proof Explorer

Theorem gpgprismgr4cycllem7

Description: Lemma 7 for gpgprismgr4cycl0 : the cycle <. P , F >. is proper, i.e., it has no overlapping vertices, except the first and the last one. (Contributed by AV, 1-Nov-2025)

Ref Expression
Hypothesis gpgprismgr4cycl.p 
|- P = <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. <. 0 , 0 >. ">
Assertion gpgprismgr4cycllem7 
|- ( ( X e. ( 0 ..^ ( # ` P ) ) /\ Y e. ( 1 ..^ 4 ) ) -> ( X =/= Y -> ( P ` X ) =/= ( P ` Y ) ) )

Proof

Step Hyp Ref Expression
1 gpgprismgr4cycl.p 
 |-  P = <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. <. 0 , 0 >. ">
2 1 gpgprismgr4cycllem4 
 |-  ( # ` P ) = 5
3 df-5 
 |-  5 = ( 4 + 1 )
4 2 3 eqtri 
 |-  ( # ` P ) = ( 4 + 1 )
5 4 oveq2i 
 |-  ( 0 ..^ ( # ` P ) ) = ( 0 ..^ ( 4 + 1 ) )
6 4nn0 
 |-  4 e. NN0
7 elnn0uz 
 |-  ( 4 e. NN0 <-> 4 e. ( ZZ>= ` 0 ) )
8 6 7 mpbi 
 |-  4 e. ( ZZ>= ` 0 )
9 fzosplitsn 
 |-  ( 4 e. ( ZZ>= ` 0 ) -> ( 0 ..^ ( 4 + 1 ) ) = ( ( 0 ..^ 4 ) u. { 4 } ) )
10 8 9 ax-mp 
 |-  ( 0 ..^ ( 4 + 1 ) ) = ( ( 0 ..^ 4 ) u. { 4 } )
11 fzo0to42pr 
 |-  ( 0 ..^ 4 ) = ( { 0 , 1 } u. { 2 , 3 } )
12 11 uneq1i 
 |-  ( ( 0 ..^ 4 ) u. { 4 } ) = ( ( { 0 , 1 } u. { 2 , 3 } ) u. { 4 } )
13 5 10 12 3eqtri 
 |-  ( 0 ..^ ( # ` P ) ) = ( ( { 0 , 1 } u. { 2 , 3 } ) u. { 4 } )
14 13 eleq2i 
 |-  ( X e. ( 0 ..^ ( # ` P ) ) <-> X e. ( ( { 0 , 1 } u. { 2 , 3 } ) u. { 4 } ) )
15 fzo1to4tp 
 |-  ( 1 ..^ 4 ) = { 1 , 2 , 3 }
16 15 eleq2i 
 |-  ( Y e. ( 1 ..^ 4 ) <-> Y e. { 1 , 2 , 3 } )
17 elun 
 |-  ( X e. ( ( { 0 , 1 } u. { 2 , 3 } ) u. { 4 } ) <-> ( X e. ( { 0 , 1 } u. { 2 , 3 } ) \/ X e. { 4 } ) )
18 elun 
 |-  ( X e. ( { 0 , 1 } u. { 2 , 3 } ) <-> ( X e. { 0 , 1 } \/ X e. { 2 , 3 } ) )
19 18 orbi1i 
 |-  ( ( X e. ( { 0 , 1 } u. { 2 , 3 } ) \/ X e. { 4 } ) <-> ( ( X e. { 0 , 1 } \/ X e. { 2 , 3 } ) \/ X e. { 4 } ) )
20 17 19 bitri 
 |-  ( X e. ( ( { 0 , 1 } u. { 2 , 3 } ) u. { 4 } ) <-> ( ( X e. { 0 , 1 } \/ X e. { 2 , 3 } ) \/ X e. { 4 } ) )
21 elpri 
 |-  ( X e. { 0 , 1 } -> ( X = 0 \/ X = 1 ) )
22 0ne1 
 |-  0 =/= 1
23 22 olci 
 |-  ( 0 =/= 0 \/ 0 =/= 1 )
24 c0ex 
 |-  0 e. _V
25 24 24 opthne 
 |-  ( <. 0 , 0 >. =/= <. 0 , 1 >. <-> ( 0 =/= 0 \/ 0 =/= 1 ) )
26 23 25 mpbir 
 |-  <. 0 , 0 >. =/= <. 0 , 1 >.
27 1 fveq1i 
 |-  ( P ` 0 ) = ( <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. <. 0 , 0 >. "> ` 0 )
28 opex 
 |-  <. 0 , 0 >. e. _V
29 df-s5 
 |-  <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. <. 0 , 0 >. "> = ( <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. "> ++ <" <. 0 , 0 >. "> )
30 s4cli 
 |-  <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. "> e. Word _V
31 s4len 
 |-  ( # ` <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. "> ) = 4
32 s4fv0 
 |-  ( <. 0 , 0 >. e. _V -> ( <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. "> ` 0 ) = <. 0 , 0 >. )
33 0nn0 
 |-  0 e. NN0
34 4pos 
 |-  0 < 4
35 29 30 31 32 33 34 cats1fv 
 |-  ( <. 0 , 0 >. e. _V -> ( <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. <. 0 , 0 >. "> ` 0 ) = <. 0 , 0 >. )
36 28 35 ax-mp 
 |-  ( <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. <. 0 , 0 >. "> ` 0 ) = <. 0 , 0 >.
37 27 36 eqtri 
 |-  ( P ` 0 ) = <. 0 , 0 >.
38 1 fveq1i 
 |-  ( P ` 1 ) = ( <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. <. 0 , 0 >. "> ` 1 )
39 opex 
 |-  <. 0 , 1 >. e. _V
40 s4fv1 
 |-  ( <. 0 , 1 >. e. _V -> ( <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. "> ` 1 ) = <. 0 , 1 >. )
41 1nn0 
 |-  1 e. NN0
42 1lt4 
 |-  1 < 4
43 29 30 31 40 41 42 cats1fv 
 |-  ( <. 0 , 1 >. e. _V -> ( <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. <. 0 , 0 >. "> ` 1 ) = <. 0 , 1 >. )
44 39 43 ax-mp 
 |-  ( <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. <. 0 , 0 >. "> ` 1 ) = <. 0 , 1 >.
45 38 44 eqtri 
 |-  ( P ` 1 ) = <. 0 , 1 >.
46 37 45 neeq12i 
 |-  ( ( P ` 0 ) =/= ( P ` 1 ) <-> <. 0 , 0 >. =/= <. 0 , 1 >. )
47 26 46 mpbir 
 |-  ( P ` 0 ) =/= ( P ` 1 )
48 47 a1i 
 |-  ( ( Y = 1 /\ X = 0 ) -> ( P ` 0 ) =/= ( P ` 1 ) )
49 fveq2 
 |-  ( X = 0 -> ( P ` X ) = ( P ` 0 ) )
50 49 adantl 
 |-  ( ( Y = 1 /\ X = 0 ) -> ( P ` X ) = ( P ` 0 ) )
51 fveq2 
 |-  ( Y = 1 -> ( P ` Y ) = ( P ` 1 ) )
52 51 adantr 
 |-  ( ( Y = 1 /\ X = 0 ) -> ( P ` Y ) = ( P ` 1 ) )
53 48 50 52 3netr4d 
 |-  ( ( Y = 1 /\ X = 0 ) -> ( P ` X ) =/= ( P ` Y ) )
54 53 a1d 
 |-  ( ( Y = 1 /\ X = 0 ) -> ( X =/= Y -> ( P ` X ) =/= ( P ` Y ) ) )
55 54 ex 
 |-  ( Y = 1 -> ( X = 0 -> ( X =/= Y -> ( P ` X ) =/= ( P ` Y ) ) ) )
56 22 orci 
 |-  ( 0 =/= 1 \/ 0 =/= 1 )
57 24 24 opthne 
 |-  ( <. 0 , 0 >. =/= <. 1 , 1 >. <-> ( 0 =/= 1 \/ 0 =/= 1 ) )
58 56 57 mpbir 
 |-  <. 0 , 0 >. =/= <. 1 , 1 >.
59 1 fveq1i 
 |-  ( P ` 2 ) = ( <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. <. 0 , 0 >. "> ` 2 )
60 opex 
 |-  <. 1 , 1 >. e. _V
61 s4fv2 
 |-  ( <. 1 , 1 >. e. _V -> ( <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. "> ` 2 ) = <. 1 , 1 >. )
62 2nn0 
 |-  2 e. NN0
63 2lt4 
 |-  2 < 4
64 29 30 31 61 62 63 cats1fv 
 |-  ( <. 1 , 1 >. e. _V -> ( <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. <. 0 , 0 >. "> ` 2 ) = <. 1 , 1 >. )
65 60 64 ax-mp 
 |-  ( <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. <. 0 , 0 >. "> ` 2 ) = <. 1 , 1 >.
66 59 65 eqtri 
 |-  ( P ` 2 ) = <. 1 , 1 >.
67 37 66 neeq12i 
 |-  ( ( P ` 0 ) =/= ( P ` 2 ) <-> <. 0 , 0 >. =/= <. 1 , 1 >. )
68 58 67 mpbir 
 |-  ( P ` 0 ) =/= ( P ` 2 )
69 68 a1i 
 |-  ( ( Y = 2 /\ X = 0 ) -> ( P ` 0 ) =/= ( P ` 2 ) )
70 49 adantl 
 |-  ( ( Y = 2 /\ X = 0 ) -> ( P ` X ) = ( P ` 0 ) )
71 fveq2 
 |-  ( Y = 2 -> ( P ` Y ) = ( P ` 2 ) )
72 71 adantr 
 |-  ( ( Y = 2 /\ X = 0 ) -> ( P ` Y ) = ( P ` 2 ) )
73 69 70 72 3netr4d 
 |-  ( ( Y = 2 /\ X = 0 ) -> ( P ` X ) =/= ( P ` Y ) )
74 73 a1d 
 |-  ( ( Y = 2 /\ X = 0 ) -> ( X =/= Y -> ( P ` X ) =/= ( P ` Y ) ) )
75 74 ex 
 |-  ( Y = 2 -> ( X = 0 -> ( X =/= Y -> ( P ` X ) =/= ( P ` Y ) ) ) )
76 22 orci 
 |-  ( 0 =/= 1 \/ 0 =/= 0 )
77 24 24 opthne 
 |-  ( <. 0 , 0 >. =/= <. 1 , 0 >. <-> ( 0 =/= 1 \/ 0 =/= 0 ) )
78 76 77 mpbir 
 |-  <. 0 , 0 >. =/= <. 1 , 0 >.
79 1 fveq1i 
 |-  ( P ` 3 ) = ( <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. <. 0 , 0 >. "> ` 3 )
80 opex 
 |-  <. 1 , 0 >. e. _V
81 s4fv3 
 |-  ( <. 1 , 0 >. e. _V -> ( <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. "> ` 3 ) = <. 1 , 0 >. )
82 3nn0 
 |-  3 e. NN0
83 3lt4 
 |-  3 < 4
84 29 30 31 81 82 83 cats1fv 
 |-  ( <. 1 , 0 >. e. _V -> ( <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. <. 0 , 0 >. "> ` 3 ) = <. 1 , 0 >. )
85 80 84 ax-mp 
 |-  ( <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. <. 0 , 0 >. "> ` 3 ) = <. 1 , 0 >.
86 79 85 eqtri 
 |-  ( P ` 3 ) = <. 1 , 0 >.
87 37 86 neeq12i 
 |-  ( ( P ` 0 ) =/= ( P ` 3 ) <-> <. 0 , 0 >. =/= <. 1 , 0 >. )
88 78 87 mpbir 
 |-  ( P ` 0 ) =/= ( P ` 3 )
89 88 a1i 
 |-  ( ( Y = 3 /\ X = 0 ) -> ( P ` 0 ) =/= ( P ` 3 ) )
90 49 adantl 
 |-  ( ( Y = 3 /\ X = 0 ) -> ( P ` X ) = ( P ` 0 ) )
91 fveq2 
 |-  ( Y = 3 -> ( P ` Y ) = ( P ` 3 ) )
92 91 adantr 
 |-  ( ( Y = 3 /\ X = 0 ) -> ( P ` Y ) = ( P ` 3 ) )
93 89 90 92 3netr4d 
 |-  ( ( Y = 3 /\ X = 0 ) -> ( P ` X ) =/= ( P ` Y ) )
94 93 a1d 
 |-  ( ( Y = 3 /\ X = 0 ) -> ( X =/= Y -> ( P ` X ) =/= ( P ` Y ) ) )
95 94 ex 
 |-  ( Y = 3 -> ( X = 0 -> ( X =/= Y -> ( P ` X ) =/= ( P ` Y ) ) ) )
96 55 75 95 3jaoi 
 |-  ( ( Y = 1 \/ Y = 2 \/ Y = 3 ) -> ( X = 0 -> ( X =/= Y -> ( P ` X ) =/= ( P ` Y ) ) ) )
97 eltpi 
 |-  ( Y e. { 1 , 2 , 3 } -> ( Y = 1 \/ Y = 2 \/ Y = 3 ) )
98 96 97 syl11 
 |-  ( X = 0 -> ( Y e. { 1 , 2 , 3 } -> ( X =/= Y -> ( P ` X ) =/= ( P ` Y ) ) ) )
99 simpr 
 |-  ( ( Y = 1 /\ X = 1 ) -> X = 1 )
100 simpl 
 |-  ( ( Y = 1 /\ X = 1 ) -> Y = 1 )
101 99 100 neeq12d 
 |-  ( ( Y = 1 /\ X = 1 ) -> ( X =/= Y <-> 1 =/= 1 ) )
102 eqid 
 |-  1 = 1
103 eqneqall 
 |-  ( 1 = 1 -> ( 1 =/= 1 -> ( P ` X ) =/= ( P ` Y ) ) )
104 102 103 ax-mp 
 |-  ( 1 =/= 1 -> ( P ` X ) =/= ( P ` Y ) )
105 101 104 biimtrdi 
 |-  ( ( Y = 1 /\ X = 1 ) -> ( X =/= Y -> ( P ` X ) =/= ( P ` Y ) ) )
106 105 ex 
 |-  ( Y = 1 -> ( X = 1 -> ( X =/= Y -> ( P ` X ) =/= ( P ` Y ) ) ) )
107 22 orci 
 |-  ( 0 =/= 1 \/ 1 =/= 1 )
108 1ex 
 |-  1 e. _V
109 24 108 opthne 
 |-  ( <. 0 , 1 >. =/= <. 1 , 1 >. <-> ( 0 =/= 1 \/ 1 =/= 1 ) )
110 107 109 mpbir 
 |-  <. 0 , 1 >. =/= <. 1 , 1 >.
111 45 66 neeq12i 
 |-  ( ( P ` 1 ) =/= ( P ` 2 ) <-> <. 0 , 1 >. =/= <. 1 , 1 >. )
112 110 111 mpbir 
 |-  ( P ` 1 ) =/= ( P ` 2 )
113 112 a1i 
 |-  ( ( Y = 2 /\ X = 1 ) -> ( P ` 1 ) =/= ( P ` 2 ) )
114 fveq2 
 |-  ( X = 1 -> ( P ` X ) = ( P ` 1 ) )
115 114 adantl 
 |-  ( ( Y = 2 /\ X = 1 ) -> ( P ` X ) = ( P ` 1 ) )
116 71 adantr 
 |-  ( ( Y = 2 /\ X = 1 ) -> ( P ` Y ) = ( P ` 2 ) )
117 113 115 116 3netr4d 
 |-  ( ( Y = 2 /\ X = 1 ) -> ( P ` X ) =/= ( P ` Y ) )
118 117 a1d 
 |-  ( ( Y = 2 /\ X = 1 ) -> ( X =/= Y -> ( P ` X ) =/= ( P ` Y ) ) )
119 118 ex 
 |-  ( Y = 2 -> ( X = 1 -> ( X =/= Y -> ( P ` X ) =/= ( P ` Y ) ) ) )
120 22 orci 
 |-  ( 0 =/= 1 \/ 1 =/= 0 )
121 24 108 opthne 
 |-  ( <. 0 , 1 >. =/= <. 1 , 0 >. <-> ( 0 =/= 1 \/ 1 =/= 0 ) )
122 120 121 mpbir 
 |-  <. 0 , 1 >. =/= <. 1 , 0 >.
123 45 86 neeq12i 
 |-  ( ( P ` 1 ) =/= ( P ` 3 ) <-> <. 0 , 1 >. =/= <. 1 , 0 >. )
124 122 123 mpbir 
 |-  ( P ` 1 ) =/= ( P ` 3 )
125 124 a1i 
 |-  ( ( Y = 3 /\ X = 1 ) -> ( P ` 1 ) =/= ( P ` 3 ) )
126 114 adantl 
 |-  ( ( Y = 3 /\ X = 1 ) -> ( P ` X ) = ( P ` 1 ) )
127 91 adantr 
 |-  ( ( Y = 3 /\ X = 1 ) -> ( P ` Y ) = ( P ` 3 ) )
128 125 126 127 3netr4d 
 |-  ( ( Y = 3 /\ X = 1 ) -> ( P ` X ) =/= ( P ` Y ) )
129 128 a1d 
 |-  ( ( Y = 3 /\ X = 1 ) -> ( X =/= Y -> ( P ` X ) =/= ( P ` Y ) ) )
130 129 ex 
 |-  ( Y = 3 -> ( X = 1 -> ( X =/= Y -> ( P ` X ) =/= ( P ` Y ) ) ) )
131 106 119 130 3jaoi 
 |-  ( ( Y = 1 \/ Y = 2 \/ Y = 3 ) -> ( X = 1 -> ( X =/= Y -> ( P ` X ) =/= ( P ` Y ) ) ) )
132 131 97 syl11 
 |-  ( X = 1 -> ( Y e. { 1 , 2 , 3 } -> ( X =/= Y -> ( P ` X ) =/= ( P ` Y ) ) ) )
133 98 132 jaoi 
 |-  ( ( X = 0 \/ X = 1 ) -> ( Y e. { 1 , 2 , 3 } -> ( X =/= Y -> ( P ` X ) =/= ( P ` Y ) ) ) )
134 21 133 syl 
 |-  ( X e. { 0 , 1 } -> ( Y e. { 1 , 2 , 3 } -> ( X =/= Y -> ( P ` X ) =/= ( P ` Y ) ) ) )
135 elpri 
 |-  ( X e. { 2 , 3 } -> ( X = 2 \/ X = 3 ) )
136 112 necomi 
 |-  ( P ` 2 ) =/= ( P ` 1 )
137 136 a1i 
 |-  ( ( Y = 1 /\ X = 2 ) -> ( P ` 2 ) =/= ( P ` 1 ) )
138 fveq2 
 |-  ( X = 2 -> ( P ` X ) = ( P ` 2 ) )
139 138 adantl 
 |-  ( ( Y = 1 /\ X = 2 ) -> ( P ` X ) = ( P ` 2 ) )
140 51 adantr 
 |-  ( ( Y = 1 /\ X = 2 ) -> ( P ` Y ) = ( P ` 1 ) )
141 137 139 140 3netr4d 
 |-  ( ( Y = 1 /\ X = 2 ) -> ( P ` X ) =/= ( P ` Y ) )
142 141 a1d 
 |-  ( ( Y = 1 /\ X = 2 ) -> ( X =/= Y -> ( P ` X ) =/= ( P ` Y ) ) )
143 142 ex 
 |-  ( Y = 1 -> ( X = 2 -> ( X =/= Y -> ( P ` X ) =/= ( P ` Y ) ) ) )
144 simpr 
 |-  ( ( Y = 2 /\ X = 2 ) -> X = 2 )
145 simpl 
 |-  ( ( Y = 2 /\ X = 2 ) -> Y = 2 )
146 144 145 neeq12d 
 |-  ( ( Y = 2 /\ X = 2 ) -> ( X =/= Y <-> 2 =/= 2 ) )
147 eqid 
 |-  2 = 2
148 eqneqall 
 |-  ( 2 = 2 -> ( 2 =/= 2 -> ( P ` X ) =/= ( P ` Y ) ) )
149 147 148 ax-mp 
 |-  ( 2 =/= 2 -> ( P ` X ) =/= ( P ` Y ) )
150 146 149 biimtrdi 
 |-  ( ( Y = 2 /\ X = 2 ) -> ( X =/= Y -> ( P ` X ) =/= ( P ` Y ) ) )
151 150 ex 
 |-  ( Y = 2 -> ( X = 2 -> ( X =/= Y -> ( P ` X ) =/= ( P ` Y ) ) ) )
152 22 necomi 
 |-  1 =/= 0
153 152 olci 
 |-  ( 1 =/= 1 \/ 1 =/= 0 )
154 108 108 opthne 
 |-  ( <. 1 , 1 >. =/= <. 1 , 0 >. <-> ( 1 =/= 1 \/ 1 =/= 0 ) )
155 153 154 mpbir 
 |-  <. 1 , 1 >. =/= <. 1 , 0 >.
156 66 86 neeq12i 
 |-  ( ( P ` 2 ) =/= ( P ` 3 ) <-> <. 1 , 1 >. =/= <. 1 , 0 >. )
157 155 156 mpbir 
 |-  ( P ` 2 ) =/= ( P ` 3 )
158 157 a1i 
 |-  ( ( Y = 3 /\ X = 2 ) -> ( P ` 2 ) =/= ( P ` 3 ) )
159 138 adantl 
 |-  ( ( Y = 3 /\ X = 2 ) -> ( P ` X ) = ( P ` 2 ) )
160 91 adantr 
 |-  ( ( Y = 3 /\ X = 2 ) -> ( P ` Y ) = ( P ` 3 ) )
161 158 159 160 3netr4d 
 |-  ( ( Y = 3 /\ X = 2 ) -> ( P ` X ) =/= ( P ` Y ) )
162 161 a1d 
 |-  ( ( Y = 3 /\ X = 2 ) -> ( X =/= Y -> ( P ` X ) =/= ( P ` Y ) ) )
163 162 ex 
 |-  ( Y = 3 -> ( X = 2 -> ( X =/= Y -> ( P ` X ) =/= ( P ` Y ) ) ) )
164 143 151 163 3jaoi 
 |-  ( ( Y = 1 \/ Y = 2 \/ Y = 3 ) -> ( X = 2 -> ( X =/= Y -> ( P ` X ) =/= ( P ` Y ) ) ) )
165 164 97 syl11 
 |-  ( X = 2 -> ( Y e. { 1 , 2 , 3 } -> ( X =/= Y -> ( P ` X ) =/= ( P ` Y ) ) ) )
166 124 necomi 
 |-  ( P ` 3 ) =/= ( P ` 1 )
167 166 a1i 
 |-  ( ( Y = 1 /\ X = 3 ) -> ( P ` 3 ) =/= ( P ` 1 ) )
168 fveq2 
 |-  ( X = 3 -> ( P ` X ) = ( P ` 3 ) )
169 168 adantl 
 |-  ( ( Y = 1 /\ X = 3 ) -> ( P ` X ) = ( P ` 3 ) )
170 51 adantr 
 |-  ( ( Y = 1 /\ X = 3 ) -> ( P ` Y ) = ( P ` 1 ) )
171 167 169 170 3netr4d 
 |-  ( ( Y = 1 /\ X = 3 ) -> ( P ` X ) =/= ( P ` Y ) )
172 171 a1d 
 |-  ( ( Y = 1 /\ X = 3 ) -> ( X =/= Y -> ( P ` X ) =/= ( P ` Y ) ) )
173 172 ex 
 |-  ( Y = 1 -> ( X = 3 -> ( X =/= Y -> ( P ` X ) =/= ( P ` Y ) ) ) )
174 157 necomi 
 |-  ( P ` 3 ) =/= ( P ` 2 )
175 174 a1i 
 |-  ( ( Y = 2 /\ X = 3 ) -> ( P ` 3 ) =/= ( P ` 2 ) )
176 168 adantl 
 |-  ( ( Y = 2 /\ X = 3 ) -> ( P ` X ) = ( P ` 3 ) )
177 71 adantr 
 |-  ( ( Y = 2 /\ X = 3 ) -> ( P ` Y ) = ( P ` 2 ) )
178 175 176 177 3netr4d 
 |-  ( ( Y = 2 /\ X = 3 ) -> ( P ` X ) =/= ( P ` Y ) )
179 178 a1d 
 |-  ( ( Y = 2 /\ X = 3 ) -> ( X =/= Y -> ( P ` X ) =/= ( P ` Y ) ) )
180 179 ex 
 |-  ( Y = 2 -> ( X = 3 -> ( X =/= Y -> ( P ` X ) =/= ( P ` Y ) ) ) )
181 simpr 
 |-  ( ( Y = 3 /\ X = 3 ) -> X = 3 )
182 simpl 
 |-  ( ( Y = 3 /\ X = 3 ) -> Y = 3 )
183 181 182 neeq12d 
 |-  ( ( Y = 3 /\ X = 3 ) -> ( X =/= Y <-> 3 =/= 3 ) )
184 eqid 
 |-  3 = 3
185 eqneqall 
 |-  ( 3 = 3 -> ( 3 =/= 3 -> ( P ` X ) =/= ( P ` Y ) ) )
186 184 185 ax-mp 
 |-  ( 3 =/= 3 -> ( P ` X ) =/= ( P ` Y ) )
187 183 186 biimtrdi 
 |-  ( ( Y = 3 /\ X = 3 ) -> ( X =/= Y -> ( P ` X ) =/= ( P ` Y ) ) )
188 187 ex 
 |-  ( Y = 3 -> ( X = 3 -> ( X =/= Y -> ( P ` X ) =/= ( P ` Y ) ) ) )
189 173 180 188 3jaoi 
 |-  ( ( Y = 1 \/ Y = 2 \/ Y = 3 ) -> ( X = 3 -> ( X =/= Y -> ( P ` X ) =/= ( P ` Y ) ) ) )
190 189 97 syl11 
 |-  ( X = 3 -> ( Y e. { 1 , 2 , 3 } -> ( X =/= Y -> ( P ` X ) =/= ( P ` Y ) ) ) )
191 165 190 jaoi 
 |-  ( ( X = 2 \/ X = 3 ) -> ( Y e. { 1 , 2 , 3 } -> ( X =/= Y -> ( P ` X ) =/= ( P ` Y ) ) ) )
192 135 191 syl 
 |-  ( X e. { 2 , 3 } -> ( Y e. { 1 , 2 , 3 } -> ( X =/= Y -> ( P ` X ) =/= ( P ` Y ) ) ) )
193 134 192 jaoi 
 |-  ( ( X e. { 0 , 1 } \/ X e. { 2 , 3 } ) -> ( Y e. { 1 , 2 , 3 } -> ( X =/= Y -> ( P ` X ) =/= ( P ` Y ) ) ) )
194 elsni 
 |-  ( X e. { 4 } -> X = 4 )
195 1 fveq1i 
 |-  ( P ` 4 ) = ( <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. <. 0 , 0 >. "> ` 4 )
196 29 30 31 cats1fvn 
 |-  ( <. 0 , 0 >. e. _V -> ( <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. <. 0 , 0 >. "> ` 4 ) = <. 0 , 0 >. )
197 28 196 ax-mp 
 |-  ( <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. <. 0 , 0 >. "> ` 4 ) = <. 0 , 0 >.
198 195 197 eqtri 
 |-  ( P ` 4 ) = <. 0 , 0 >.
199 198 45 neeq12i 
 |-  ( ( P ` 4 ) =/= ( P ` 1 ) <-> <. 0 , 0 >. =/= <. 0 , 1 >. )
200 26 199 mpbir 
 |-  ( P ` 4 ) =/= ( P ` 1 )
201 200 a1i 
 |-  ( ( Y = 1 /\ X = 4 ) -> ( P ` 4 ) =/= ( P ` 1 ) )
202 fveq2 
 |-  ( X = 4 -> ( P ` X ) = ( P ` 4 ) )
203 202 adantl 
 |-  ( ( Y = 1 /\ X = 4 ) -> ( P ` X ) = ( P ` 4 ) )
204 51 adantr 
 |-  ( ( Y = 1 /\ X = 4 ) -> ( P ` Y ) = ( P ` 1 ) )
205 201 203 204 3netr4d 
 |-  ( ( Y = 1 /\ X = 4 ) -> ( P ` X ) =/= ( P ` Y ) )
206 205 a1d 
 |-  ( ( Y = 1 /\ X = 4 ) -> ( X =/= Y -> ( P ` X ) =/= ( P ` Y ) ) )
207 206 ex 
 |-  ( Y = 1 -> ( X = 4 -> ( X =/= Y -> ( P ` X ) =/= ( P ` Y ) ) ) )
208 198 66 neeq12i 
 |-  ( ( P ` 4 ) =/= ( P ` 2 ) <-> <. 0 , 0 >. =/= <. 1 , 1 >. )
209 58 208 mpbir 
 |-  ( P ` 4 ) =/= ( P ` 2 )
210 209 a1i 
 |-  ( ( Y = 2 /\ X = 4 ) -> ( P ` 4 ) =/= ( P ` 2 ) )
211 202 adantl 
 |-  ( ( Y = 2 /\ X = 4 ) -> ( P ` X ) = ( P ` 4 ) )
212 71 adantr 
 |-  ( ( Y = 2 /\ X = 4 ) -> ( P ` Y ) = ( P ` 2 ) )
213 210 211 212 3netr4d 
 |-  ( ( Y = 2 /\ X = 4 ) -> ( P ` X ) =/= ( P ` Y ) )
214 213 a1d 
 |-  ( ( Y = 2 /\ X = 4 ) -> ( X =/= Y -> ( P ` X ) =/= ( P ` Y ) ) )
215 214 ex 
 |-  ( Y = 2 -> ( X = 4 -> ( X =/= Y -> ( P ` X ) =/= ( P ` Y ) ) ) )
216 198 86 neeq12i 
 |-  ( ( P ` 4 ) =/= ( P ` 3 ) <-> <. 0 , 0 >. =/= <. 1 , 0 >. )
217 78 216 mpbir 
 |-  ( P ` 4 ) =/= ( P ` 3 )
218 217 a1i 
 |-  ( ( Y = 3 /\ X = 4 ) -> ( P ` 4 ) =/= ( P ` 3 ) )
219 202 adantl 
 |-  ( ( Y = 3 /\ X = 4 ) -> ( P ` X ) = ( P ` 4 ) )
220 91 adantr 
 |-  ( ( Y = 3 /\ X = 4 ) -> ( P ` Y ) = ( P ` 3 ) )
221 218 219 220 3netr4d 
 |-  ( ( Y = 3 /\ X = 4 ) -> ( P ` X ) =/= ( P ` Y ) )
222 221 a1d 
 |-  ( ( Y = 3 /\ X = 4 ) -> ( X =/= Y -> ( P ` X ) =/= ( P ` Y ) ) )
223 222 ex 
 |-  ( Y = 3 -> ( X = 4 -> ( X =/= Y -> ( P ` X ) =/= ( P ` Y ) ) ) )
224 207 215 223 3jaoi 
 |-  ( ( Y = 1 \/ Y = 2 \/ Y = 3 ) -> ( X = 4 -> ( X =/= Y -> ( P ` X ) =/= ( P ` Y ) ) ) )
225 97 194 224 syl2imc 
 |-  ( X e. { 4 } -> ( Y e. { 1 , 2 , 3 } -> ( X =/= Y -> ( P ` X ) =/= ( P ` Y ) ) ) )
226 193 225 jaoi 
 |-  ( ( ( X e. { 0 , 1 } \/ X e. { 2 , 3 } ) \/ X e. { 4 } ) -> ( Y e. { 1 , 2 , 3 } -> ( X =/= Y -> ( P ` X ) =/= ( P ` Y ) ) ) )
227 20 226 sylbi 
 |-  ( X e. ( ( { 0 , 1 } u. { 2 , 3 } ) u. { 4 } ) -> ( Y e. { 1 , 2 , 3 } -> ( X =/= Y -> ( P ` X ) =/= ( P ` Y ) ) ) )
228 227 imp 
 |-  ( ( X e. ( ( { 0 , 1 } u. { 2 , 3 } ) u. { 4 } ) /\ Y e. { 1 , 2 , 3 } ) -> ( X =/= Y -> ( P ` X ) =/= ( P ` Y ) ) )
229 14 16 228 syl2anb 
 |-  ( ( X e. ( 0 ..^ ( # ` P ) ) /\ Y e. ( 1 ..^ 4 ) ) -> ( X =/= Y -> ( P ` X ) =/= ( P ` Y ) ) )