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 prefix 0 =

Proof

Step Hyp Ref Expression
1 opelxp S 0 V × 0 S V 0 0
2 pfxval S V 0 0 S prefix 0 = S substr 0 0
3 swrd00 S substr 0 0 =
4 2 3 syl6eq S V 0 0 S prefix 0 =
5 1 4 sylbi S 0 V × 0 S prefix 0 =
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 S 0 dom prefix S prefix 0 =
10 df-ov S prefix 0 = prefix S 0
11 ndmfv ¬ S 0 dom prefix prefix S 0 =
12 10 11 syl5eq ¬ S 0 dom prefix S prefix 0 =
13 9 12 pm2.61i S prefix 0 =