Metamath Proof Explorer

Theorem s3iunsndisj

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

Ref Expression
Assertion s3iunsndisj ⊢B∈X→Disja∈Y⋃c∈Z∖a⟨“aBc”⟩

Proof

Step Hyp Ref Expression
1 orc ⊢a=d→a=d∨⋃c∈Z∖a⟨“aBc”⟩∩⋃c∈Z∖d⟨“dBc”⟩=∅
2 1 a1d ⊢a=d→B∈X∧a∈Y∧d∈Y→a=d∨⋃c∈Z∖a⟨“aBc”⟩∩⋃c∈Z∖d⟨“dBc”⟩=∅
3 eliun ⊢s∈⋃c∈Z∖a⟨“aBc”⟩↔∃c∈Z∖as∈⟨“aBc”⟩
4 velsn ⊢s∈⟨“aBc”⟩↔s=⟨“aBc”⟩
5 eqeq1 ⊢s=⟨“aBc”⟩→s=⟨“dBe”⟩↔⟨“aBc”⟩=⟨“dBe”⟩
6 5 adantl ⊢B∈X∧a∈Y∧d∈Y∧c∈Z∖a∧e∈Z∖d∧s=⟨“aBc”⟩→s=⟨“dBe”⟩↔⟨“aBc”⟩=⟨“dBe”⟩
7 s3cli ⊢⟨“aBc”⟩∈WordV
8 elex ⊢B∈X→B∈V
9 elex ⊢d∈Y→d∈V
10 9 adantl ⊢a∈Y∧d∈Y→d∈V
11 8 10 anim12ci ⊢B∈X∧a∈Y∧d∈Y→d∈V∧B∈V
12 elex ⊢e∈Z∖d→e∈V
13 12 adantl ⊢c∈Z∖a∧e∈Z∖d→e∈V
14 11 13 anim12i ⊢B∈X∧a∈Y∧d∈Y∧c∈Z∖a∧e∈Z∖d→d∈V∧B∈V∧e∈V
15 df-3an ⊢d∈V∧B∈V∧e∈V↔d∈V∧B∈V∧e∈V
16 14 15 sylibr ⊢B∈X∧a∈Y∧d∈Y∧c∈Z∖a∧e∈Z∖d→d∈V∧B∈V∧e∈V
17 eqwrds3 ⊢⟨“aBc”⟩∈WordV∧d∈V∧B∈V∧e∈V→⟨“aBc”⟩=⟨“dBe”⟩↔⟨“aBc”⟩=3∧⟨“aBc”⟩⁡0=d∧⟨“aBc”⟩⁡1=B∧⟨“aBc”⟩⁡2=e
18 7 16 17 sylancr ⊢B∈X∧a∈Y∧d∈Y∧c∈Z∖a∧e∈Z∖d→⟨“aBc”⟩=⟨“dBe”⟩↔⟨“aBc”⟩=3∧⟨“aBc”⟩⁡0=d∧⟨“aBc”⟩⁡1=B∧⟨“aBc”⟩⁡2=e
19 s3fv0 ⊢a∈V→⟨“aBc”⟩⁡0=a
20 19 elv ⊢⟨“aBc”⟩⁡0=a
21 simp1 ⊢⟨“aBc”⟩⁡0=d∧⟨“aBc”⟩⁡1=B∧⟨“aBc”⟩⁡2=e→⟨“aBc”⟩⁡0=d
22 20 21 eqtr3id ⊢⟨“aBc”⟩⁡0=d∧⟨“aBc”⟩⁡1=B∧⟨“aBc”⟩⁡2=e→a=d
23 22 adantl ⊢⟨“aBc”⟩=3∧⟨“aBc”⟩⁡0=d∧⟨“aBc”⟩⁡1=B∧⟨“aBc”⟩⁡2=e→a=d
24 18 23 syl6bi ⊢B∈X∧a∈Y∧d∈Y∧c∈Z∖a∧e∈Z∖d→⟨“aBc”⟩=⟨“dBe”⟩→a=d
25 24 adantr ⊢B∈X∧a∈Y∧d∈Y∧c∈Z∖a∧e∈Z∖d∧s=⟨“aBc”⟩→⟨“aBc”⟩=⟨“dBe”⟩→a=d
26 6 25 sylbid ⊢B∈X∧a∈Y∧d∈Y∧c∈Z∖a∧e∈Z∖d∧s=⟨“aBc”⟩→s=⟨“dBe”⟩→a=d
27 26 ancoms ⊢s=⟨“aBc”⟩∧B∈X∧a∈Y∧d∈Y∧c∈Z∖a∧e∈Z∖d→s=⟨“dBe”⟩→a=d
28 27 con3d ⊢s=⟨“aBc”⟩∧B∈X∧a∈Y∧d∈Y∧c∈Z∖a∧e∈Z∖d→¬a=d→¬s=⟨“dBe”⟩
29 28 exp32 ⊢s=⟨“aBc”⟩→B∈X∧a∈Y∧d∈Y→c∈Z∖a∧e∈Z∖d→¬a=d→¬s=⟨“dBe”⟩
30 29 com14 ⊢¬a=d→B∈X∧a∈Y∧d∈Y→c∈Z∖a∧e∈Z∖d→s=⟨“aBc”⟩→¬s=⟨“dBe”⟩
31 30 imp ⊢¬a=d∧B∈X∧a∈Y∧d∈Y→c∈Z∖a∧e∈Z∖d→s=⟨“aBc”⟩→¬s=⟨“dBe”⟩
32 31 expd ⊢¬a=d∧B∈X∧a∈Y∧d∈Y→c∈Z∖a→e∈Z∖d→s=⟨“aBc”⟩→¬s=⟨“dBe”⟩
33 32 com34 ⊢¬a=d∧B∈X∧a∈Y∧d∈Y→c∈Z∖a→s=⟨“aBc”⟩→e∈Z∖d→¬s=⟨“dBe”⟩
34 33 imp ⊢¬a=d∧B∈X∧a∈Y∧d∈Y∧c∈Z∖a→s=⟨“aBc”⟩→e∈Z∖d→¬s=⟨“dBe”⟩
35 4 34 biimtrid ⊢¬a=d∧B∈X∧a∈Y∧d∈Y∧c∈Z∖a→s∈⟨“aBc”⟩→e∈Z∖d→¬s=⟨“dBe”⟩
36 35 imp ⊢¬a=d∧B∈X∧a∈Y∧d∈Y∧c∈Z∖a∧s∈⟨“aBc”⟩→e∈Z∖d→¬s=⟨“dBe”⟩
37 36 imp ⊢¬a=d∧B∈X∧a∈Y∧d∈Y∧c∈Z∖a∧s∈⟨“aBc”⟩∧e∈Z∖d→¬s=⟨“dBe”⟩
38 velsn ⊢s∈⟨“dBe”⟩↔s=⟨“dBe”⟩
39 37 38 sylnibr ⊢¬a=d∧B∈X∧a∈Y∧d∈Y∧c∈Z∖a∧s∈⟨“aBc”⟩∧e∈Z∖d→¬s∈⟨“dBe”⟩
40 39 nrexdv ⊢¬a=d∧B∈X∧a∈Y∧d∈Y∧c∈Z∖a∧s∈⟨“aBc”⟩→¬∃e∈Z∖ds∈⟨“dBe”⟩
41 eliun ⊢s∈⋃e∈Z∖d⟨“dBe”⟩↔∃e∈Z∖ds∈⟨“dBe”⟩
42 40 41 sylnibr ⊢¬a=d∧B∈X∧a∈Y∧d∈Y∧c∈Z∖a∧s∈⟨“aBc”⟩→¬s∈⋃e∈Z∖d⟨“dBe”⟩
43 42 rexlimdva2 ⊢¬a=d∧B∈X∧a∈Y∧d∈Y→∃c∈Z∖as∈⟨“aBc”⟩→¬s∈⋃e∈Z∖d⟨“dBe”⟩
44 3 43 biimtrid ⊢¬a=d∧B∈X∧a∈Y∧d∈Y→s∈⋃c∈Z∖a⟨“aBc”⟩→¬s∈⋃e∈Z∖d⟨“dBe”⟩
45 44 ralrimiv ⊢¬a=d∧B∈X∧a∈Y∧d∈Y→∀s∈⋃c∈Z∖a⟨“aBc”⟩¬s∈⋃e∈Z∖d⟨“dBe”⟩
46 eqidd ⊢c=e→d=d
47 eqidd ⊢c=e→B=B
48 id ⊢c=e→c=e
49 46 47 48 s3eqd ⊢c=e→⟨“dBc”⟩=⟨“dBe”⟩
50 49 sneqd ⊢c=e→⟨“dBc”⟩=⟨“dBe”⟩
51 50 cbviunv ⊢⋃c∈Z∖d⟨“dBc”⟩=⋃e∈Z∖d⟨“dBe”⟩
52 51 eleq2i ⊢s∈⋃c∈Z∖d⟨“dBc”⟩↔s∈⋃e∈Z∖d⟨“dBe”⟩
53 52 notbii ⊢¬s∈⋃c∈Z∖d⟨“dBc”⟩↔¬s∈⋃e∈Z∖d⟨“dBe”⟩
54 53 ralbii ⊢∀s∈⋃c∈Z∖a⟨“aBc”⟩¬s∈⋃c∈Z∖d⟨“dBc”⟩↔∀s∈⋃c∈Z∖a⟨“aBc”⟩¬s∈⋃e∈Z∖d⟨“dBe”⟩
55 45 54 sylibr ⊢¬a=d∧B∈X∧a∈Y∧d∈Y→∀s∈⋃c∈Z∖a⟨“aBc”⟩¬s∈⋃c∈Z∖d⟨“dBc”⟩
56 disj ⊢⋃c∈Z∖a⟨“aBc”⟩∩⋃c∈Z∖d⟨“dBc”⟩=∅↔∀s∈⋃c∈Z∖a⟨“aBc”⟩¬s∈⋃c∈Z∖d⟨“dBc”⟩
57 55 56 sylibr ⊢¬a=d∧B∈X∧a∈Y∧d∈Y→⋃c∈Z∖a⟨“aBc”⟩∩⋃c∈Z∖d⟨“dBc”⟩=∅
58 57 olcd ⊢¬a=d∧B∈X∧a∈Y∧d∈Y→a=d∨⋃c∈Z∖a⟨“aBc”⟩∩⋃c∈Z∖d⟨“dBc”⟩=∅
59 58 ex ⊢¬a=d→B∈X∧a∈Y∧d∈Y→a=d∨⋃c∈Z∖a⟨“aBc”⟩∩⋃c∈Z∖d⟨“dBc”⟩=∅
60 2 59 pm2.61i ⊢B∈X∧a∈Y∧d∈Y→a=d∨⋃c∈Z∖a⟨“aBc”⟩∩⋃c∈Z∖d⟨“dBc”⟩=∅
61 60 ralrimivva ⊢B∈X→∀a∈Y∀d∈Ya=d∨⋃c∈Z∖a⟨“aBc”⟩∩⋃c∈Z∖d⟨“dBc”⟩=∅
62 sneq ⊢a=d→a=d
63 62 difeq2d ⊢a=d→Z∖a=Z∖d
64 id ⊢a=d→a=d
65 eqidd ⊢a=d→B=B
66 eqidd ⊢a=d→c=c
67 64 65 66 s3eqd ⊢a=d→⟨“aBc”⟩=⟨“dBc”⟩
68 67 sneqd ⊢a=d→⟨“aBc”⟩=⟨“dBc”⟩
69 63 68 disjiunb ⊢Disja∈Y⋃c∈Z∖a⟨“aBc”⟩↔∀a∈Y∀d∈Ya=d∨⋃c∈Z∖a⟨“aBc”⟩∩⋃c∈Z∖d⟨“dBc”⟩=∅
70 61 69 sylibr ⊢B∈X→Disja∈Y⋃c∈Z∖a⟨“aBc”⟩