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 L S substr F L =

Proof

Step Hyp Ref Expression
1 opelxp F L × F L
2 1 biimpi F L × F L
3 2 adantl S V F L × F L
4 df-substr substr = s V , b × if 1 st b ..^ 2 nd b dom s x 0 ..^ 2 nd b 1 st b s x + 1 st b
5 4 mpondm0 ¬ S V F L × S substr F L =
6 3 5 nsyl5 ¬ F L S substr F L =