This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 biimtrdi ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ∧ ( 𝑐 ∈ 𝑍 ∧ 𝑑 ∈ 𝑍 ) ) → ( ⟨“ 𝐴 𝐵 𝑐 ”⟩ = ⟨“ 𝐴 𝐵 𝑑 ”⟩ → 𝑐 = 𝑑 ) )
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 𝑐 ∈ 𝑍 { ⟨“ 𝐴 𝐵 𝑐 ”⟩ } )