Theorem 1wlkdlem3

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

	Ref	Expression
Hypotheses	1wlkd.p	⊢ 𝑃 = ⟨“ 𝑋 𝑌 ”⟩
	1wlkd.f	⊢ 𝐹 = ⟨“ 𝐽 ”⟩
	1wlkd.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
	1wlkd.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
	1wlkd.l	⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → ( 𝐼 ‘ 𝐽 ) = { 𝑋 } )
	1wlkd.j	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → { 𝑋 , 𝑌 } ⊆ ( 𝐼 ‘ 𝐽 ) )
Assertion	1wlkdlem3	⊢ ( 𝜑 → 𝐹 ∈ Word dom 𝐼 )

Proof

Step	Hyp	Ref	Expression
1		1wlkd.p	⊢ 𝑃 = ⟨“ 𝑋 𝑌 ”⟩
2		1wlkd.f	⊢ 𝐹 = ⟨“ 𝐽 ”⟩
3		1wlkd.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
4		1wlkd.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
5		1wlkd.l	⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → ( 𝐼 ‘ 𝐽 ) = { 𝑋 } )
6		1wlkd.j	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → { 𝑋 , 𝑌 } ⊆ ( 𝐼 ‘ 𝐽 ) )
7	1 2 3 4 5 6	1wlkdlem2	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐼 ‘ 𝐽 ) )
8		elfvdm	⊢ ( 𝑋 ∈ ( 𝐼 ‘ 𝐽 ) → 𝐽 ∈ dom 𝐼 )
9		s1cl	⊢ ( 𝐽 ∈ dom 𝐼 → ⟨“ 𝐽 ”⟩ ∈ Word dom 𝐼 )
10	2 9	eqeltrid	⊢ ( 𝐽 ∈ dom 𝐼 → 𝐹 ∈ Word dom 𝐼 )
11	7 8 10	3syl	⊢ ( 𝜑 → 𝐹 ∈ Word dom 𝐼 )