1pthdlem2

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

Metamath Proof Explorer