Metamath Proof Explorer

Theorem chndin

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

Ref Expression
Assertion chndin 
|- ( ( A e. ( R Chain B ) /\ A e. ( R Chain C ) ) -> A e. ( R Chain ( B i^i C ) ) )

Proof

Step Hyp Ref Expression
1 id 
 |-  ( A e. ( R Chain B ) -> A e. ( R Chain B ) )
2 1 chnwrd 
 |-  ( A e. ( R Chain B ) -> A e. Word B )
3 id 
 |-  ( A e. ( R Chain C ) -> A e. ( R Chain C ) )
4 3 chnwrd 
 |-  ( A e. ( R Chain C ) -> A e. Word C )
5 wrddin 
 |-  ( ( A e. Word B /\ A e. Word C ) -> A e. Word ( B i^i C ) )
6 2 4 5 syl2an 
 |-  ( ( A e. ( R Chain B ) /\ A e. ( R Chain C ) ) -> A e. Word ( B i^i C ) )
7 ischn 
 |-  ( A e. ( R Chain B ) <-> ( A e. Word B /\ A. n e. ( dom A \ { 0 } ) ( A ` ( n - 1 ) ) R ( A ` n ) ) )
8 7 simprbi 
 |-  ( A e. ( R Chain B ) -> A. n e. ( dom A \ { 0 } ) ( A ` ( n - 1 ) ) R ( A ` n ) )
9 8 adantr 
 |-  ( ( A e. ( R Chain B ) /\ A e. ( R Chain C ) ) -> A. n e. ( dom A \ { 0 } ) ( A ` ( n - 1 ) ) R ( A ` n ) )
10 ischn 
 |-  ( A e. ( R Chain ( B i^i C ) ) <-> ( A e. Word ( B i^i C ) /\ A. n e. ( dom A \ { 0 } ) ( A ` ( n - 1 ) ) R ( A ` n ) ) )
11 6 9 10 sylanbrc 
 |-  ( ( A e. ( R Chain B ) /\ A e. ( R Chain C ) ) -> A e. ( R Chain ( B i^i C ) ) )