1pthdlem1

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

Metamath Proof Explorer