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

Metamath Proof Explorer

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 eqtrid ⊢ ( ¬ ⟨ ∅ , 𝐿 ⟩ ∈ dom prefix → ( ∅ prefix 𝐿 ) = ∅ )
13 9 12 pm2.61i ⊢ ( ∅ prefix 𝐿 ) = ∅