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 ( ( 𝐴𝑋𝐵𝑌 ) → Disj 𝑐𝑍 { ⟨“ 𝐴 𝐵 𝑐 ”⟩ } )

Proof

Step Hyp Ref Expression
1 orc ( 𝑐 = 𝑑 → ( 𝑐 = 𝑑 ∨ ( { ⟨“ 𝐴 𝐵 𝑐 ”⟩ } ∩ { ⟨“ 𝐴 𝐵 𝑑 ”⟩ } ) = ∅ ) )
2 1 a1d ( 𝑐 = 𝑑 → ( ( ( 𝐴𝑋𝐵𝑌 ) ∧ ( 𝑐𝑍𝑑𝑍 ) ) → ( 𝑐 = 𝑑 ∨ ( { ⟨“ 𝐴 𝐵 𝑐 ”⟩ } ∩ { ⟨“ 𝐴 𝐵 𝑑 ”⟩ } ) = ∅ ) ) )
3 s3cli ⟨“ 𝐴 𝐵 𝑐 ”⟩ ∈ Word V
4 elex ( 𝐴𝑋𝐴 ∈ V )
5 elex ( 𝐵𝑌𝐵 ∈ V )
6 4 5 anim12i ( ( 𝐴𝑋𝐵𝑌 ) → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
7 elex ( 𝑑𝑍𝑑 ∈ V )
8 7 adantl ( ( 𝑐𝑍𝑑𝑍 ) → 𝑑 ∈ V )
9 6 8 anim12i ( ( ( 𝐴𝑋𝐵𝑌 ) ∧ ( 𝑐𝑍𝑑𝑍 ) ) → ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝑑 ∈ V ) )
10 df-3an ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑑 ∈ V ) ↔ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝑑 ∈ V ) )
11 9 10 sylibr ( ( ( 𝐴𝑋𝐵𝑌 ) ∧ ( 𝑐𝑍𝑑𝑍 ) ) → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑑 ∈ V ) )
12 eqwrds3 ( ( ⟨“ 𝐴 𝐵 𝑐 ”⟩ ∈ Word V ∧ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑑 ∈ V ) ) → ( ⟨“ 𝐴 𝐵 𝑐 ”⟩ = ⟨“ 𝐴 𝐵 𝑑 ”⟩ ↔ ( ( ♯ ‘ ⟨“ 𝐴 𝐵 𝑐 ”⟩ ) = 3 ∧ ( ( ⟨“ 𝐴 𝐵 𝑐 ”⟩ ‘ 0 ) = 𝐴 ∧ ( ⟨“ 𝐴 𝐵 𝑐 ”⟩ ‘ 1 ) = 𝐵 ∧ ( ⟨“ 𝐴 𝐵 𝑐 ”⟩ ‘ 2 ) = 𝑑 ) ) ) )
13 3 11 12 sylancr ( ( ( 𝐴𝑋𝐵𝑌 ) ∧ ( 𝑐𝑍𝑑𝑍 ) ) → ( ⟨“ 𝐴 𝐵 𝑐 ”⟩ = ⟨“ 𝐴 𝐵 𝑑 ”⟩ ↔ ( ( ♯ ‘ ⟨“ 𝐴 𝐵 𝑐 ”⟩ ) = 3 ∧ ( ( ⟨“ 𝐴 𝐵 𝑐 ”⟩ ‘ 0 ) = 𝐴 ∧ ( ⟨“ 𝐴 𝐵 𝑐 ”⟩ ‘ 1 ) = 𝐵 ∧ ( ⟨“ 𝐴 𝐵 𝑐 ”⟩ ‘ 2 ) = 𝑑 ) ) ) )
14 s3fv2 ( 𝑐 ∈ V → ( ⟨“ 𝐴 𝐵 𝑐 ”⟩ ‘ 2 ) = 𝑐 )
15 14 elv ( ⟨“ 𝐴 𝐵 𝑐 ”⟩ ‘ 2 ) = 𝑐
16 simp3 ( ( ( ⟨“ 𝐴 𝐵 𝑐 ”⟩ ‘ 0 ) = 𝐴 ∧ ( ⟨“ 𝐴 𝐵 𝑐 ”⟩ ‘ 1 ) = 𝐵 ∧ ( ⟨“ 𝐴 𝐵 𝑐 ”⟩ ‘ 2 ) = 𝑑 ) → ( ⟨“ 𝐴 𝐵 𝑐 ”⟩ ‘ 2 ) = 𝑑 )
17 15 16 eqtr3id ( ( ( ⟨“ 𝐴 𝐵 𝑐 ”⟩ ‘ 0 ) = 𝐴 ∧ ( ⟨“ 𝐴 𝐵 𝑐 ”⟩ ‘ 1 ) = 𝐵 ∧ ( ⟨“ 𝐴 𝐵 𝑐 ”⟩ ‘ 2 ) = 𝑑 ) → 𝑐 = 𝑑 )
18 17 adantl ( ( ( ♯ ‘ ⟨“ 𝐴 𝐵 𝑐 ”⟩ ) = 3 ∧ ( ( ⟨“ 𝐴 𝐵 𝑐 ”⟩ ‘ 0 ) = 𝐴 ∧ ( ⟨“ 𝐴 𝐵 𝑐 ”⟩ ‘ 1 ) = 𝐵 ∧ ( ⟨“ 𝐴 𝐵 𝑐 ”⟩ ‘ 2 ) = 𝑑 ) ) → 𝑐 = 𝑑 )
19 13 18 syl6bi ( ( ( 𝐴𝑋𝐵𝑌 ) ∧ ( 𝑐𝑍𝑑𝑍 ) ) → ( ⟨“ 𝐴 𝐵 𝑐 ”⟩ = ⟨“ 𝐴 𝐵 𝑑 ”⟩ → 𝑐 = 𝑑 ) )
20 19 con3rr3 ( ¬ 𝑐 = 𝑑 → ( ( ( 𝐴𝑋𝐵𝑌 ) ∧ ( 𝑐𝑍𝑑𝑍 ) ) → ¬ ⟨“ 𝐴 𝐵 𝑐 ”⟩ = ⟨“ 𝐴 𝐵 𝑑 ”⟩ ) )
21 20 imp ( ( ¬ 𝑐 = 𝑑 ∧ ( ( 𝐴𝑋𝐵𝑌 ) ∧ ( 𝑐𝑍𝑑𝑍 ) ) ) → ¬ ⟨“ 𝐴 𝐵 𝑐 ”⟩ = ⟨“ 𝐴 𝐵 𝑑 ”⟩ )
22 21 neqned ( ( ¬ 𝑐 = 𝑑 ∧ ( ( 𝐴𝑋𝐵𝑌 ) ∧ ( 𝑐𝑍𝑑𝑍 ) ) ) → ⟨“ 𝐴 𝐵 𝑐 ”⟩ ≠ ⟨“ 𝐴 𝐵 𝑑 ”⟩ )
23 disjsn2 ( ⟨“ 𝐴 𝐵 𝑐 ”⟩ ≠ ⟨“ 𝐴 𝐵 𝑑 ”⟩ → ( { ⟨“ 𝐴 𝐵 𝑐 ”⟩ } ∩ { ⟨“ 𝐴 𝐵 𝑑 ”⟩ } ) = ∅ )
24 22 23 syl ( ( ¬ 𝑐 = 𝑑 ∧ ( ( 𝐴𝑋𝐵𝑌 ) ∧ ( 𝑐𝑍𝑑𝑍 ) ) ) → ( { ⟨“ 𝐴 𝐵 𝑐 ”⟩ } ∩ { ⟨“ 𝐴 𝐵 𝑑 ”⟩ } ) = ∅ )
25 24 olcd ( ( ¬ 𝑐 = 𝑑 ∧ ( ( 𝐴𝑋𝐵𝑌 ) ∧ ( 𝑐𝑍𝑑𝑍 ) ) ) → ( 𝑐 = 𝑑 ∨ ( { ⟨“ 𝐴 𝐵 𝑐 ”⟩ } ∩ { ⟨“ 𝐴 𝐵 𝑑 ”⟩ } ) = ∅ ) )
26 25 ex ( ¬ 𝑐 = 𝑑 → ( ( ( 𝐴𝑋𝐵𝑌 ) ∧ ( 𝑐𝑍𝑑𝑍 ) ) → ( 𝑐 = 𝑑 ∨ ( { ⟨“ 𝐴 𝐵 𝑐 ”⟩ } ∩ { ⟨“ 𝐴 𝐵 𝑑 ”⟩ } ) = ∅ ) ) )
27 2 26 pm2.61i ( ( ( 𝐴𝑋𝐵𝑌 ) ∧ ( 𝑐𝑍𝑑𝑍 ) ) → ( 𝑐 = 𝑑 ∨ ( { ⟨“ 𝐴 𝐵 𝑐 ”⟩ } ∩ { ⟨“ 𝐴 𝐵 𝑑 ”⟩ } ) = ∅ ) )
28 27 ralrimivva ( ( 𝐴𝑋𝐵𝑌 ) → ∀ 𝑐𝑍𝑑𝑍 ( 𝑐 = 𝑑 ∨ ( { ⟨“ 𝐴 𝐵 𝑐 ”⟩ } ∩ { ⟨“ 𝐴 𝐵 𝑑 ”⟩ } ) = ∅ ) )
29 eqidd ( 𝑐 = 𝑑𝐴 = 𝐴 )
30 eqidd ( 𝑐 = 𝑑𝐵 = 𝐵 )
31 id ( 𝑐 = 𝑑𝑐 = 𝑑 )
32 29 30 31 s3eqd ( 𝑐 = 𝑑 → ⟨“ 𝐴 𝐵 𝑐 ”⟩ = ⟨“ 𝐴 𝐵 𝑑 ”⟩ )
33 32 sneqd ( 𝑐 = 𝑑 → { ⟨“ 𝐴 𝐵 𝑐 ”⟩ } = { ⟨“ 𝐴 𝐵 𝑑 ”⟩ } )
34 33 disjor ( Disj 𝑐𝑍 { ⟨“ 𝐴 𝐵 𝑐 ”⟩ } ↔ ∀ 𝑐𝑍𝑑𝑍 ( 𝑐 = 𝑑 ∨ ( { ⟨“ 𝐴 𝐵 𝑐 ”⟩ } ∩ { ⟨“ 𝐴 𝐵 𝑑 ”⟩ } ) = ∅ ) )
35 28 34 sylibr ( ( 𝐴𝑋𝐵𝑌 ) → Disj 𝑐𝑍 { ⟨“ 𝐴 𝐵 𝑐 ”⟩ } )