Metamath Proof Explorer

Theorem vdwapf

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

Ref Expression
Assertion vdwapf ⊢K∈ℕ0→AP⁡K:ℕ×ℕ⟶𝒫ℕ

Proof

Step Hyp Ref Expression
1 simpll ⊢a∈ℕ∧d∈ℕ∧m∈0…K−1→a∈ℕ
2 elfznn0 ⊢m∈0…K−1→m∈ℕ0
3 2 adantl ⊢a∈ℕ∧d∈ℕ∧m∈0…K−1→m∈ℕ0
4 nnnn0 ⊢d∈ℕ→d∈ℕ0
5 4 ad2antlr ⊢a∈ℕ∧d∈ℕ∧m∈0…K−1→d∈ℕ0
6 3 5 nn0mulcld ⊢a∈ℕ∧d∈ℕ∧m∈0…K−1→m⁢d∈ℕ0
7 nnnn0addcl ⊢a∈ℕ∧m⁢d∈ℕ0→a+m⁢d∈ℕ
8 1 6 7 syl2anc ⊢a∈ℕ∧d∈ℕ∧m∈0…K−1→a+m⁢d∈ℕ
9 8 fmpttd ⊢a∈ℕ∧d∈ℕ→m∈0…K−1⟼a+m⁢d:0…K−1⟶ℕ
10 9 frnd ⊢a∈ℕ∧d∈ℕ→ran⁡m∈0…K−1⟼a+m⁢d⊆ℕ
11 nnex ⊢ℕ∈V
12 11 elpw2 ⊢ran⁡m∈0…K−1⟼a+m⁢d∈𝒫ℕ↔ran⁡m∈0…K−1⟼a+m⁢d⊆ℕ
13 10 12 sylibr ⊢a∈ℕ∧d∈ℕ→ran⁡m∈0…K−1⟼a+m⁢d∈𝒫ℕ
14 13 rgen2 ⊢∀a∈ℕ∀d∈ℕran⁡m∈0…K−1⟼a+m⁢d∈𝒫ℕ
15 eqid ⊢a∈ℕ,d∈ℕ⟼ran⁡m∈0…K−1⟼a+m⁢d=a∈ℕ,d∈ℕ⟼ran⁡m∈0…K−1⟼a+m⁢d
16 15 fmpo ⊢∀a∈ℕ∀d∈ℕran⁡m∈0…K−1⟼a+m⁢d∈𝒫ℕ↔a∈ℕ,d∈ℕ⟼ran⁡m∈0…K−1⟼a+m⁢d:ℕ×ℕ⟶𝒫ℕ
17 14 16 mpbi ⊢a∈ℕ,d∈ℕ⟼ran⁡m∈0…K−1⟼a+m⁢d:ℕ×ℕ⟶𝒫ℕ
18 vdwapfval ⊢K∈ℕ0→AP⁡K=a∈ℕ,d∈ℕ⟼ran⁡m∈0…K−1⟼a+m⁢d
19 18 feq1d ⊢K∈ℕ0→AP⁡K:ℕ×ℕ⟶𝒫ℕ↔a∈ℕ,d∈ℕ⟼ran⁡m∈0…K−1⟼a+m⁢d:ℕ×ℕ⟶𝒫ℕ
20 17 19 mpbiri ⊢K∈ℕ0→AP⁡K:ℕ×ℕ⟶𝒫ℕ