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	⊢ 𝐼 = ⟨“ { 𝑋 , 𝑌 } ”⟩
	wlk2v2e.f	⊢ 𝐹 = ⟨“ 0 0 ”⟩
Assertion	wlk2v2elem1	⊢ 𝐹 ∈ Word dom 𝐼

Proof

Step	Hyp	Ref	Expression
1		wlk2v2e.i	⊢ 𝐼 = ⟨“ { 𝑋 , 𝑌 } ”⟩
2		wlk2v2e.f	⊢ 𝐹 = ⟨“ 0 0 ”⟩
3		c0ex	⊢ 0 ∈ V
4	3	snid	⊢ 0 ∈ { 0 }
5		id	⊢ ( 0 ∈ { 0 } → 0 ∈ { 0 } )
6	5 5	s2cld	⊢ ( 0 ∈ { 0 } → ⟨“ 0 0 ”⟩ ∈ Word { 0 } )
7	4 6	ax-mp	⊢ ⟨“ 0 0 ”⟩ ∈ Word { 0 }
8	1	dmeqi	⊢ dom 𝐼 = dom ⟨“ { 𝑋 , 𝑌 } ”⟩
9		s1dm	⊢ dom ⟨“ { 𝑋 , 𝑌 } ”⟩ = { 0 }
10	8 9	eqtri	⊢ dom 𝐼 = { 0 }
11	10	wrdeqi	⊢ Word dom 𝐼 = Word { 0 }
12	7 2 11	3eltr4i	⊢ 𝐹 ∈ Word dom 𝐼