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 biimtrdi ⊢ 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 ”⟩