Metamath Proof Explorer

Theorem vdwlem4

Description: Lemma for vdw . (Contributed by Mario Carneiro, 12-Sep-2014)

		Ref	Expression
	Hypotheses	vdwlem3.v	$⊢ φ \to V \in ℕ$
		vdwlem3.w	$⊢ φ \to W \in ℕ$
		vdwlem4.r	$⊢ φ \to R \in Fin$
		vdwlem4.h	$⊢ φ \to H : (1 \dots W 2 V) ⟶ R$
		vdwlem4.f	$⊢ F = (x \in (1 \dots V) ⟼ (y \in (1 \dots W) ⟼ H (y + W (x - 1 + V))))$
	Assertion	vdwlem4	$⊢ φ \to F : (1 \dots V) ⟶ R^{(1 \dots W)}$

Proof

Step	Hyp	Ref	Expression
1		vdwlem3.v	$⊢ φ \to V \in ℕ$
2		vdwlem3.w	$⊢ φ \to W \in ℕ$
3		vdwlem4.r	$⊢ φ \to R \in Fin$
4		vdwlem4.h	$⊢ φ \to H : (1 \dots W 2 V) ⟶ R$
5		vdwlem4.f	$⊢ F = (x \in (1 \dots V) ⟼ (y \in (1 \dots W) ⟼ H (y + W (x - 1 + V))))$
6	4	ad2antrr	$⊢ ((φ \land x \in (1 \dots V)) \land y \in (1 \dots W)) \to H : (1 \dots W 2 V) ⟶ R$
7	1	ad2antrr	$⊢ ((φ \land x \in (1 \dots V)) \land y \in (1 \dots W)) \to V \in ℕ$
8	2	ad2antrr	$⊢ ((φ \land x \in (1 \dots V)) \land y \in (1 \dots W)) \to W \in ℕ$
9		simplr	$⊢ ((φ \land x \in (1 \dots V)) \land y \in (1 \dots W)) \to x \in (1 \dots V)$
10		simpr	$⊢ ((φ \land x \in (1 \dots V)) \land y \in (1 \dots W)) \to y \in (1 \dots W)$
11	7 8 9 10	vdwlem3	$⊢ ((φ \land x \in (1 \dots V)) \land y \in (1 \dots W)) \to y + W (x - 1 + V) \in (1 \dots W 2 V)$
12	6 11	ffvelrnd	$⊢ ((φ \land x \in (1 \dots V)) \land y \in (1 \dots W)) \to H (y + W (x - 1 + V)) \in R$
13	12	fmpttd	$⊢ (φ \land x \in (1 \dots V)) \to (y \in (1 \dots W) ⟼ H (y + W (x - 1 + V))) : (1 \dots W) ⟶ R$
14	3	adantr	$⊢ (φ \land x \in (1 \dots V)) \to R \in Fin$
15		ovex	$⊢ (1 \dots W) \in V$
16		elmapg	$⊢ (R \in Fin \land (1 \dots W) \in V) \to ((y \in (1 \dots W) ⟼ H (y + W (x - 1 + V))) \in (R^{(1 \dots W)}) \leftrightarrow (y \in (1 \dots W) ⟼ H (y + W (x - 1 + V))) : (1 \dots W) ⟶ R)$
17	14 15 16	sylancl	$⊢ (φ \land x \in (1 \dots V)) \to ((y \in (1 \dots W) ⟼ H (y + W (x - 1 + V))) \in (R^{(1 \dots W)}) \leftrightarrow (y \in (1 \dots W) ⟼ H (y + W (x - 1 + V))) : (1 \dots W) ⟶ R)$
18	13 17	mpbird	$⊢ (φ \land x \in (1 \dots V)) \to (y \in (1 \dots W) ⟼ H (y + W (x - 1 + V))) \in (R^{(1 \dots W)})$
19	18 5	fmptd	$⊢ φ \to F : (1 \dots V) ⟶ R^{(1 \dots W)}$