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

Metamath Proof Explorer

Theorem 1wlkdlem3

Description: Lemma 3 for 1wlkd . (Contributed by AV, 22-Jan-2021)

Ref Expression
Hypotheses 1wlkd.p ⊢ P = ⟨“ XY ”⟩
1wlkd.f ⊢ F = ⟨“ J ”⟩
1wlkd.x ⊢ φ → X ∈ V
1wlkd.y ⊢ φ → Y ∈ V
1wlkd.l ⊢ φ ∧ X = Y → I ⁡ J = X
1wlkd.j ⊢ φ ∧ X ≠ Y → X Y ⊆ I ⁡ J
Assertion 1wlkdlem3 ⊢ φ → F ∈ Word dom ⁡ I

Proof

Step Hyp Ref Expression
1 1wlkd.p ⊢ P = ⟨“ XY ”⟩
2 1wlkd.f ⊢ F = ⟨“ J ”⟩
3 1wlkd.x ⊢ φ → X ∈ V
4 1wlkd.y ⊢ φ → Y ∈ V
5 1wlkd.l ⊢ φ ∧ X = Y → I ⁡ J = X
6 1wlkd.j ⊢ φ ∧ X ≠ Y → X Y ⊆ I ⁡ J
7 1 2 3 4 5 6 1wlkdlem2 ⊢ φ → X ∈ I ⁡ J
8 elfvdm ⊢ X ∈ I ⁡ J → J ∈ dom ⁡ I
9 s1cl ⊢ J ∈ dom ⁡ I → ⟨“ J ”⟩ ∈ Word dom ⁡ I
10 2 9 eqeltrid ⊢ J ∈ dom ⁡ I → F ∈ Word dom ⁡ I
11 7 8 10 3syl ⊢ φ → F ∈ Word dom ⁡ I