Theorem vdwapf

Description: The arithmetic progression function is a function. (Contributed by Mario Carneiro, 18-Aug-2014)

	Ref	Expression
Assertion	vdwapf	⊢ ( 𝐾 ∈ ℕ0 → ( AP ‘ 𝐾 ) : ( ℕ × ℕ ) ⟶ 𝒫 ℕ )

Proof

Step	Hyp	Ref	Expression
1		simpll	⊢ ( ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → 𝑎 ∈ ℕ )
2		elfznn0	⊢ ( 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) → 𝑚 ∈ ℕ0 )
3	2	adantl	⊢ ( ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → 𝑚 ∈ ℕ0 )
4		nnnn0	⊢ ( 𝑑 ∈ ℕ → 𝑑 ∈ ℕ0 )
5	4	ad2antlr	⊢ ( ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → 𝑑 ∈ ℕ0 )
6	3 5	nn0mulcld	⊢ ( ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → ( 𝑚 · 𝑑 ) ∈ ℕ0 )
7		nnnn0addcl	⊢ ( ( 𝑎 ∈ ℕ ∧ ( 𝑚 · 𝑑 ) ∈ ℕ0 ) → ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ℕ )
8	1 6 7	syl2anc	⊢ ( ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ℕ )
9	8	fmpttd	⊢ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) → ( 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ↦ ( 𝑎 + ( 𝑚 · 𝑑 ) ) ) : ( 0 ... ( 𝐾 − 1 ) ) ⟶ ℕ )
10	9	frnd	⊢ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) → ran ( 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ↦ ( 𝑎 + ( 𝑚 · 𝑑 ) ) ) ⊆ ℕ )
11		nnex	⊢ ℕ ∈ V
12	11	elpw2	⊢ ( ran ( 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ↦ ( 𝑎 + ( 𝑚 · 𝑑 ) ) ) ∈ 𝒫 ℕ ↔ ran ( 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ↦ ( 𝑎 + ( 𝑚 · 𝑑 ) ) ) ⊆ ℕ )
13	10 12	sylibr	⊢ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) → ran ( 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ↦ ( 𝑎 + ( 𝑚 · 𝑑 ) ) ) ∈ 𝒫 ℕ )
14	13	rgen2	⊢ ∀ 𝑎 ∈ ℕ ∀ 𝑑 ∈ ℕ ran ( 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ↦ ( 𝑎 + ( 𝑚 · 𝑑 ) ) ) ∈ 𝒫 ℕ
15		eqid	⊢ ( 𝑎 ∈ ℕ , 𝑑 ∈ ℕ ↦ ran ( 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ↦ ( 𝑎 + ( 𝑚 · 𝑑 ) ) ) ) = ( 𝑎 ∈ ℕ , 𝑑 ∈ ℕ ↦ ran ( 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ↦ ( 𝑎 + ( 𝑚 · 𝑑 ) ) ) )
16	15	fmpo	⊢ ( ∀ 𝑎 ∈ ℕ ∀ 𝑑 ∈ ℕ ran ( 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ↦ ( 𝑎 + ( 𝑚 · 𝑑 ) ) ) ∈ 𝒫 ℕ ↔ ( 𝑎 ∈ ℕ , 𝑑 ∈ ℕ ↦ ran ( 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ↦ ( 𝑎 + ( 𝑚 · 𝑑 ) ) ) ) : ( ℕ × ℕ ) ⟶ 𝒫 ℕ )
17	14 16	mpbi	⊢ ( 𝑎 ∈ ℕ , 𝑑 ∈ ℕ ↦ ran ( 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ↦ ( 𝑎 + ( 𝑚 · 𝑑 ) ) ) ) : ( ℕ × ℕ ) ⟶ 𝒫 ℕ
18		vdwapfval	⊢ ( 𝐾 ∈ ℕ0 → ( AP ‘ 𝐾 ) = ( 𝑎 ∈ ℕ , 𝑑 ∈ ℕ ↦ ran ( 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ↦ ( 𝑎 + ( 𝑚 · 𝑑 ) ) ) ) )
19	18	feq1d	⊢ ( 𝐾 ∈ ℕ0 → ( ( AP ‘ 𝐾 ) : ( ℕ × ℕ ) ⟶ 𝒫 ℕ ↔ ( 𝑎 ∈ ℕ , 𝑑 ∈ ℕ ↦ ran ( 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ↦ ( 𝑎 + ( 𝑚 · 𝑑 ) ) ) ) : ( ℕ × ℕ ) ⟶ 𝒫 ℕ ) )
20	17 19	mpbiri	⊢ ( 𝐾 ∈ ℕ0 → ( AP ‘ 𝐾 ) : ( ℕ × ℕ ) ⟶ 𝒫 ℕ )