wlkdlem1

Step	Hyp	Ref	Expression
1		wlkd.p	$⊢ φ \to P \in Word V$
2		wlkd.f	$⊢ φ \to F \in Word V$
3		wlkd.l	$⊢ φ \to \|P\| = \|F\| + 1$
4		wlkdlem1.v	$⊢ φ \to \forall k \in (0 \dots \|F\|) P (k) \in V$
5		wrdf	$⊢ P \in Word V \to P : (0 ..^\|P\|) ⟶ V$
6	1 5	syl	$⊢ φ \to P : (0 ..^\|P\|) ⟶ V$
7	3	oveq2d	$⊢ φ \to (0 ..^\|P\|) = (0 ..^\|F\| + 1)$
8		lencl	$⊢ F \in Word V \to \|F\| \in ℕ_{0}$
9	2 8	syl	$⊢ φ \to \|F\| \in ℕ_{0}$
10	9	nn0zd	$⊢ φ \to \|F\| \in ℤ$
11		fzval3	$⊢ \|F\| \in ℤ \to (0 \dots \|F\|) = (0 ..^\|F\| + 1)$
12	10 11	syl	$⊢ φ \to (0 \dots \|F\|) = (0 ..^\|F\| + 1)$
13	7 12	eqtr4d	$⊢ φ \to (0 ..^\|P\|) = (0 \dots \|F\|)$
14	13	feq2d	$⊢ φ \to (P : (0 ..^\|P\|) ⟶ V \leftrightarrow P : (0 \dots \|F\|) ⟶ V)$
15		ssv	$⊢ V \subseteq V$
16		fcdmssb	$⊢ (V \subseteq V \land \forall k \in (0 \dots \|F\|) P (k) \in V) \to (P : (0 \dots \|F\|) ⟶ V \leftrightarrow P : (0 \dots \|F\|) ⟶ V)$
17	15 4 16	sylancr	$⊢ φ \to (P : (0 \dots \|F\|) ⟶ V \leftrightarrow P : (0 \dots \|F\|) ⟶ V)$
18	14 17	bitrd	$⊢ φ \to (P : (0 ..^\|P\|) ⟶ V \leftrightarrow P : (0 \dots \|F\|) ⟶ V)$
19	6 18	mpbid	$⊢ φ \to P : (0 \dots \|F\|) ⟶ V$

Metamath Proof Explorer