Theorem 1pthdlem1

Description: Lemma 1 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	1pthdlem1	$$⊢\mathrm{Fun}{\left({P\upharpoonright }_{\left(1..^\left|F\right|\right)}\right)}^{-1}$$

Proof

Step	Hyp	Ref	Expression
1		1wlkd.p	$$⊢P=⟨“XY”⟩$$
2		1wlkd.f	$$⊢F=⟨“J”⟩$$
3		fun0	$$⊢\mathrm{Fun}\varnothing$$
4	2	fveq2i	$$⊢\left|F\right|=\left|⟨“J”⟩\right|$$
5		s1len	$$⊢\left|⟨“J”⟩\right|=1$$
6	4 5	eqtri	$$⊢\left|F\right|=1$$
7	6	oveq2i	$$⊢\left(1..^\left|F\right|\right)=\left(1..^1\right)$$
8		fzo0	$$⊢\left(1..^1\right)=\varnothing$$
9	7 8	eqtri	$$⊢\left(1..^\left|F\right|\right)=\varnothing$$
10	9	reseq2i	$$⊢{P\upharpoonright }_{\left(1..^\left|F\right|\right)}={P\upharpoonright }_{\varnothing }$$
11		res0	$$⊢{P\upharpoonright }_{\varnothing }=\varnothing$$
12	10 11	eqtri	$$⊢{P\upharpoonright }_{\left(1..^\left|F\right|\right)}=\varnothing$$
13	12	cnveqi	$$⊢{\left({P\upharpoonright }_{\left(1..^\left|F\right|\right)}\right)}^{-1}={\varnothing }^{-1}$$
14		cnv0	$$⊢{\varnothing }^{-1}=\varnothing$$
15	13 14	eqtri	$$⊢{\left({P\upharpoonright }_{\left(1..^\left|F\right|\right)}\right)}^{-1}=\varnothing$$
16	15	funeqi	$$⊢\mathrm{Fun}{\left({P\upharpoonright }_{\left(1..^\left|F\right|\right)}\right)}^{-1}\leftrightarrow \mathrm{Fun}\varnothing$$
17	3 16	mpbir	$$⊢\mathrm{Fun}{\left({P\upharpoonright }_{\left(1..^\left|F\right|\right)}\right)}^{-1}$$