Theorem pfx00

Description: The zero length prefix is the empty set. (Contributed by AV, 2-May-2020)

	Ref	Expression
Assertion	pfx00	⊢ ( 𝑆 prefix 0 ) = ∅

Proof

Step	Hyp	Ref	Expression
1		opelxp	⊢ ( ⟨ 𝑆 , 0 ⟩ ∈ ( V × ℕ0 ) ↔ ( 𝑆 ∈ V ∧ 0 ∈ ℕ0 ) )
2		pfxval	⊢ ( ( 𝑆 ∈ V ∧ 0 ∈ ℕ0 ) → ( 𝑆 prefix 0 ) = ( 𝑆 substr ⟨ 0 , 0 ⟩ ) )
3		swrd00	⊢ ( 𝑆 substr ⟨ 0 , 0 ⟩ ) = ∅
4	2 3	eqtrdi	⊢ ( ( 𝑆 ∈ V ∧ 0 ∈ ℕ0 ) → ( 𝑆 prefix 0 ) = ∅ )
5	1 4	sylbi	⊢ ( ⟨ 𝑆 , 0 ⟩ ∈ ( V × ℕ0 ) → ( 𝑆 prefix 0 ) = ∅ )
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	⊢ ( ⟨ 𝑆 , 0 ⟩ ∈ dom prefix → ( 𝑆 prefix 0 ) = ∅ )
10		df-ov	⊢ ( 𝑆 prefix 0 ) = ( prefix ‘ ⟨ 𝑆 , 0 ⟩ )
11		ndmfv	⊢ ( ¬ ⟨ 𝑆 , 0 ⟩ ∈ dom prefix → ( prefix ‘ ⟨ 𝑆 , 0 ⟩ ) = ∅ )
12	10 11	eqtrid	⊢ ( ¬ ⟨ 𝑆 , 0 ⟩ ∈ dom prefix → ( 𝑆 prefix 0 ) = ∅ )
13	9 12	pm2.61i	⊢ ( 𝑆 prefix 0 ) = ∅