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 e. Word B /\ A e. Word C ) -> A e. Word ( B i^i C ) )

Proof

Step Hyp Ref Expression
1 wrdf 
 |-  ( A e. Word B -> A : ( 0 ..^ ( # ` A ) ) --> B )
2 wrdf 
 |-  ( A e. Word C -> A : ( 0 ..^ ( # ` A ) ) --> C )
3 1 2 anim12i 
 |-  ( ( A e. Word B /\ A e. Word C ) -> ( A : ( 0 ..^ ( # ` A ) ) --> B /\ A : ( 0 ..^ ( # ` A ) ) --> C ) )
4 fin 
 |-  ( A : ( 0 ..^ ( # ` A ) ) --> ( B i^i C ) <-> ( A : ( 0 ..^ ( # ` A ) ) --> B /\ A : ( 0 ..^ ( # ` A ) ) --> C ) )
5 3 4 sylibr 
 |-  ( ( A e. Word B /\ A e. Word C ) -> A : ( 0 ..^ ( # ` A ) ) --> ( B i^i C ) )
6 iswrdb 
 |-  ( A e. Word ( B i^i C ) <-> A : ( 0 ..^ ( # ` A ) ) --> ( B i^i C ) )
7 5 6 sylibr 
 |-  ( ( A e. Word B /\ A e. Word C ) -> A e. Word ( B i^i C ) )