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		dfss2	⊢ ( ( 𝑎 ( 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 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) ) )