Theorem pfx0

Description: A prefix of an empty set is always the empty set. (Contributed by AV, 3-May-2020)

	Ref	Expression
Assertion	pfx0	⊢ ( ∅ prefix 𝐿 ) = ∅

Proof

Step	Hyp	Ref	Expression
1		opelxp	⊢ ( ⟨ ∅ , 𝐿 ⟩ ∈ ( V × ℕ0 ) ↔ ( ∅ ∈ V ∧ 𝐿 ∈ ℕ0 ) )
2		pfxval	⊢ ( ( ∅ ∈ V ∧ 𝐿 ∈ ℕ0 ) → ( ∅ prefix 𝐿 ) = ( ∅ substr ⟨ 0 , 𝐿 ⟩ ) )
3		swrd0	⊢ ( ∅ substr ⟨ 0 , 𝐿 ⟩ ) = ∅
4	2 3	eqtrdi	⊢ ( ( ∅ ∈ V ∧ 𝐿 ∈ ℕ0 ) → ( ∅ prefix 𝐿 ) = ∅ )
5	1 4	sylbi	⊢ ( ⟨ ∅ , 𝐿 ⟩ ∈ ( V × ℕ0 ) → ( ∅ prefix 𝐿 ) = ∅ )
6		df-pfx	⊢ prefix = ( 𝑠 ∈ V , 𝑙 ∈ ℕ0 ↦ ( 𝑠 substr ⟨ 0 , 𝑙 ⟩ ) )
7		ovex	⊢ ( 𝑠 substr ⟨ 0 , 𝑙 ⟩ ) ∈ V
8	6 7	dmmpo	⊢ dom prefix = ( V × ℕ0 )
9	5 8	eleq2s	⊢ ( ⟨ ∅ , 𝐿 ⟩ ∈ dom prefix → ( ∅ prefix 𝐿 ) = ∅ )
10		df-ov	⊢ ( ∅ prefix 𝐿 ) = ( prefix ‘ ⟨ ∅ , 𝐿 ⟩ )
11		ndmfv	⊢ ( ¬ ⟨ ∅ , 𝐿 ⟩ ∈ dom prefix → ( prefix ‘ ⟨ ∅ , 𝐿 ⟩ ) = ∅ )
12	10 11	syl5eq	⊢ ( ¬ ⟨ ∅ , 𝐿 ⟩ ∈ dom prefix → ( ∅ prefix 𝐿 ) = ∅ )
13	9 12	pm2.61i	⊢ ( ∅ prefix 𝐿 ) = ∅