Metamath Proof Explorer


Theorem wlk2v2elem1

Description: Lemma 1 for wlk2v2e : F is a length 2 word of over { 0 } , the domain of the singleton word I . (Contributed by Alexander van der Vekens, 22-Oct-2017) (Revised by AV, 9-Jan-2021)

Ref Expression
Hypotheses wlk2v2e.i I=⟨“XY”⟩
wlk2v2e.f F=⟨“00”⟩
Assertion wlk2v2elem1 FWorddomI

Proof

Step Hyp Ref Expression
1 wlk2v2e.i I=⟨“XY”⟩
2 wlk2v2e.f F=⟨“00”⟩
3 c0ex 0V
4 3 snid 00
5 id 0000
6 5 5 s2cld 00⟨“00”⟩Word0
7 4 6 ax-mp ⟨“00”⟩Word0
8 1 dmeqi domI=dom⟨“XY”⟩
9 s1dm dom⟨“XY”⟩=0
10 8 9 eqtri domI=0
11 10 wrdeqi WorddomI=Word0
12 7 2 11 3eltr4i FWorddomI