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 ⊢ 𝑃 = ⟨“ ⟨ 0 , 0 ⟩ ⟨ 0 , 1 ⟩ ⟨ 1 , 1 ⟩ ⟨ 1 , 0 ⟩ ⟨ 0 , 0 ⟩ ”⟩
Assertion gpgprismgr4cycllem7 ( ( 𝑋 ∈ ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ∧ 𝑌 ∈ ( 1 ..^ 4 ) ) → ( 𝑋 ≠ 𝑌 → ( 𝑃 ‘ 𝑋 ) ≠ ( 𝑃 ‘ 𝑌 ) ) )

Proof

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