Metamath Proof Explorer

Theorem pfx00

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

Ref Expression
Assertion pfx00 ${⊢}{S}\mathrm{prefix}0=\varnothing$

Proof

Step Hyp Ref Expression
1 opelxp ${⊢}⟨{S},0⟩\in \left(\mathrm{V}×{ℕ}_{0}\right)↔\left({S}\in \mathrm{V}\wedge 0\in {ℕ}_{0}\right)$
2 pfxval ${⊢}\left({S}\in \mathrm{V}\wedge 0\in {ℕ}_{0}\right)\to {S}\mathrm{prefix}0={S}\mathrm{substr}⟨0,0⟩$
3 swrd00 ${⊢}{S}\mathrm{substr}⟨0,0⟩=\varnothing$
4 2 3 syl6eq ${⊢}\left({S}\in \mathrm{V}\wedge 0\in {ℕ}_{0}\right)\to {S}\mathrm{prefix}0=\varnothing$
5 1 4 sylbi ${⊢}⟨{S},0⟩\in \left(\mathrm{V}×{ℕ}_{0}\right)\to {S}\mathrm{prefix}0=\varnothing$
6 df-pfx ${⊢}\mathrm{prefix}=\left({s}\in \mathrm{V},{l}\in {ℕ}_{0}⟼{s}\mathrm{substr}⟨0,{l}⟩\right)$
7 ovex ${⊢}{s}\mathrm{substr}⟨0,{l}⟩\in \mathrm{V}$
8 6 7 dmmpo ${⊢}\mathrm{dom}\mathrm{prefix}=\mathrm{V}×{ℕ}_{0}$
9 5 8 eleq2s ${⊢}⟨{S},0⟩\in \mathrm{dom}\mathrm{prefix}\to {S}\mathrm{prefix}0=\varnothing$
10 df-ov ${⊢}{S}\mathrm{prefix}0=\mathrm{prefix}\left(⟨{S},0⟩\right)$
11 ndmfv ${⊢}¬⟨{S},0⟩\in \mathrm{dom}\mathrm{prefix}\to \mathrm{prefix}\left(⟨{S},0⟩\right)=\varnothing$
12 10 11 syl5eq ${⊢}¬⟨{S},0⟩\in \mathrm{dom}\mathrm{prefix}\to {S}\mathrm{prefix}0=\varnothing$
13 9 12 pm2.61i ${⊢}{S}\mathrm{prefix}0=\varnothing$