# 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 ${⊢}\left({A}\in {X}\wedge {B}\in {Y}\right)\to \underset{{c}\in {Z}}{Disj}\left\{⟨“{A}{B}{c}”⟩\right\}$

### Proof

Step Hyp Ref Expression
1 orc ${⊢}{c}={d}\to \left({c}={d}\vee \left\{⟨“{A}{B}{c}”⟩\right\}\cap \left\{⟨“{A}{B}{d}”⟩\right\}=\varnothing \right)$
2 1 a1d ${⊢}{c}={d}\to \left(\left(\left({A}\in {X}\wedge {B}\in {Y}\right)\wedge \left({c}\in {Z}\wedge {d}\in {Z}\right)\right)\to \left({c}={d}\vee \left\{⟨“{A}{B}{c}”⟩\right\}\cap \left\{⟨“{A}{B}{d}”⟩\right\}=\varnothing \right)\right)$
3 s3cli ${⊢}⟨“{A}{B}{c}”⟩\in \mathrm{Word}\mathrm{V}$
4 elex ${⊢}{A}\in {X}\to {A}\in \mathrm{V}$
5 elex ${⊢}{B}\in {Y}\to {B}\in \mathrm{V}$
6 4 5 anim12i ${⊢}\left({A}\in {X}\wedge {B}\in {Y}\right)\to \left({A}\in \mathrm{V}\wedge {B}\in \mathrm{V}\right)$
7 elex ${⊢}{d}\in {Z}\to {d}\in \mathrm{V}$
8 7 adantl ${⊢}\left({c}\in {Z}\wedge {d}\in {Z}\right)\to {d}\in \mathrm{V}$
9 6 8 anim12i ${⊢}\left(\left({A}\in {X}\wedge {B}\in {Y}\right)\wedge \left({c}\in {Z}\wedge {d}\in {Z}\right)\right)\to \left(\left({A}\in \mathrm{V}\wedge {B}\in \mathrm{V}\right)\wedge {d}\in \mathrm{V}\right)$
10 df-3an ${⊢}\left({A}\in \mathrm{V}\wedge {B}\in \mathrm{V}\wedge {d}\in \mathrm{V}\right)↔\left(\left({A}\in \mathrm{V}\wedge {B}\in \mathrm{V}\right)\wedge {d}\in \mathrm{V}\right)$
11 9 10 sylibr ${⊢}\left(\left({A}\in {X}\wedge {B}\in {Y}\right)\wedge \left({c}\in {Z}\wedge {d}\in {Z}\right)\right)\to \left({A}\in \mathrm{V}\wedge {B}\in \mathrm{V}\wedge {d}\in \mathrm{V}\right)$
12 eqwrds3 ${⊢}\left(⟨“{A}{B}{c}”⟩\in \mathrm{Word}\mathrm{V}\wedge \left({A}\in \mathrm{V}\wedge {B}\in \mathrm{V}\wedge {d}\in \mathrm{V}\right)\right)\to \left(⟨“{A}{B}{c}”⟩=⟨“{A}{B}{d}”⟩↔\left(\left|⟨“{A}{B}{c}”⟩\right|=3\wedge \left(⟨“{A}{B}{c}”⟩\left(0\right)={A}\wedge ⟨“{A}{B}{c}”⟩\left(1\right)={B}\wedge ⟨“{A}{B}{c}”⟩\left(2\right)={d}\right)\right)\right)$
13 3 11 12 sylancr ${⊢}\left(\left({A}\in {X}\wedge {B}\in {Y}\right)\wedge \left({c}\in {Z}\wedge {d}\in {Z}\right)\right)\to \left(⟨“{A}{B}{c}”⟩=⟨“{A}{B}{d}”⟩↔\left(\left|⟨“{A}{B}{c}”⟩\right|=3\wedge \left(⟨“{A}{B}{c}”⟩\left(0\right)={A}\wedge ⟨“{A}{B}{c}”⟩\left(1\right)={B}\wedge ⟨“{A}{B}{c}”⟩\left(2\right)={d}\right)\right)\right)$
14 s3fv2 ${⊢}{c}\in \mathrm{V}\to ⟨“{A}{B}{c}”⟩\left(2\right)={c}$
15 14 elv ${⊢}⟨“{A}{B}{c}”⟩\left(2\right)={c}$
16 simp3 ${⊢}\left(⟨“{A}{B}{c}”⟩\left(0\right)={A}\wedge ⟨“{A}{B}{c}”⟩\left(1\right)={B}\wedge ⟨“{A}{B}{c}”⟩\left(2\right)={d}\right)\to ⟨“{A}{B}{c}”⟩\left(2\right)={d}$
17 15 16 syl5eqr ${⊢}\left(⟨“{A}{B}{c}”⟩\left(0\right)={A}\wedge ⟨“{A}{B}{c}”⟩\left(1\right)={B}\wedge ⟨“{A}{B}{c}”⟩\left(2\right)={d}\right)\to {c}={d}$
18 17 adantl ${⊢}\left(\left|⟨“{A}{B}{c}”⟩\right|=3\wedge \left(⟨“{A}{B}{c}”⟩\left(0\right)={A}\wedge ⟨“{A}{B}{c}”⟩\left(1\right)={B}\wedge ⟨“{A}{B}{c}”⟩\left(2\right)={d}\right)\right)\to {c}={d}$
19 13 18 syl6bi ${⊢}\left(\left({A}\in {X}\wedge {B}\in {Y}\right)\wedge \left({c}\in {Z}\wedge {d}\in {Z}\right)\right)\to \left(⟨“{A}{B}{c}”⟩=⟨“{A}{B}{d}”⟩\to {c}={d}\right)$
20 19 con3rr3 ${⊢}¬{c}={d}\to \left(\left(\left({A}\in {X}\wedge {B}\in {Y}\right)\wedge \left({c}\in {Z}\wedge {d}\in {Z}\right)\right)\to ¬⟨“{A}{B}{c}”⟩=⟨“{A}{B}{d}”⟩\right)$
21 20 imp ${⊢}\left(¬{c}={d}\wedge \left(\left({A}\in {X}\wedge {B}\in {Y}\right)\wedge \left({c}\in {Z}\wedge {d}\in {Z}\right)\right)\right)\to ¬⟨“{A}{B}{c}”⟩=⟨“{A}{B}{d}”⟩$
22 21 neqned ${⊢}\left(¬{c}={d}\wedge \left(\left({A}\in {X}\wedge {B}\in {Y}\right)\wedge \left({c}\in {Z}\wedge {d}\in {Z}\right)\right)\right)\to ⟨“{A}{B}{c}”⟩\ne ⟨“{A}{B}{d}”⟩$
23 disjsn2 ${⊢}⟨“{A}{B}{c}”⟩\ne ⟨“{A}{B}{d}”⟩\to \left\{⟨“{A}{B}{c}”⟩\right\}\cap \left\{⟨“{A}{B}{d}”⟩\right\}=\varnothing$
24 22 23 syl ${⊢}\left(¬{c}={d}\wedge \left(\left({A}\in {X}\wedge {B}\in {Y}\right)\wedge \left({c}\in {Z}\wedge {d}\in {Z}\right)\right)\right)\to \left\{⟨“{A}{B}{c}”⟩\right\}\cap \left\{⟨“{A}{B}{d}”⟩\right\}=\varnothing$
25 24 olcd ${⊢}\left(¬{c}={d}\wedge \left(\left({A}\in {X}\wedge {B}\in {Y}\right)\wedge \left({c}\in {Z}\wedge {d}\in {Z}\right)\right)\right)\to \left({c}={d}\vee \left\{⟨“{A}{B}{c}”⟩\right\}\cap \left\{⟨“{A}{B}{d}”⟩\right\}=\varnothing \right)$
26 25 ex ${⊢}¬{c}={d}\to \left(\left(\left({A}\in {X}\wedge {B}\in {Y}\right)\wedge \left({c}\in {Z}\wedge {d}\in {Z}\right)\right)\to \left({c}={d}\vee \left\{⟨“{A}{B}{c}”⟩\right\}\cap \left\{⟨“{A}{B}{d}”⟩\right\}=\varnothing \right)\right)$
27 2 26 pm2.61i ${⊢}\left(\left({A}\in {X}\wedge {B}\in {Y}\right)\wedge \left({c}\in {Z}\wedge {d}\in {Z}\right)\right)\to \left({c}={d}\vee \left\{⟨“{A}{B}{c}”⟩\right\}\cap \left\{⟨“{A}{B}{d}”⟩\right\}=\varnothing \right)$
28 27 ralrimivva ${⊢}\left({A}\in {X}\wedge {B}\in {Y}\right)\to \forall {c}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {d}\in {Z}\phantom{\rule{.4em}{0ex}}\left({c}={d}\vee \left\{⟨“{A}{B}{c}”⟩\right\}\cap \left\{⟨“{A}{B}{d}”⟩\right\}=\varnothing \right)$
29 eqidd ${⊢}{c}={d}\to {A}={A}$
30 eqidd ${⊢}{c}={d}\to {B}={B}$
31 id ${⊢}{c}={d}\to {c}={d}$
32 29 30 31 s3eqd ${⊢}{c}={d}\to ⟨“{A}{B}{c}”⟩=⟨“{A}{B}{d}”⟩$
33 32 sneqd ${⊢}{c}={d}\to \left\{⟨“{A}{B}{c}”⟩\right\}=\left\{⟨“{A}{B}{d}”⟩\right\}$
34 33 disjor ${⊢}\underset{{c}\in {Z}}{Disj}\left\{⟨“{A}{B}{c}”⟩\right\}↔\forall {c}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {d}\in {Z}\phantom{\rule{.4em}{0ex}}\left({c}={d}\vee \left\{⟨“{A}{B}{c}”⟩\right\}\cap \left\{⟨“{A}{B}{d}”⟩\right\}=\varnothing \right)$
35 28 34 sylibr ${⊢}\left({A}\in {X}\wedge {B}\in {Y}\right)\to \underset{{c}\in {Z}}{Disj}\left\{⟨“{A}{B}{c}”⟩\right\}$