Theorem 1pthdlem2

Description: Lemma 2 for 1pthd . (Contributed by Alexander van der Vekens, 4-Dec-2017) (Revised by AV, 22-Jan-2021)

	Ref	Expression
Hypotheses	1wlkd.p	$$⊢P=⟨“XY”⟩$$
	1wlkd.f	$$⊢F=⟨“J”⟩$$
Assertion	1pthdlem2	$$⊢P\left[\left\{0,\left|F\right|\right\}\right]\cap P\left[\left(1..^\left|F\right|\right)\right]=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		1wlkd.p	$$⊢P=⟨“XY”⟩$$
2		1wlkd.f	$$⊢F=⟨“J”⟩$$
3	2	fveq2i	$$⊢\left|F\right|=\left|⟨“J”⟩\right|$$
4		s1len	$$⊢\left|⟨“J”⟩\right|=1$$
5	3 4	eqtri	$$⊢\left|F\right|=1$$
6	5	oveq2i	$$⊢\left(1..^\left|F\right|\right)=\left(1..^1\right)$$
7		fzo0	$$⊢\left(1..^1\right)=\varnothing$$
8	6 7	eqtri	$$⊢\left(1..^\left|F\right|\right)=\varnothing$$
9	8	imaeq2i	$$⊢P\left[\left(1..^\left|F\right|\right)\right]=P\left[\varnothing \right]$$
10	9	ineq2i	$$⊢P\left[\left\{0,\left|F\right|\right\}\right]\cap P\left[\left(1..^\left|F\right|\right)\right]=P\left[\left\{0,\left|F\right|\right\}\right]\cap P\left[\varnothing \right]$$
11		ima0	$$⊢P\left[\varnothing \right]=\varnothing$$
12	11	ineq2i	$$⊢P\left[\left\{0,\left|F\right|\right\}\right]\cap P\left[\varnothing \right]=P\left[\left\{0,\left|F\right|\right\}\right]\cap \varnothing$$
13		in0	$$⊢P\left[\left\{0,\left|F\right|\right\}\right]\cap \varnothing =\varnothing$$
14	12 13	eqtri	$$⊢P\left[\left\{0,\left|F\right|\right\}\right]\cap P\left[\varnothing \right]=\varnothing$$
15	10 14	eqtri	$$⊢P\left[\left\{0,\left|F\right|\right\}\right]\cap P\left[\left(1..^\left|F\right|\right)\right]=\varnothing$$