Database
REAL AND COMPLEX NUMBERS
Words over a set
Prefixes of a word
pfx0
Next ⟩
pfxval0
Metamath Proof Explorer
Ascii
Unicode
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
=
∅