Metamath Proof Explorer

Theorem vdwmc2

Description: Expand out the definition of an arithmetic progression. (Contributed by Mario Carneiro, 18-Aug-2014)

Ref Expression
Hypotheses vdwmc.1 ⊢ 𝑋 ∈ V
vdwmc.2 ⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
vdwmc.3 ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ 𝑅 )
vdwmc2.4 ⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
Assertion vdwmc2 ( 𝜑 → ( 𝐾 MonoAP 𝐹 ↔ ∃ 𝑐 ∈ 𝑅 ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) ) )

Proof

Step Hyp Ref Expression
1 vdwmc.1 ⊢ 𝑋 ∈ V
2 vdwmc.2 ⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
3 vdwmc.3 ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ 𝑅 )
4 vdwmc2.4 ⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
5 1 2 3 vdwmc ⊢ ( 𝜑 → ( 𝐾 MonoAP 𝐹 ↔ ∃ 𝑐 ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑐 } ) ) )
6 vdwapid1 ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) → 𝑎 ∈ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) )
7 6 ne0d ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) → ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ≠ ∅ )
8 7 3expb ⊢ ( ( 𝐾 ∈ ℕ ∧ ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ) → ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ≠ ∅ )
9 8 adantll ⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ ℕ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ) → ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ≠ ∅ )
10 ssn0 ⊢ ( ( ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑐 } ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ≠ ∅ ) → ( ◡ 𝐹 “ { 𝑐 } ) ≠ ∅ )
11 10 expcom ⊢ ( ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ≠ ∅ → ( ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑐 } ) → ( ◡ 𝐹 “ { 𝑐 } ) ≠ ∅ ) )
12 9 11 syl ⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ ℕ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ) → ( ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑐 } ) → ( ◡ 𝐹 “ { 𝑐 } ) ≠ ∅ ) )
13 disjsn ⊢ ( ( 𝑅 ∩ { 𝑐 } ) = ∅ ↔ ¬ 𝑐 ∈ 𝑅 )
14 3 adantr ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ℕ ) → 𝐹 : 𝑋 ⟶ 𝑅 )
15 fimacnvdisj ⊢ ( ( 𝐹 : 𝑋 ⟶ 𝑅 ∧ ( 𝑅 ∩ { 𝑐 } ) = ∅ ) → ( ◡ 𝐹 “ { 𝑐 } ) = ∅ )
16 15 ex ⊢ ( 𝐹 : 𝑋 ⟶ 𝑅 → ( ( 𝑅 ∩ { 𝑐 } ) = ∅ → ( ◡ 𝐹 “ { 𝑐 } ) = ∅ ) )
17 14 16 syl ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ℕ ) → ( ( 𝑅 ∩ { 𝑐 } ) = ∅ → ( ◡ 𝐹 “ { 𝑐 } ) = ∅ ) )
18 17 adantr ⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ ℕ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ) → ( ( 𝑅 ∩ { 𝑐 } ) = ∅ → ( ◡ 𝐹 “ { 𝑐 } ) = ∅ ) )
19 13 18 biimtrrid ⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ ℕ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ) → ( ¬ 𝑐 ∈ 𝑅 → ( ◡ 𝐹 “ { 𝑐 } ) = ∅ ) )
20 19 necon1ad ⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ ℕ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ) → ( ( ◡ 𝐹 “ { 𝑐 } ) ≠ ∅ → 𝑐 ∈ 𝑅 ) )
21 12 20 syld ⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ ℕ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ) → ( ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑐 } ) → 𝑐 ∈ 𝑅 ) )
22 21 rexlimdvva ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ℕ ) → ( ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑐 } ) → 𝑐 ∈ 𝑅 ) )
23 22 pm4.71rd ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ℕ ) → ( ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑐 } ) ↔ ( 𝑐 ∈ 𝑅 ∧ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑐 } ) ) ) )
24 23 exbidv ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ℕ ) → ( ∃ 𝑐 ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑐 } ) ↔ ∃ 𝑐 ( 𝑐 ∈ 𝑅 ∧ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑐 } ) ) ) )
25 df-rex ⊢ ( ∃ 𝑐 ∈ 𝑅 ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑐 } ) ↔ ∃ 𝑐 ( 𝑐 ∈ 𝑅 ∧ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑐 } ) ) )
26 24 25 bitr4di ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ℕ ) → ( ∃ 𝑐 ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑐 } ) ↔ ∃ 𝑐 ∈ 𝑅 ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑐 } ) ) )
27 3 4 ffvelcdmd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) ∈ 𝑅 )
28 27 ne0d ⊢ ( 𝜑 → 𝑅 ≠ ∅ )
29 1nn ⊢ 1 ∈ ℕ
30 29 ne0ii ⊢ ℕ ≠ ∅
31 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝐾 = 0 ) ∧ 𝑎 ∈ ℕ ) ∧ 𝑑 ∈ ℕ ) → 𝐾 = 0 )
32 31 fveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝐾 = 0 ) ∧ 𝑎 ∈ ℕ ) ∧ 𝑑 ∈ ℕ ) → ( AP ‘ 𝐾 ) = ( AP ‘ 0 ) )
33 32 oveqd ⊢ ( ( ( ( 𝜑 ∧ 𝐾 = 0 ) ∧ 𝑎 ∈ ℕ ) ∧ 𝑑 ∈ ℕ ) → ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) = ( 𝑎 ( AP ‘ 0 ) 𝑑 ) )
34 vdwap0 ⊢ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) → ( 𝑎 ( AP ‘ 0 ) 𝑑 ) = ∅ )
35 34 adantll ⊢ ( ( ( ( 𝜑 ∧ 𝐾 = 0 ) ∧ 𝑎 ∈ ℕ ) ∧ 𝑑 ∈ ℕ ) → ( 𝑎 ( AP ‘ 0 ) 𝑑 ) = ∅ )
36 33 35 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝐾 = 0 ) ∧ 𝑎 ∈ ℕ ) ∧ 𝑑 ∈ ℕ ) → ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) = ∅ )
37 0ss ⊢ ∅ ⊆ ( ◡ 𝐹 “ { 𝑐 } )
38 36 37 eqsstrdi ⊢ ( ( ( ( 𝜑 ∧ 𝐾 = 0 ) ∧ 𝑎 ∈ ℕ ) ∧ 𝑑 ∈ ℕ ) → ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑐 } ) )
39 38 ralrimiva ⊢ ( ( ( 𝜑 ∧ 𝐾 = 0 ) ∧ 𝑎 ∈ ℕ ) → ∀ 𝑑 ∈ ℕ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑐 } ) )
40 r19.2z ⊢ ( ( ℕ ≠ ∅ ∧ ∀ 𝑑 ∈ ℕ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑐 } ) ) → ∃ 𝑑 ∈ ℕ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑐 } ) )
41 30 39 40 sylancr ⊢ ( ( ( 𝜑 ∧ 𝐾 = 0 ) ∧ 𝑎 ∈ ℕ ) → ∃ 𝑑 ∈ ℕ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑐 } ) )
42 41 ralrimiva ⊢ ( ( 𝜑 ∧ 𝐾 = 0 ) → ∀ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑐 } ) )
43 r19.2z ⊢ ( ( ℕ ≠ ∅ ∧ ∀ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑐 } ) ) → ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑐 } ) )
44 30 42 43 sylancr ⊢ ( ( 𝜑 ∧ 𝐾 = 0 ) → ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑐 } ) )
45 44 ralrimivw ⊢ ( ( 𝜑 ∧ 𝐾 = 0 ) → ∀ 𝑐 ∈ 𝑅 ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑐 } ) )
46 r19.2z ⊢ ( ( 𝑅 ≠ ∅ ∧ ∀ 𝑐 ∈ 𝑅 ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑐 } ) ) → ∃ 𝑐 ∈ 𝑅 ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑐 } ) )
47 28 45 46 syl2an2r ⊢ ( ( 𝜑 ∧ 𝐾 = 0 ) → ∃ 𝑐 ∈ 𝑅 ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑐 } ) )
48 rexex ⊢ ( ∃ 𝑐 ∈ 𝑅 ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑐 } ) → ∃ 𝑐 ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑐 } ) )
49 47 48 syl ⊢ ( ( 𝜑 ∧ 𝐾 = 0 ) → ∃ 𝑐 ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑐 } ) )
50 49 47 2thd ⊢ ( ( 𝜑 ∧ 𝐾 = 0 ) → ( ∃ 𝑐 ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑐 } ) ↔ ∃ 𝑐 ∈ 𝑅 ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑐 } ) ) )
51 elnn0 ⊢ ( 𝐾 ∈ ℕ0 ↔ ( 𝐾 ∈ ℕ ∨ 𝐾 = 0 ) )
52 2 51 sylib ⊢ ( 𝜑 → ( 𝐾 ∈ ℕ ∨ 𝐾 = 0 ) )
53 26 50 52 mpjaodan ⊢ ( 𝜑 → ( ∃ 𝑐 ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑐 } ) ↔ ∃ 𝑐 ∈ 𝑅 ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑐 } ) ) )
54 vdwapval ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) → ( 𝑥 ∈ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ↔ ∃ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) 𝑥 = ( 𝑎 + ( 𝑚 · 𝑑 ) ) ) )
55 54 3expb ⊢ ( ( 𝐾 ∈ ℕ0 ∧ ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ) → ( 𝑥 ∈ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ↔ ∃ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) 𝑥 = ( 𝑎 + ( 𝑚 · 𝑑 ) ) ) )
56 2 55 sylan ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ) → ( 𝑥 ∈ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ↔ ∃ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) 𝑥 = ( 𝑎 + ( 𝑚 · 𝑑 ) ) ) )
57 56 imbi1d ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ) → ( ( 𝑥 ∈ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) → 𝑥 ∈ ( ◡ 𝐹 “ { 𝑐 } ) ) ↔ ( ∃ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) 𝑥 = ( 𝑎 + ( 𝑚 · 𝑑 ) ) → 𝑥 ∈ ( ◡ 𝐹 “ { 𝑐 } ) ) ) )
58 57 albidv ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ) → ( ∀ 𝑥 ( 𝑥 ∈ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) → 𝑥 ∈ ( ◡ 𝐹 “ { 𝑐 } ) ) ↔ ∀ 𝑥 ( ∃ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) 𝑥 = ( 𝑎 + ( 𝑚 · 𝑑 ) ) → 𝑥 ∈ ( ◡ 𝐹 “ { 𝑐 } ) ) ) )
59 df-ss ⊢ ( ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑐 } ) ↔ ∀ 𝑥 ( 𝑥 ∈ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) → 𝑥 ∈ ( ◡ 𝐹 “ { 𝑐 } ) ) )
60 ralcom4 ⊢ ( ∀ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ∀ 𝑥 ( 𝑥 = ( 𝑎 + ( 𝑚 · 𝑑 ) ) → 𝑥 ∈ ( ◡ 𝐹 “ { 𝑐 } ) ) ↔ ∀ 𝑥 ∀ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ( 𝑥 = ( 𝑎 + ( 𝑚 · 𝑑 ) ) → 𝑥 ∈ ( ◡ 𝐹 “ { 𝑐 } ) ) )
61 ovex ⊢ ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ V
62 eleq1 ⊢ ( 𝑥 = ( 𝑎 + ( 𝑚 · 𝑑 ) ) → ( 𝑥 ∈ ( ◡ 𝐹 “ { 𝑐 } ) ↔ ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) ) )
63 61 62 ceqsalv ⊢ ( ∀ 𝑥 ( 𝑥 = ( 𝑎 + ( 𝑚 · 𝑑 ) ) → 𝑥 ∈ ( ◡ 𝐹 “ { 𝑐 } ) ) ↔ ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) )
64 63 ralbii ⊢ ( ∀ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ∀ 𝑥 ( 𝑥 = ( 𝑎 + ( 𝑚 · 𝑑 ) ) → 𝑥 ∈ ( ◡ 𝐹 “ { 𝑐 } ) ) ↔ ∀ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) )
65 r19.23v ⊢ ( ∀ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ( 𝑥 = ( 𝑎 + ( 𝑚 · 𝑑 ) ) → 𝑥 ∈ ( ◡ 𝐹 “ { 𝑐 } ) ) ↔ ( ∃ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) 𝑥 = ( 𝑎 + ( 𝑚 · 𝑑 ) ) → 𝑥 ∈ ( ◡ 𝐹 “ { 𝑐 } ) ) )
66 65 albii ⊢ ( ∀ 𝑥 ∀ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ( 𝑥 = ( 𝑎 + ( 𝑚 · 𝑑 ) ) → 𝑥 ∈ ( ◡ 𝐹 “ { 𝑐 } ) ) ↔ ∀ 𝑥 ( ∃ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) 𝑥 = ( 𝑎 + ( 𝑚 · 𝑑 ) ) → 𝑥 ∈ ( ◡ 𝐹 “ { 𝑐 } ) ) )
67 60 64 66 3bitr3i ⊢ ( ∀ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) ↔ ∀ 𝑥 ( ∃ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) 𝑥 = ( 𝑎 + ( 𝑚 · 𝑑 ) ) → 𝑥 ∈ ( ◡ 𝐹 “ { 𝑐 } ) ) )
68 58 59 67 3bitr4g ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ) → ( ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑐 } ) ↔ ∀ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) ) )
69 68 2rexbidva ⊢ ( 𝜑 → ( ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑐 } ) ↔ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) ) )
70 69 rexbidv ⊢ ( 𝜑 → ( ∃ 𝑐 ∈ 𝑅 ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑐 } ) ↔ ∃ 𝑐 ∈ 𝑅 ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) ) )
71 5 53 70 3bitrd ⊢ ( 𝜑 → ( 𝐾 MonoAP 𝐹 ↔ ∃ 𝑐 ∈ 𝑅 ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) ) )