Theorem upgr1wlkdlem1

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

	Ref	Expression
Hypotheses	upgr1wlkd.p	|- P = <" X Y ">
	upgr1wlkd.f	|- F = <" J ">
	upgr1wlkd.x	|- ( ph -> X e. ( Vtx ` G ) )
	upgr1wlkd.y	|- ( ph -> Y e. ( Vtx ` G ) )
	upgr1wlkd.j	|- ( ph -> ( ( iEdg ` G ) ` J ) = { X , Y } )
Assertion	upgr1wlkdlem1	|- ( ( ph /\ X = Y ) -> ( ( iEdg ` G ) ` J ) = { X } )

Proof

Step	Hyp	Ref	Expression
1		upgr1wlkd.p	|- P = <" X Y ">
2		upgr1wlkd.f	|- F = <" J ">
3		upgr1wlkd.x	|- ( ph -> X e. ( Vtx ` G ) )
4		upgr1wlkd.y	|- ( ph -> Y e. ( Vtx ` G ) )
5		upgr1wlkd.j	|- ( ph -> ( ( iEdg ` G ) ` J ) = { X , Y } )
6		preq2	|- ( Y = X -> { X , Y } = { X , X } )
7	6	eqeq2d	|- ( Y = X -> ( ( ( iEdg ` G ) ` J ) = { X , Y } <-> ( ( iEdg ` G ) ` J ) = { X , X } ) )
8	7	eqcoms	|- ( X = Y -> ( ( ( iEdg ` G ) ` J ) = { X , Y } <-> ( ( iEdg ` G ) ` J ) = { X , X } ) )
9		simpl	|- ( ( ( ( iEdg ` G ) ` J ) = { X , X } /\ ph ) -> ( ( iEdg ` G ) ` J ) = { X , X } )
10		dfsn2	|- { X } = { X , X }
11	9 10	eqtr4di	|- ( ( ( ( iEdg ` G ) ` J ) = { X , X } /\ ph ) -> ( ( iEdg ` G ) ` J ) = { X } )
12	11	ex	|- ( ( ( iEdg ` G ) ` J ) = { X , X } -> ( ph -> ( ( iEdg ` G ) ` J ) = { X } ) )
13	8 12	syl6bi	|- ( X = Y -> ( ( ( iEdg ` G ) ` J ) = { X , Y } -> ( ph -> ( ( iEdg ` G ) ` J ) = { X } ) ) )
14	13	com13	|- ( ph -> ( ( ( iEdg ` G ) ` J ) = { X , Y } -> ( X = Y -> ( ( iEdg ` G ) ` J ) = { X } ) ) )
15	5 14	mpd	|- ( ph -> ( X = Y -> ( ( iEdg ` G ) ` J ) = { X } ) )
16	15	imp	|- ( ( ph /\ X = Y ) -> ( ( iEdg ` G ) ` J ) = { X } )