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=⟨“\left\{X,Y\right\}”⟩$$
	wlk2v2e.f	$$⊢F=⟨“00”⟩$$
Assertion	wlk2v2elem1	$$⊢F\in \mathrm{Word}\mathrm{dom}I$$

Proof

Step	Hyp	Ref	Expression
1		wlk2v2e.i	$$⊢I=⟨“\left\{X,Y\right\}”⟩$$
2		wlk2v2e.f	$$⊢F=⟨“00”⟩$$
3		c0ex	$$⊢0\in \mathrm{V}$$
4	3	snid	$$⊢0\in \left\{0\right\}$$
5		id	$$⊢0\in \left\{0\right\}\to 0\in \left\{0\right\}$$
6	5 5	s2cld	$$⊢0\in \left\{0\right\}\to ⟨“00”⟩\in \mathrm{Word}\left\{0\right\}$$
7	4 6	ax-mp	$$⊢⟨“00”⟩\in \mathrm{Word}\left\{0\right\}$$
8	1	dmeqi	$$⊢\mathrm{dom}I=\mathrm{dom}⟨“\left\{X,Y\right\}”⟩$$
9		s1dm	$$⊢\mathrm{dom}⟨“\left\{X,Y\right\}”⟩=\left\{0\right\}$$
10	8 9	eqtri	$$⊢\mathrm{dom}I=\left\{0\right\}$$
11	10	wrdeqi	$$⊢\mathrm{Word}\mathrm{dom}I=\mathrm{Word}\left\{0\right\}$$
12	7 2 11	3eltr4i	$$⊢F\in \mathrm{Word}\mathrm{dom}I$$