Theorem 1wlkdlem3

Description: Lemma 3 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	1wlkdlem3	$$⊢\phi \to F\in \mathrm{Word}\mathrm{dom}I$$

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	1 2 3 4 5 6	1wlkdlem2	$$⊢\phi \to X\in I\left(J\right)$$
8		elfvdm	$$⊢X\in I\left(J\right)\to J\in \mathrm{dom}I$$
9		s1cl	$$⊢J\in \mathrm{dom}I\to ⟨“J”⟩\in \mathrm{Word}\mathrm{dom}I$$
10	2 9	eqeltrid	$$⊢J\in \mathrm{dom}I\to F\in \mathrm{Word}\mathrm{dom}I$$
11	7 8 10	3syl	$$⊢\phi \to F\in \mathrm{Word}\mathrm{dom}I$$