Metamath Proof Explorer

Theorem wrddin

Description: A word in two alphabets is also a word under their intersection. (Contributed by Ender Ting, 24-Jul-2026)

Ref Expression
Assertion wrddin ⊢ A ∈ Word B ∧ A ∈ Word C → A ∈ Word B ∩ C

Proof

Step Hyp Ref Expression
1 wrdf ⊢ A ∈ Word B → A : 0 ..^ A ⟶ B
2 wrdf ⊢ A ∈ Word C → A : 0 ..^ A ⟶ C
3 1 2 anim12i ⊢ A ∈ Word B ∧ A ∈ Word C → A : 0 ..^ A ⟶ B ∧ A : 0 ..^ A ⟶ C
4 fin ⊢ A : 0 ..^ A ⟶ B ∩ C ↔ A : 0 ..^ A ⟶ B ∧ A : 0 ..^ A ⟶ C
5 3 4 sylibr ⊢ A ∈ Word B ∧ A ∈ Word C → A : 0 ..^ A ⟶ B ∩ C
6 iswrdb ⊢ A ∈ Word B ∩ C ↔ A : 0 ..^ A ⟶ B ∩ C
7 5 6 sylibr ⊢ A ∈ Word B ∧ A ∈ Word C → A ∈ Word B ∩ C