Metamath Proof Explorer


Theorem s3sndisj

Description: The singletons consisting of length 3 strings which have distinct third symbols are disjunct. (Contributed by AV, 17-May-2021)

Ref Expression
Assertion s3sndisj A X B Y Disj c Z ⟨“ ABc ”⟩

Proof

Step Hyp Ref Expression
1 orc c = d c = d ⟨“ ABc ”⟩ ⟨“ ABd ”⟩ =
2 1 a1d c = d A X B Y c Z d Z c = d ⟨“ ABc ”⟩ ⟨“ ABd ”⟩ =
3 s3cli ⟨“ ABc ”⟩ Word V
4 elex A X A V
5 elex B Y B V
6 4 5 anim12i A X B Y A V B V
7 elex d Z d V
8 7 adantl c Z d Z d V
9 6 8 anim12i A X B Y c Z d Z A V B V d V
10 df-3an A V B V d V A V B V d V
11 9 10 sylibr A X B Y c Z d Z A V B V d V
12 eqwrds3 ⟨“ ABc ”⟩ Word V A V B V d V ⟨“ ABc ”⟩ = ⟨“ ABd ”⟩ ⟨“ ABc ”⟩ = 3 ⟨“ ABc ”⟩ 0 = A ⟨“ ABc ”⟩ 1 = B ⟨“ ABc ”⟩ 2 = d
13 3 11 12 sylancr A X B Y c Z d Z ⟨“ ABc ”⟩ = ⟨“ ABd ”⟩ ⟨“ ABc ”⟩ = 3 ⟨“ ABc ”⟩ 0 = A ⟨“ ABc ”⟩ 1 = B ⟨“ ABc ”⟩ 2 = d
14 s3fv2 c V ⟨“ ABc ”⟩ 2 = c
15 14 elv ⟨“ ABc ”⟩ 2 = c
16 simp3 ⟨“ ABc ”⟩ 0 = A ⟨“ ABc ”⟩ 1 = B ⟨“ ABc ”⟩ 2 = d ⟨“ ABc ”⟩ 2 = d
17 15 16 eqtr3id ⟨“ ABc ”⟩ 0 = A ⟨“ ABc ”⟩ 1 = B ⟨“ ABc ”⟩ 2 = d c = d
18 17 adantl ⟨“ ABc ”⟩ = 3 ⟨“ ABc ”⟩ 0 = A ⟨“ ABc ”⟩ 1 = B ⟨“ ABc ”⟩ 2 = d c = d
19 13 18 syl6bi A X B Y c Z d Z ⟨“ ABc ”⟩ = ⟨“ ABd ”⟩ c = d
20 19 con3rr3 ¬ c = d A X B Y c Z d Z ¬ ⟨“ ABc ”⟩ = ⟨“ ABd ”⟩
21 20 imp ¬ c = d A X B Y c Z d Z ¬ ⟨“ ABc ”⟩ = ⟨“ ABd ”⟩
22 21 neqned ¬ c = d A X B Y c Z d Z ⟨“ ABc ”⟩ ⟨“ ABd ”⟩
23 disjsn2 ⟨“ ABc ”⟩ ⟨“ ABd ”⟩ ⟨“ ABc ”⟩ ⟨“ ABd ”⟩ =
24 22 23 syl ¬ c = d A X B Y c Z d Z ⟨“ ABc ”⟩ ⟨“ ABd ”⟩ =
25 24 olcd ¬ c = d A X B Y c Z d Z c = d ⟨“ ABc ”⟩ ⟨“ ABd ”⟩ =
26 25 ex ¬ c = d A X B Y c Z d Z c = d ⟨“ ABc ”⟩ ⟨“ ABd ”⟩ =
27 2 26 pm2.61i A X B Y c Z d Z c = d ⟨“ ABc ”⟩ ⟨“ ABd ”⟩ =
28 27 ralrimivva A X B Y c Z d Z c = d ⟨“ ABc ”⟩ ⟨“ ABd ”⟩ =
29 eqidd c = d A = A
30 eqidd c = d B = B
31 id c = d c = d
32 29 30 31 s3eqd c = d ⟨“ ABc ”⟩ = ⟨“ ABd ”⟩
33 32 sneqd c = d ⟨“ ABc ”⟩ = ⟨“ ABd ”⟩
34 33 disjor Disj c Z ⟨“ ABc ”⟩ c Z d Z c = d ⟨“ ABc ”⟩ ⟨“ ABd ”⟩ =
35 28 34 sylibr A X B Y Disj c Z ⟨“ ABc ”⟩