Theorem vdwlem4

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

	Ref	Expression
Hypotheses	vdwlem3.v	⊢ ( 𝜑 → 𝑉 ∈ ℕ )
	vdwlem3.w	⊢ ( 𝜑 → 𝑊 ∈ ℕ )
	vdwlem4.r	⊢ ( 𝜑 → 𝑅 ∈ Fin )
	vdwlem4.h	⊢ ( 𝜑 → 𝐻 : ( 1 ... ( 𝑊 · ( 2 · 𝑉 ) ) ) ⟶ 𝑅 )
	vdwlem4.f	⊢ 𝐹 = ( 𝑥 ∈ ( 1 ... 𝑉 ) ↦ ( 𝑦 ∈ ( 1 ... 𝑊 ) ↦ ( 𝐻 ‘ ( 𝑦 + ( 𝑊 · ( ( 𝑥 − 1 ) + 𝑉 ) ) ) ) ) )
Assertion	vdwlem4	⊢ ( 𝜑 → 𝐹 : ( 1 ... 𝑉 ) ⟶ ( 𝑅 ↑m ( 1 ... 𝑊 ) ) )

Proof

Step	Hyp	Ref	Expression
1		vdwlem3.v	⊢ ( 𝜑 → 𝑉 ∈ ℕ )
2		vdwlem3.w	⊢ ( 𝜑 → 𝑊 ∈ ℕ )
3		vdwlem4.r	⊢ ( 𝜑 → 𝑅 ∈ Fin )
4		vdwlem4.h	⊢ ( 𝜑 → 𝐻 : ( 1 ... ( 𝑊 · ( 2 · 𝑉 ) ) ) ⟶ 𝑅 )
5		vdwlem4.f	⊢ 𝐹 = ( 𝑥 ∈ ( 1 ... 𝑉 ) ↦ ( 𝑦 ∈ ( 1 ... 𝑊 ) ↦ ( 𝐻 ‘ ( 𝑦 + ( 𝑊 · ( ( 𝑥 − 1 ) + 𝑉 ) ) ) ) ) )
6	4	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑉 ) ) ∧ 𝑦 ∈ ( 1 ... 𝑊 ) ) → 𝐻 : ( 1 ... ( 𝑊 · ( 2 · 𝑉 ) ) ) ⟶ 𝑅 )
7	1	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑉 ) ) ∧ 𝑦 ∈ ( 1 ... 𝑊 ) ) → 𝑉 ∈ ℕ )
8	2	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑉 ) ) ∧ 𝑦 ∈ ( 1 ... 𝑊 ) ) → 𝑊 ∈ ℕ )
9		simplr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑉 ) ) ∧ 𝑦 ∈ ( 1 ... 𝑊 ) ) → 𝑥 ∈ ( 1 ... 𝑉 ) )
10		simpr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑉 ) ) ∧ 𝑦 ∈ ( 1 ... 𝑊 ) ) → 𝑦 ∈ ( 1 ... 𝑊 ) )
11	7 8 9 10	vdwlem3	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑉 ) ) ∧ 𝑦 ∈ ( 1 ... 𝑊 ) ) → ( 𝑦 + ( 𝑊 · ( ( 𝑥 − 1 ) + 𝑉 ) ) ) ∈ ( 1 ... ( 𝑊 · ( 2 · 𝑉 ) ) ) )
12	6 11	ffvelrnd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑉 ) ) ∧ 𝑦 ∈ ( 1 ... 𝑊 ) ) → ( 𝐻 ‘ ( 𝑦 + ( 𝑊 · ( ( 𝑥 − 1 ) + 𝑉 ) ) ) ) ∈ 𝑅 )
13	12	fmpttd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑉 ) ) → ( 𝑦 ∈ ( 1 ... 𝑊 ) ↦ ( 𝐻 ‘ ( 𝑦 + ( 𝑊 · ( ( 𝑥 − 1 ) + 𝑉 ) ) ) ) ) : ( 1 ... 𝑊 ) ⟶ 𝑅 )
14	3	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑉 ) ) → 𝑅 ∈ Fin )
15		ovex	⊢ ( 1 ... 𝑊 ) ∈ V
16		elmapg	⊢ ( ( 𝑅 ∈ Fin ∧ ( 1 ... 𝑊 ) ∈ V ) → ( ( 𝑦 ∈ ( 1 ... 𝑊 ) ↦ ( 𝐻 ‘ ( 𝑦 + ( 𝑊 · ( ( 𝑥 − 1 ) + 𝑉 ) ) ) ) ) ∈ ( 𝑅 ↑m ( 1 ... 𝑊 ) ) ↔ ( 𝑦 ∈ ( 1 ... 𝑊 ) ↦ ( 𝐻 ‘ ( 𝑦 + ( 𝑊 · ( ( 𝑥 − 1 ) + 𝑉 ) ) ) ) ) : ( 1 ... 𝑊 ) ⟶ 𝑅 ) )
17	14 15 16	sylancl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑉 ) ) → ( ( 𝑦 ∈ ( 1 ... 𝑊 ) ↦ ( 𝐻 ‘ ( 𝑦 + ( 𝑊 · ( ( 𝑥 − 1 ) + 𝑉 ) ) ) ) ) ∈ ( 𝑅 ↑m ( 1 ... 𝑊 ) ) ↔ ( 𝑦 ∈ ( 1 ... 𝑊 ) ↦ ( 𝐻 ‘ ( 𝑦 + ( 𝑊 · ( ( 𝑥 − 1 ) + 𝑉 ) ) ) ) ) : ( 1 ... 𝑊 ) ⟶ 𝑅 ) )
18	13 17	mpbird	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑉 ) ) → ( 𝑦 ∈ ( 1 ... 𝑊 ) ↦ ( 𝐻 ‘ ( 𝑦 + ( 𝑊 · ( ( 𝑥 − 1 ) + 𝑉 ) ) ) ) ) ∈ ( 𝑅 ↑m ( 1 ... 𝑊 ) ) )
19	18 5	fmptd	⊢ ( 𝜑 → 𝐹 : ( 1 ... 𝑉 ) ⟶ ( 𝑅 ↑m ( 1 ... 𝑊 ) ) )