Metamath Proof Explorer

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 ‘ 𝐾 ) : ( ℕ × ℕ ) ⟶ 𝒫 ℕ )