This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) = ∅