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	$⊢ \neg (F \in ℤ \land L \in ℤ) \to S substr ⟨F, L⟩ = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		opelxp	$⊢ ⟨F, L⟩ \in (ℤ \times ℤ) \leftrightarrow (F \in ℤ \land L \in ℤ)$
2	1	biimpi	$⊢ ⟨F, L⟩ \in (ℤ \times ℤ) \to (F \in ℤ \land L \in ℤ)$
3	2	adantl	$⊢ (S \in V \land ⟨F, L⟩ \in (ℤ \times ℤ)) \to (F \in ℤ \land L \in ℤ)$
4	3	con3i	$⊢ \neg (F \in ℤ \land L \in ℤ) \to \neg (S \in V \land ⟨F, L⟩ \in (ℤ \times ℤ))$
5		df-substr	$⊢ substr = (s \in V, b \in (ℤ \times ℤ) ⟼ if ((1^{st} (b) ..^2^{nd} (b)) \subseteq dom s, (x \in (0 ..^2^{nd} (b) - 1^{st} (b)) ⟼ s (x + 1^{st} (b))), \emptyset))$
6	5	mpondm0	$⊢ \neg (S \in V \land ⟨F, L⟩ \in (ℤ \times ℤ)) \to S substr ⟨F, L⟩ = \emptyset$
7	4 6	syl	$⊢ \neg (F \in ℤ \land L \in ℤ) \to S substr ⟨F, L⟩ = \emptyset$