This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = ⟨“ X Y ”⟩
wlk2v2e.f ⊢ F = ⟨“ 0 0 ”⟩
Assertion wlk2v2elem1 ⊢ F ∈ Word dom ⁡ I

Proof

Step Hyp Ref Expression
1 wlk2v2e.i ⊢ I = ⟨“ X Y ”⟩
2 wlk2v2e.f ⊢ 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 ⁡ I = dom ⁡ ⟨“ X Y ”⟩
9 s1dm ⊢ dom ⁡ ⟨“ X Y ”⟩ = 0
10 8 9 eqtri ⊢ dom ⁡ I = 0
11 10 wrdeqi ⊢ Word dom ⁡ I = Word 0
12 7 2 11 3eltr4i ⊢ F ∈ Word dom ⁡ I