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	⊢ ( ¬ ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		opelxp	⊢ ( ⟨ 𝐹 , 𝐿 ⟩ ∈ ( ℤ × ℤ ) ↔ ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) )
2	1	biimpi	⊢ ( ⟨ 𝐹 , 𝐿 ⟩ ∈ ( ℤ × ℤ ) → ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) )
3	2	adantl	⊢ ( ( 𝑆 ∈ V ∧ ⟨ 𝐹 , 𝐿 ⟩ ∈ ( ℤ × ℤ ) ) → ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) )
4		df-substr	⊢ substr = ( 𝑠 ∈ V , 𝑏 ∈ ( ℤ × ℤ ) ↦ if ( ( ( 1^st ‘ 𝑏 ) ..^ ( 2^nd ‘ 𝑏 ) ) ⊆ dom 𝑠 , ( 𝑥 ∈ ( 0 ..^ ( ( 2^nd ‘ 𝑏 ) − ( 1^st ‘ 𝑏 ) ) ) ↦ ( 𝑠 ‘ ( 𝑥 + ( 1^st ‘ 𝑏 ) ) ) ) , ∅ ) )
5	4	mpondm0	⊢ ( ¬ ( 𝑆 ∈ V ∧ ⟨ 𝐹 , 𝐿 ⟩ ∈ ( ℤ × ℤ ) ) → ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) = ∅ )
6	3 5	nsyl5	⊢ ( ¬ ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) = ∅ )

Metamath Proof Explorer

Theorem swrdnznd

Proof