Theorem 1wlkdlem2

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

	Ref	Expression
Hypotheses	1wlkd.p	$$⊢P=⟨“XY”⟩$$
	1wlkd.f	$$⊢F=⟨“J”⟩$$
	1wlkd.x	$$⊢\phi \to X\in V$$
	1wlkd.y	$$⊢\phi \to Y\in V$$
	1wlkd.l	$$⊢\left(\phi \wedge X=Y\right)\to I\left(J\right)=\left\{X\right\}$$
	1wlkd.j	$$⊢\left(\phi \wedge X\ne Y\right)\to \left\{X,Y\right\}\subseteq I\left(J\right)$$
Assertion	1wlkdlem2	$$⊢\phi \to X\in I\left(J\right)$$

Proof

Step	Hyp	Ref	Expression
1		1wlkd.p	$$⊢P=⟨“XY”⟩$$
2		1wlkd.f	$$⊢F=⟨“J”⟩$$
3		1wlkd.x	$$⊢\phi \to X\in V$$
4		1wlkd.y	$$⊢\phi \to Y\in V$$
5		1wlkd.l	$$⊢\left(\phi \wedge X=Y\right)\to I\left(J\right)=\left\{X\right\}$$
6		1wlkd.j	$$⊢\left(\phi \wedge X\ne Y\right)\to \left\{X,Y\right\}\subseteq I\left(J\right)$$
7		snidg	$$⊢X\in V\to X\in \left\{X\right\}$$
8	3 7	syl	$$⊢\phi \to X\in \left\{X\right\}$$
9	8	adantr	$$⊢\left(\phi \wedge X=Y\right)\to X\in \left\{X\right\}$$
10	9 5	eleqtrrd	$$⊢\left(\phi \wedge X=Y\right)\to X\in I\left(J\right)$$
11	4	adantr	$$⊢\left(\phi \wedge X\ne Y\right)\to Y\in V$$
12		prssg	$$⊢\left(X\in V\wedge Y\in V\right)\to \left(\left(X\in I\left(J\right)\wedge Y\in I\left(J\right)\right)\leftrightarrow \left\{X,Y\right\}\subseteq I\left(J\right)\right)$$
13	3 11 12	syl2an2r	$$⊢\left(\phi \wedge X\ne Y\right)\to \left(\left(X\in I\left(J\right)\wedge Y\in I\left(J\right)\right)\leftrightarrow \left\{X,Y\right\}\subseteq I\left(J\right)\right)$$
14	6 13	mpbird	$$⊢\left(\phi \wedge X\ne Y\right)\to \left(X\in I\left(J\right)\wedge Y\in I\left(J\right)\right)$$
15	14	simpld	$$⊢\left(\phi \wedge X\ne Y\right)\to X\in I\left(J\right)$$
16	10 15	pm2.61dane	$$⊢\phi \to X\in I\left(J\right)$$