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 → Disj a ∈ 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 ∖ a s ∈ ⟨“ 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 ”⟩ ∈ Word V
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 ”⟩ ∈ Word V ∧ 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 syl5bi ⊢ ¬ 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 ∖ d s ∈ ⟨“ dBe ”⟩
41 eliun ⊢ s ∈ ⋃ e ∈ Z ∖ d ⟨“ dBe ”⟩ ↔ ∃ e ∈ Z ∖ d s ∈ ⟨“ 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 ∖ a s ∈ ⟨“ aBc ”⟩ → ¬ s ∈ ⋃ e ∈ Z ∖ d ⟨“ dBe ”⟩
44 3 43 syl5bi ⊢ ¬ 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 ∈ Y a = 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 ⊢ Disj a ∈ Y ⋃ c ∈ Z ∖ a ⟨“ aBc ”⟩ ↔ ∀ a ∈ Y ∀ d ∈ Y a = d ∨ ⋃ c ∈ Z ∖ a ⟨“ aBc ”⟩ ∩ ⋃ c ∈ Z ∖ d ⟨“ dBc ”⟩ = ∅
70 61 69 sylibr ⊢ B ∈ X → Disj a ∈ Y ⋃ c ∈ Z ∖ a ⟨“ aBc ”⟩