Metamath Proof Explorer

Theorem swrdnznd

Description: The value of a subword operation for noninteger arguments is the empty set. (This is due to our definition of function values for out-of-domain arguments, see ndmfv ). (Contributed by AV, 2-Dec-2022) (New usage is discouraged.)

Ref Expression
Assertion swrdnznd 
|- ( -. ( F e. ZZ /\ L e. ZZ ) -> ( S substr <. F , L >. ) = (/) )

Proof

Step Hyp Ref Expression
1 opelxp 
 |-  ( <. F , L >. e. ( ZZ X. ZZ ) <-> ( F e. ZZ /\ L e. ZZ ) )
2 1 biimpi 
 |-  ( <. F , L >. e. ( ZZ X. ZZ ) -> ( F e. ZZ /\ L e. ZZ ) )
3 2 adantl 
 |-  ( ( S e. _V /\ <. F , L >. e. ( ZZ X. ZZ ) ) -> ( F e. ZZ /\ L e. ZZ ) )
4 df-substr 
 |-  substr = ( s e. _V , b e. ( ZZ X. ZZ ) |-> if ( ( ( 1st ` b ) ..^ ( 2nd ` b ) ) C_ dom s , ( x e. ( 0 ..^ ( ( 2nd ` b ) - ( 1st ` b ) ) ) |-> ( s ` ( x + ( 1st ` b ) ) ) ) , (/) ) )
5 4 mpondm0 
 |-  ( -. ( S e. _V /\ <. F , L >. e. ( ZZ X. ZZ ) ) -> ( S substr <. F , L >. ) = (/) )
6 3 5 nsyl5 
 |-  ( -. ( F e. ZZ /\ L e. ZZ ) -> ( S substr <. F , L >. ) = (/) )