Metamath Proof Explorer


Theorem s3f1

Description: Conditions for a length 3 string to be a one-to-one function. (Contributed by Thierry Arnoux, 19-Sep-2023)

Ref Expression
Hypotheses s3f1.i φ I D
s3f1.j φ J D
s3f1.k φ K D
s3f1.1 φ I J
s3f1.2 φ J K
s3f1.3 φ K I
Assertion s3f1 φ ⟨“ IJK ”⟩ : dom ⟨“ IJK ”⟩ 1-1 D

Proof

Step Hyp Ref Expression
1 s3f1.i φ I D
2 s3f1.j φ J D
3 s3f1.k φ K D
4 s3f1.1 φ I J
5 s3f1.2 φ J K
6 s3f1.3 φ K I
7 1 2 3 s3cld φ ⟨“ IJK ”⟩ Word D
8 wrdf ⟨“ IJK ”⟩ Word D ⟨“ IJK ”⟩ : 0 ..^ ⟨“ IJK ”⟩ D
9 7 8 syl φ ⟨“ IJK ”⟩ : 0 ..^ ⟨“ IJK ”⟩ D
10 9 ffdmd φ ⟨“ IJK ”⟩ : dom ⟨“ IJK ”⟩ D
11 simplr φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j i = 0 j = 0 i = 0
12 simpr φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j i = 0 j = 0 j = 0
13 11 12 eqtr4d φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j i = 0 j = 0 i = j
14 simpllr φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j i = 0 j = 1 ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j
15 simpr φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j i = 0 i = 0
16 15 fveq2d φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j i = 0 ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ 0
17 s3fv0 I D ⟨“ IJK ”⟩ 0 = I
18 1 17 syl φ ⟨“ IJK ”⟩ 0 = I
19 18 ad4antr φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j i = 0 ⟨“ IJK ”⟩ 0 = I
20 16 19 eqtrd φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j i = 0 ⟨“ IJK ”⟩ i = I
21 20 adantr φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j i = 0 j = 1 ⟨“ IJK ”⟩ i = I
22 simpr φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j j = 1 j = 1
23 22 fveq2d φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j j = 1 ⟨“ IJK ”⟩ j = ⟨“ IJK ”⟩ 1
24 s3fv1 J D ⟨“ IJK ”⟩ 1 = J
25 2 24 syl φ ⟨“ IJK ”⟩ 1 = J
26 25 ad4antr φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j j = 1 ⟨“ IJK ”⟩ 1 = J
27 23 26 eqtrd φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j j = 1 ⟨“ IJK ”⟩ j = J
28 27 adantlr φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j i = 0 j = 1 ⟨“ IJK ”⟩ j = J
29 14 21 28 3eqtr3d φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j i = 0 j = 1 I = J
30 4 ad5antr φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j i = 0 j = 1 I J
31 29 30 pm2.21ddne φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j i = 0 j = 1 i = j
32 simpllr φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j i = 0 j = 2 ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j
33 20 adantr φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j i = 0 j = 2 ⟨“ IJK ”⟩ i = I
34 simpr φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j j = 2 j = 2
35 34 fveq2d φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j j = 2 ⟨“ IJK ”⟩ j = ⟨“ IJK ”⟩ 2
36 s3fv2 K D ⟨“ IJK ”⟩ 2 = K
37 3 36 syl φ ⟨“ IJK ”⟩ 2 = K
38 37 ad4antr φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j j = 2 ⟨“ IJK ”⟩ 2 = K
39 35 38 eqtrd φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j j = 2 ⟨“ IJK ”⟩ j = K
40 39 adantlr φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j i = 0 j = 2 ⟨“ IJK ”⟩ j = K
41 32 33 40 3eqtr3rd φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j i = 0 j = 2 K = I
42 6 ad5antr φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j i = 0 j = 2 K I
43 41 42 pm2.21ddne φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j i = 0 j = 2 i = j
44 wrddm ⟨“ IJK ”⟩ Word D dom ⟨“ IJK ”⟩ = 0 ..^ ⟨“ IJK ”⟩
45 7 44 syl φ dom ⟨“ IJK ”⟩ = 0 ..^ ⟨“ IJK ”⟩
46 s3len ⟨“ IJK ”⟩ = 3
47 46 oveq2i 0 ..^ ⟨“ IJK ”⟩ = 0 ..^ 3
48 fzo0to3tp 0 ..^ 3 = 0 1 2
49 47 48 eqtri 0 ..^ ⟨“ IJK ”⟩ = 0 1 2
50 45 49 eqtrdi φ dom ⟨“ IJK ”⟩ = 0 1 2
51 50 eleq2d φ j dom ⟨“ IJK ”⟩ j 0 1 2
52 51 biimpa φ j dom ⟨“ IJK ”⟩ j 0 1 2
53 vex j V
54 53 eltp j 0 1 2 j = 0 j = 1 j = 2
55 52 54 sylib φ j dom ⟨“ IJK ”⟩ j = 0 j = 1 j = 2
56 55 adantlr φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ j = 0 j = 1 j = 2
57 56 ad2antrr φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j i = 0 j = 0 j = 1 j = 2
58 13 31 43 57 mpjao3dan φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j i = 0 i = j
59 simpllr φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j i = 1 j = 0 ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j
60 simpr φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j i = 1 i = 1
61 60 fveq2d φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j i = 1 ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ 1
62 25 ad4antr φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j i = 1 ⟨“ IJK ”⟩ 1 = J
63 61 62 eqtrd φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j i = 1 ⟨“ IJK ”⟩ i = J
64 63 adantr φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j i = 1 j = 0 ⟨“ IJK ”⟩ i = J
65 simpr φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j j = 0 j = 0
66 65 fveq2d φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j j = 0 ⟨“ IJK ”⟩ j = ⟨“ IJK ”⟩ 0
67 18 ad4antr φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j j = 0 ⟨“ IJK ”⟩ 0 = I
68 66 67 eqtrd φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j j = 0 ⟨“ IJK ”⟩ j = I
69 68 adantlr φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j i = 1 j = 0 ⟨“ IJK ”⟩ j = I
70 59 64 69 3eqtr3rd φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j i = 1 j = 0 I = J
71 4 ad5antr φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j i = 1 j = 0 I J
72 70 71 pm2.21ddne φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j i = 1 j = 0 i = j
73 simplr φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j i = 1 j = 1 i = 1
74 simpr φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j i = 1 j = 1 j = 1
75 73 74 eqtr4d φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j i = 1 j = 1 i = j
76 simpllr φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j i = 1 j = 2 ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j
77 63 adantr φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j i = 1 j = 2 ⟨“ IJK ”⟩ i = J
78 39 adantlr φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j i = 1 j = 2 ⟨“ IJK ”⟩ j = K
79 76 77 78 3eqtr3d φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j i = 1 j = 2 J = K
80 5 ad5antr φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j i = 1 j = 2 J K
81 79 80 pm2.21ddne φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j i = 1 j = 2 i = j
82 56 ad2antrr φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j i = 1 j = 0 j = 1 j = 2
83 72 75 81 82 mpjao3dan φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j i = 1 i = j
84 simpllr φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j i = 2 j = 0 ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j
85 simpr φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j i = 2 i = 2
86 85 fveq2d φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j i = 2 ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ 2
87 37 ad4antr φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j i = 2 ⟨“ IJK ”⟩ 2 = K
88 86 87 eqtrd φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j i = 2 ⟨“ IJK ”⟩ i = K
89 88 adantr φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j i = 2 j = 0 ⟨“ IJK ”⟩ i = K
90 68 adantlr φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j i = 2 j = 0 ⟨“ IJK ”⟩ j = I
91 84 89 90 3eqtr3d φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j i = 2 j = 0 K = I
92 6 ad5antr φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j i = 2 j = 0 K I
93 91 92 pm2.21ddne φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j i = 2 j = 0 i = j
94 simpllr φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j i = 2 j = 1 ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j
95 88 adantr φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j i = 2 j = 1 ⟨“ IJK ”⟩ i = K
96 27 adantlr φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j i = 2 j = 1 ⟨“ IJK ”⟩ j = J
97 94 95 96 3eqtr3rd φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j i = 2 j = 1 J = K
98 5 ad5antr φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j i = 2 j = 1 J K
99 97 98 pm2.21ddne φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j i = 2 j = 1 i = j
100 simplr φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j i = 2 j = 2 i = 2
101 simpr φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j i = 2 j = 2 j = 2
102 100 101 eqtr4d φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j i = 2 j = 2 i = j
103 56 ad2antrr φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j i = 2 j = 0 j = 1 j = 2
104 93 99 102 103 mpjao3dan φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j i = 2 i = j
105 50 eleq2d φ i dom ⟨“ IJK ”⟩ i 0 1 2
106 105 biimpa φ i dom ⟨“ IJK ”⟩ i 0 1 2
107 vex i V
108 107 eltp i 0 1 2 i = 0 i = 1 i = 2
109 106 108 sylib φ i dom ⟨“ IJK ”⟩ i = 0 i = 1 i = 2
110 109 ad2antrr φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j i = 0 i = 1 i = 2
111 58 83 104 110 mpjao3dan φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j i = j
112 111 ex φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j i = j
113 112 anasss φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j i = j
114 113 ralrimivva φ i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j i = j
115 dff13 ⟨“ IJK ”⟩ : dom ⟨“ IJK ”⟩ 1-1 D ⟨“ IJK ”⟩ : dom ⟨“ IJK ”⟩ D i dom ⟨“ IJK ”⟩ j dom ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ i = ⟨“ IJK ”⟩ j i = j
116 10 114 115 sylanbrc φ ⟨“ IJK ”⟩ : dom ⟨“ IJK ”⟩ 1-1 D