Theorem 1wlkdlem3

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

	Ref	Expression
Hypotheses	1wlkd.p	|- P = <" X Y ">
	1wlkd.f	|- F = <" J ">
	1wlkd.x	|- ( ph -> X e. V )
	1wlkd.y	|- ( ph -> Y e. V )
	1wlkd.l	|- ( ( ph /\ X = Y ) -> ( I ` J ) = { X } )
	1wlkd.j	|- ( ( ph /\ X =/= Y ) -> { X , Y } C_ ( I ` J ) )
Assertion	1wlkdlem3	|- ( ph -> F e. Word dom I )

Proof

Step	Hyp	Ref	Expression
1		1wlkd.p	|- P = <" X Y ">
2		1wlkd.f	|- F = <" J ">
3		1wlkd.x	|- ( ph -> X e. V )
4		1wlkd.y	|- ( ph -> Y e. V )
5		1wlkd.l	|- ( ( ph /\ X = Y ) -> ( I ` J ) = { X } )
6		1wlkd.j	|- ( ( ph /\ X =/= Y ) -> { X , Y } C_ ( I ` J ) )
7	1 2 3 4 5 6	1wlkdlem2	|- ( ph -> X e. ( I ` J ) )
8		elfvdm	|- ( X e. ( I ` J ) -> J e. dom I )
9		s1cl	|- ( J e. dom I -> <" J "> e. Word dom I )
10	2 9	eqeltrid	|- ( J e. dom I -> F e. Word dom I )
11	7 8 10	3syl	|- ( ph -> F e. Word dom I )