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→Disjc∈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”⟩∈WordV
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”⟩∈WordV∧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∈Zc=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 ⊢Disjc∈Z⟨“ABc”⟩↔∀c∈Z∀d∈Zc=d∨⟨“ABc”⟩∩⟨“ABd”⟩=∅
35 28 34 sylibr ⊢A∈X∧B∈Y→Disjc∈Z⟨“ABc”⟩