Step | Hyp | Ref
| Expression |
1 | | vdwmc.1 |
. . 3
⊢ 𝑋 ∈ V |
2 | | vdwmc.2 |
. . 3
⊢ (𝜑 → 𝐾 ∈
ℕ0) |
3 | | vdwmc.3 |
. . 3
⊢ (𝜑 → 𝐹:𝑋⟶𝑅) |
4 | 1, 2, 3 | vdwmc 15520 |
. 2
⊢ (𝜑 → (𝐾 MonoAP 𝐹 ↔ ∃𝑐∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑐}))) |
5 | | vdwapid1 15517 |
. . . . . . . . . . . 12
⊢ ((𝐾 ∈ ℕ ∧ 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) → 𝑎 ∈ (𝑎(AP‘𝐾)𝑑)) |
6 | | ne0i 3880 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ (𝑎(AP‘𝐾)𝑑) → (𝑎(AP‘𝐾)𝑑) ≠ ∅) |
7 | 5, 6 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝐾 ∈ ℕ ∧ 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) → (𝑎(AP‘𝐾)𝑑) ≠ ∅) |
8 | 7 | 3expb 1258 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ ℕ ∧ (𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ)) → (𝑎(AP‘𝐾)𝑑) ≠ ∅) |
9 | 8 | adantll 746 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐾 ∈ ℕ) ∧ (𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ)) → (𝑎(AP‘𝐾)𝑑) ≠ ∅) |
10 | | ssn0 3928 |
. . . . . . . . . 10
⊢ (((𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑐}) ∧ (𝑎(AP‘𝐾)𝑑) ≠ ∅) → (◡𝐹 “ {𝑐}) ≠ ∅) |
11 | 10 | expcom 450 |
. . . . . . . . 9
⊢ ((𝑎(AP‘𝐾)𝑑) ≠ ∅ → ((𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑐}) → (◡𝐹 “ {𝑐}) ≠ ∅)) |
12 | 9, 11 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐾 ∈ ℕ) ∧ (𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ)) → ((𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑐}) → (◡𝐹 “ {𝑐}) ≠ ∅)) |
13 | | disjsn 4192 |
. . . . . . . . . 10
⊢ ((𝑅 ∩ {𝑐}) = ∅ ↔ ¬ 𝑐 ∈ 𝑅) |
14 | 3 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐾 ∈ ℕ) → 𝐹:𝑋⟶𝑅) |
15 | | fimacnvdisj 5996 |
. . . . . . . . . . . . 13
⊢ ((𝐹:𝑋⟶𝑅 ∧ (𝑅 ∩ {𝑐}) = ∅) → (◡𝐹 “ {𝑐}) = ∅) |
16 | 15 | ex 449 |
. . . . . . . . . . . 12
⊢ (𝐹:𝑋⟶𝑅 → ((𝑅 ∩ {𝑐}) = ∅ → (◡𝐹 “ {𝑐}) = ∅)) |
17 | 14, 16 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐾 ∈ ℕ) → ((𝑅 ∩ {𝑐}) = ∅ → (◡𝐹 “ {𝑐}) = ∅)) |
18 | 17 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐾 ∈ ℕ) ∧ (𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ)) → ((𝑅 ∩ {𝑐}) = ∅ → (◡𝐹 “ {𝑐}) = ∅)) |
19 | 13, 18 | syl5bir 232 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐾 ∈ ℕ) ∧ (𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ)) → (¬ 𝑐 ∈ 𝑅 → (◡𝐹 “ {𝑐}) = ∅)) |
20 | 19 | necon1ad 2799 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐾 ∈ ℕ) ∧ (𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ)) → ((◡𝐹 “ {𝑐}) ≠ ∅ → 𝑐 ∈ 𝑅)) |
21 | 12, 20 | syld 46 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐾 ∈ ℕ) ∧ (𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ)) → ((𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑐}) → 𝑐 ∈ 𝑅)) |
22 | 21 | rexlimdvva 3020 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐾 ∈ ℕ) → (∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑐}) → 𝑐 ∈ 𝑅)) |
23 | 22 | pm4.71rd 665 |
. . . . 5
⊢ ((𝜑 ∧ 𝐾 ∈ ℕ) → (∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑐}) ↔ (𝑐 ∈ 𝑅 ∧ ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑐})))) |
24 | 23 | exbidv 1837 |
. . . 4
⊢ ((𝜑 ∧ 𝐾 ∈ ℕ) → (∃𝑐∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑐}) ↔ ∃𝑐(𝑐 ∈ 𝑅 ∧ ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑐})))) |
25 | | df-rex 2902 |
. . . 4
⊢
(∃𝑐 ∈
𝑅 ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑐}) ↔ ∃𝑐(𝑐 ∈ 𝑅 ∧ ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑐}))) |
26 | 24, 25 | syl6bbr 277 |
. . 3
⊢ ((𝜑 ∧ 𝐾 ∈ ℕ) → (∃𝑐∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑐}) ↔ ∃𝑐 ∈ 𝑅 ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑐}))) |
27 | | vdwmc2.4 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ 𝑋) |
28 | 3, 27 | ffvelrnd 6268 |
. . . . . . . 8
⊢ (𝜑 → (𝐹‘𝐴) ∈ 𝑅) |
29 | | ne0i 3880 |
. . . . . . . 8
⊢ ((𝐹‘𝐴) ∈ 𝑅 → 𝑅 ≠ ∅) |
30 | 28, 29 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑅 ≠ ∅) |
31 | 30 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐾 = 0) → 𝑅 ≠ ∅) |
32 | | 1nn 10908 |
. . . . . . . . 9
⊢ 1 ∈
ℕ |
33 | 32 | ne0ii 3882 |
. . . . . . . 8
⊢ ℕ
≠ ∅ |
34 | | simpllr 795 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝐾 = 0) ∧ 𝑎 ∈ ℕ) ∧ 𝑑 ∈ ℕ) → 𝐾 = 0) |
35 | 34 | fveq2d 6107 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝐾 = 0) ∧ 𝑎 ∈ ℕ) ∧ 𝑑 ∈ ℕ) → (AP‘𝐾) =
(AP‘0)) |
36 | 35 | oveqd 6566 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝐾 = 0) ∧ 𝑎 ∈ ℕ) ∧ 𝑑 ∈ ℕ) → (𝑎(AP‘𝐾)𝑑) = (𝑎(AP‘0)𝑑)) |
37 | | vdwap0 15518 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) → (𝑎(AP‘0)𝑑) = ∅) |
38 | 37 | adantll 746 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝐾 = 0) ∧ 𝑎 ∈ ℕ) ∧ 𝑑 ∈ ℕ) → (𝑎(AP‘0)𝑑) = ∅) |
39 | 36, 38 | eqtrd 2644 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝐾 = 0) ∧ 𝑎 ∈ ℕ) ∧ 𝑑 ∈ ℕ) → (𝑎(AP‘𝐾)𝑑) = ∅) |
40 | | 0ss 3924 |
. . . . . . . . . . . 12
⊢ ∅
⊆ (◡𝐹 “ {𝑐}) |
41 | 39, 40 | syl6eqss 3618 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝐾 = 0) ∧ 𝑎 ∈ ℕ) ∧ 𝑑 ∈ ℕ) → (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑐})) |
42 | 41 | ralrimiva 2949 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐾 = 0) ∧ 𝑎 ∈ ℕ) → ∀𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑐})) |
43 | | r19.2z 4012 |
. . . . . . . . . 10
⊢ ((ℕ
≠ ∅ ∧ ∀𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑐})) → ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑐})) |
44 | 33, 42, 43 | sylancr 694 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐾 = 0) ∧ 𝑎 ∈ ℕ) → ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑐})) |
45 | 44 | ralrimiva 2949 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐾 = 0) → ∀𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑐})) |
46 | | r19.2z 4012 |
. . . . . . . 8
⊢ ((ℕ
≠ ∅ ∧ ∀𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑐})) → ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑐})) |
47 | 33, 45, 46 | sylancr 694 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐾 = 0) → ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑐})) |
48 | 47 | ralrimivw 2950 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐾 = 0) → ∀𝑐 ∈ 𝑅 ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑐})) |
49 | | r19.2z 4012 |
. . . . . 6
⊢ ((𝑅 ≠ ∅ ∧
∀𝑐 ∈ 𝑅 ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑐})) → ∃𝑐 ∈ 𝑅 ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑐})) |
50 | 31, 48, 49 | syl2anc 691 |
. . . . 5
⊢ ((𝜑 ∧ 𝐾 = 0) → ∃𝑐 ∈ 𝑅 ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑐})) |
51 | | rexex 2985 |
. . . . 5
⊢
(∃𝑐 ∈
𝑅 ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑐}) → ∃𝑐∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑐})) |
52 | 50, 51 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝐾 = 0) → ∃𝑐∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑐})) |
53 | 52, 50 | 2thd 254 |
. . 3
⊢ ((𝜑 ∧ 𝐾 = 0) → (∃𝑐∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑐}) ↔ ∃𝑐 ∈ 𝑅 ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑐}))) |
54 | | elnn0 11171 |
. . . 4
⊢ (𝐾 ∈ ℕ0
↔ (𝐾 ∈ ℕ
∨ 𝐾 =
0)) |
55 | 2, 54 | sylib 207 |
. . 3
⊢ (𝜑 → (𝐾 ∈ ℕ ∨ 𝐾 = 0)) |
56 | 26, 53, 55 | mpjaodan 823 |
. 2
⊢ (𝜑 → (∃𝑐∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑐}) ↔ ∃𝑐 ∈ 𝑅 ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑐}))) |
57 | | vdwapval 15515 |
. . . . . . . . 9
⊢ ((𝐾 ∈ ℕ0
∧ 𝑎 ∈ ℕ
∧ 𝑑 ∈ ℕ)
→ (𝑥 ∈ (𝑎(AP‘𝐾)𝑑) ↔ ∃𝑚 ∈ (0...(𝐾 − 1))𝑥 = (𝑎 + (𝑚 · 𝑑)))) |
58 | 57 | 3expb 1258 |
. . . . . . . 8
⊢ ((𝐾 ∈ ℕ0
∧ (𝑎 ∈ ℕ
∧ 𝑑 ∈ ℕ))
→ (𝑥 ∈ (𝑎(AP‘𝐾)𝑑) ↔ ∃𝑚 ∈ (0...(𝐾 − 1))𝑥 = (𝑎 + (𝑚 · 𝑑)))) |
59 | 2, 58 | sylan 487 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ)) → (𝑥 ∈ (𝑎(AP‘𝐾)𝑑) ↔ ∃𝑚 ∈ (0...(𝐾 − 1))𝑥 = (𝑎 + (𝑚 · 𝑑)))) |
60 | 59 | imbi1d 330 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ)) → ((𝑥 ∈ (𝑎(AP‘𝐾)𝑑) → 𝑥 ∈ (◡𝐹 “ {𝑐})) ↔ (∃𝑚 ∈ (0...(𝐾 − 1))𝑥 = (𝑎 + (𝑚 · 𝑑)) → 𝑥 ∈ (◡𝐹 “ {𝑐})))) |
61 | 60 | albidv 1836 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ)) → (∀𝑥(𝑥 ∈ (𝑎(AP‘𝐾)𝑑) → 𝑥 ∈ (◡𝐹 “ {𝑐})) ↔ ∀𝑥(∃𝑚 ∈ (0...(𝐾 − 1))𝑥 = (𝑎 + (𝑚 · 𝑑)) → 𝑥 ∈ (◡𝐹 “ {𝑐})))) |
62 | | dfss2 3557 |
. . . . 5
⊢ ((𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑐}) ↔ ∀𝑥(𝑥 ∈ (𝑎(AP‘𝐾)𝑑) → 𝑥 ∈ (◡𝐹 “ {𝑐}))) |
63 | | ralcom4 3197 |
. . . . . 6
⊢
(∀𝑚 ∈
(0...(𝐾 −
1))∀𝑥(𝑥 = (𝑎 + (𝑚 · 𝑑)) → 𝑥 ∈ (◡𝐹 “ {𝑐})) ↔ ∀𝑥∀𝑚 ∈ (0...(𝐾 − 1))(𝑥 = (𝑎 + (𝑚 · 𝑑)) → 𝑥 ∈ (◡𝐹 “ {𝑐}))) |
64 | | ovex 6577 |
. . . . . . . 8
⊢ (𝑎 + (𝑚 · 𝑑)) ∈ V |
65 | | eleq1 2676 |
. . . . . . . 8
⊢ (𝑥 = (𝑎 + (𝑚 · 𝑑)) → (𝑥 ∈ (◡𝐹 “ {𝑐}) ↔ (𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐}))) |
66 | 64, 65 | ceqsalv 3206 |
. . . . . . 7
⊢
(∀𝑥(𝑥 = (𝑎 + (𝑚 · 𝑑)) → 𝑥 ∈ (◡𝐹 “ {𝑐})) ↔ (𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐})) |
67 | 66 | ralbii 2963 |
. . . . . 6
⊢
(∀𝑚 ∈
(0...(𝐾 −
1))∀𝑥(𝑥 = (𝑎 + (𝑚 · 𝑑)) → 𝑥 ∈ (◡𝐹 “ {𝑐})) ↔ ∀𝑚 ∈ (0...(𝐾 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐})) |
68 | | r19.23v 3005 |
. . . . . . 7
⊢
(∀𝑚 ∈
(0...(𝐾 − 1))(𝑥 = (𝑎 + (𝑚 · 𝑑)) → 𝑥 ∈ (◡𝐹 “ {𝑐})) ↔ (∃𝑚 ∈ (0...(𝐾 − 1))𝑥 = (𝑎 + (𝑚 · 𝑑)) → 𝑥 ∈ (◡𝐹 “ {𝑐}))) |
69 | 68 | albii 1737 |
. . . . . 6
⊢
(∀𝑥∀𝑚 ∈ (0...(𝐾 − 1))(𝑥 = (𝑎 + (𝑚 · 𝑑)) → 𝑥 ∈ (◡𝐹 “ {𝑐})) ↔ ∀𝑥(∃𝑚 ∈ (0...(𝐾 − 1))𝑥 = (𝑎 + (𝑚 · 𝑑)) → 𝑥 ∈ (◡𝐹 “ {𝑐}))) |
70 | 63, 67, 69 | 3bitr3i 289 |
. . . . 5
⊢
(∀𝑚 ∈
(0...(𝐾 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐}) ↔ ∀𝑥(∃𝑚 ∈ (0...(𝐾 − 1))𝑥 = (𝑎 + (𝑚 · 𝑑)) → 𝑥 ∈ (◡𝐹 “ {𝑐}))) |
71 | 61, 62, 70 | 3bitr4g 302 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ)) → ((𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑐}) ↔ ∀𝑚 ∈ (0...(𝐾 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐}))) |
72 | 71 | 2rexbidva 3038 |
. . 3
⊢ (𝜑 → (∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑐}) ↔ ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(𝐾 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐}))) |
73 | 72 | rexbidv 3034 |
. 2
⊢ (𝜑 → (∃𝑐 ∈ 𝑅 ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑐}) ↔ ∃𝑐 ∈ 𝑅 ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(𝐾 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐}))) |
74 | 4, 56, 73 | 3bitrd 293 |
1
⊢ (𝜑 → (𝐾 MonoAP 𝐹 ↔ ∃𝑐 ∈ 𝑅 ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(𝐾 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐}))) |