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

Proof

Step Hyp Ref Expression
1 opelxp ⊢ ∅ L ∈ V × ℕ 0 ↔ ∅ ∈ V ∧ L ∈ ℕ 0
2 pfxval ⊢ ∅ ∈ V ∧ L ∈ ℕ 0 → ∅ prefix L = ∅ substr 0 L
3 swrd0 ⊢ ∅ substr 0 L = ∅
4 2 3 eqtrdi ⊢ ∅ ∈ V ∧ L ∈ ℕ 0 → ∅ prefix L = ∅
5 1 4 sylbi ⊢ ∅ L ∈ V × ℕ 0 → ∅ prefix L = ∅
6 df-pfx ⊢ prefix = s ∈ V , l ∈ ℕ 0 ⟼ s substr 0 l
7 ovex ⊢ s substr 0 l ∈ V
8 6 7 dmmpo ⊢ dom ⁡ prefix = V × ℕ 0
9 5 8 eleq2s ⊢ ∅ L ∈ dom ⁡ prefix → ∅ prefix L = ∅
10 df-ov ⊢ ∅ prefix L = prefix ⁡ ∅ L
11 ndmfv ⊢ ¬ ∅ L ∈ dom ⁡ prefix → prefix ⁡ ∅ L = ∅
12 10 11 syl5eq ⊢ ¬ ∅ L ∈ dom ⁡ prefix → ∅ prefix L = ∅
13 9 12 pm2.61i ⊢ ∅ prefix L = ∅