Theorem 1wlkdlem2

Description: Lemma 2 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	1wlkdlem2	|- ( ph -> X e. ( I ` J ) )

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		snidg	|- ( X e. V -> X e. { X } )
8	3 7	syl	|- ( ph -> X e. { X } )
9	8	adantr	|- ( ( ph /\ X = Y ) -> X e. { X } )
10	9 5	eleqtrrd	|- ( ( ph /\ X = Y ) -> X e. ( I ` J ) )
11	4	adantr	|- ( ( ph /\ X =/= Y ) -> Y e. V )
12		prssg	|- ( ( X e. V /\ Y e. V ) -> ( ( X e. ( I ` J ) /\ Y e. ( I ` J ) ) <-> { X , Y } C_ ( I ` J ) ) )
13	3 11 12	syl2an2r	|- ( ( ph /\ X =/= Y ) -> ( ( X e. ( I ` J ) /\ Y e. ( I ` J ) ) <-> { X , Y } C_ ( I ` J ) ) )
14	6 13	mpbird	|- ( ( ph /\ X =/= Y ) -> ( X e. ( I ` J ) /\ Y e. ( I ` J ) ) )
15	14	simpld	|- ( ( ph /\ X =/= Y ) -> X e. ( I ` J ) )
16	10 15	pm2.61dane	|- ( ph -> X e. ( I ` J ) )