Metamath Proof Explorer

Theorem vdwlem2

Description: Lemma for vdw . (Contributed by Mario Carneiro, 12-Sep-2014)

Ref Expression
Hypotheses vdwlem2.r ⊢ ( 𝜑 → 𝑅 ∈ Fin )
vdwlem2.k ⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
vdwlem2.w ⊢ ( 𝜑 → 𝑊 ∈ ℕ )
vdwlem2.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
vdwlem2.f ⊢ ( 𝜑 → 𝐹 : ( 1 ... 𝑀 ) ⟶ 𝑅 )
vdwlem2.m ⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ ( 𝑊 + 𝑁 ) ) )
vdwlem2.g ⊢ 𝐺 = ( 𝑥 ∈ ( 1 ... 𝑊 ) ↦ ( 𝐹 ‘ ( 𝑥 + 𝑁 ) ) )
Assertion vdwlem2 ( 𝜑 → ( 𝐾 MonoAP 𝐺 → 𝐾 MonoAP 𝐹 ) )

Proof

Step Hyp Ref Expression
1 vdwlem2.r ⊢ ( 𝜑 → 𝑅 ∈ Fin )
2 vdwlem2.k ⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
3 vdwlem2.w ⊢ ( 𝜑 → 𝑊 ∈ ℕ )
4 vdwlem2.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
5 vdwlem2.f ⊢ ( 𝜑 → 𝐹 : ( 1 ... 𝑀 ) ⟶ 𝑅 )
6 vdwlem2.m ⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ ( 𝑊 + 𝑁 ) ) )
7 vdwlem2.g ⊢ 𝐺 = ( 𝑥 ∈ ( 1 ... 𝑊 ) ↦ ( 𝐹 ‘ ( 𝑥 + 𝑁 ) ) )
8 id ⊢ ( 𝑎 ∈ ℕ → 𝑎 ∈ ℕ )
9 nnaddcl ⊢ ( ( 𝑎 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝑎 + 𝑁 ) ∈ ℕ )
10 8 4 9 syl2anr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℕ ) → ( 𝑎 + 𝑁 ) ∈ ℕ )
11 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ ) ∧ ( 𝑑 ∈ ℕ ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐺 “ { 𝑐 } ) ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → 𝑎 ∈ ℕ )
12 11 nncnd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ ) ∧ ( 𝑑 ∈ ℕ ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐺 “ { 𝑐 } ) ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → 𝑎 ∈ ℂ )
13 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ ) ∧ ( 𝑑 ∈ ℕ ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐺 “ { 𝑐 } ) ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → 𝑁 ∈ ℕ )
14 13 nncnd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ ) ∧ ( 𝑑 ∈ ℕ ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐺 “ { 𝑐 } ) ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → 𝑁 ∈ ℂ )
15 elfznn0 ⊢ ( 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) → 𝑚 ∈ ℕ0 )
16 15 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ ) ∧ ( 𝑑 ∈ ℕ ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐺 “ { 𝑐 } ) ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → 𝑚 ∈ ℕ0 )
17 16 nn0cnd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ ) ∧ ( 𝑑 ∈ ℕ ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐺 “ { 𝑐 } ) ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → 𝑚 ∈ ℂ )
18 simplrl ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ ) ∧ ( 𝑑 ∈ ℕ ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐺 “ { 𝑐 } ) ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → 𝑑 ∈ ℕ )
19 18 nncnd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ ) ∧ ( 𝑑 ∈ ℕ ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐺 “ { 𝑐 } ) ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → 𝑑 ∈ ℂ )
20 17 19 mulcld ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ ) ∧ ( 𝑑 ∈ ℕ ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐺 “ { 𝑐 } ) ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → ( 𝑚 · 𝑑 ) ∈ ℂ )
21 12 14 20 add32d ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ ) ∧ ( 𝑑 ∈ ℕ ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐺 “ { 𝑐 } ) ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → ( ( 𝑎 + 𝑁 ) + ( 𝑚 · 𝑑 ) ) = ( ( 𝑎 + ( 𝑚 · 𝑑 ) ) + 𝑁 ) )
22 oveq1 ⊢ ( 𝑥 = ( 𝑎 + ( 𝑚 · 𝑑 ) ) → ( 𝑥 + 𝑁 ) = ( ( 𝑎 + ( 𝑚 · 𝑑 ) ) + 𝑁 ) )
23 22 eleq1d ⊢ ( 𝑥 = ( 𝑎 + ( 𝑚 · 𝑑 ) ) → ( ( 𝑥 + 𝑁 ) ∈ ( 1 ... 𝑀 ) ↔ ( ( 𝑎 + ( 𝑚 · 𝑑 ) ) + 𝑁 ) ∈ ( 1 ... 𝑀 ) ) )
24 elfznn ⊢ ( 𝑥 ∈ ( 1 ... 𝑊 ) → 𝑥 ∈ ℕ )
25 nnaddcl ⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝑥 + 𝑁 ) ∈ ℕ )
26 24 4 25 syl2anr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑊 ) ) → ( 𝑥 + 𝑁 ) ∈ ℕ )
27 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
28 26 27 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑊 ) ) → ( 𝑥 + 𝑁 ) ∈ ( ℤ≥ ‘ 1 ) )
29 elfzuz3 ⊢ ( 𝑥 ∈ ( 1 ... 𝑊 ) → 𝑊 ∈ ( ℤ≥ ‘ 𝑥 ) )
30 4 nnzd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
31 eluzadd ⊢ ( ( 𝑊 ∈ ( ℤ≥ ‘ 𝑥 ) ∧ 𝑁 ∈ ℤ ) → ( 𝑊 + 𝑁 ) ∈ ( ℤ≥ ‘ ( 𝑥 + 𝑁 ) ) )
32 29 30 31 syl2anr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑊 ) ) → ( 𝑊 + 𝑁 ) ∈ ( ℤ≥ ‘ ( 𝑥 + 𝑁 ) ) )
33 uztrn ⊢ ( ( 𝑀 ∈ ( ℤ≥ ‘ ( 𝑊 + 𝑁 ) ) ∧ ( 𝑊 + 𝑁 ) ∈ ( ℤ≥ ‘ ( 𝑥 + 𝑁 ) ) ) → 𝑀 ∈ ( ℤ≥ ‘ ( 𝑥 + 𝑁 ) ) )
34 6 32 33 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑊 ) ) → 𝑀 ∈ ( ℤ≥ ‘ ( 𝑥 + 𝑁 ) ) )
35 elfzuzb ⊢ ( ( 𝑥 + 𝑁 ) ∈ ( 1 ... 𝑀 ) ↔ ( ( 𝑥 + 𝑁 ) ∈ ( ℤ≥ ‘ 1 ) ∧ 𝑀 ∈ ( ℤ≥ ‘ ( 𝑥 + 𝑁 ) ) ) )
36 28 34 35 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑊 ) ) → ( 𝑥 + 𝑁 ) ∈ ( 1 ... 𝑀 ) )
37 36 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 1 ... 𝑊 ) ( 𝑥 + 𝑁 ) ∈ ( 1 ... 𝑀 ) )
38 37 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ ) ∧ ( 𝑑 ∈ ℕ ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐺 “ { 𝑐 } ) ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → ∀ 𝑥 ∈ ( 1 ... 𝑊 ) ( 𝑥 + 𝑁 ) ∈ ( 1 ... 𝑀 ) )
39 simplrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ ) ∧ ( 𝑑 ∈ ℕ ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐺 “ { 𝑐 } ) ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐺 “ { 𝑐 } ) )
40 eqid ⊢ ( 𝑎 + ( 𝑚 · 𝑑 ) ) = ( 𝑎 + ( 𝑚 · 𝑑 ) )
41 oveq1 ⊢ ( 𝑛 = 𝑚 → ( 𝑛 · 𝑑 ) = ( 𝑚 · 𝑑 ) )
42 41 oveq2d ⊢ ( 𝑛 = 𝑚 → ( 𝑎 + ( 𝑛 · 𝑑 ) ) = ( 𝑎 + ( 𝑚 · 𝑑 ) ) )
43 42 rspceeqv ⊢ ( ( 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ∧ ( 𝑎 + ( 𝑚 · 𝑑 ) ) = ( 𝑎 + ( 𝑚 · 𝑑 ) ) ) → ∃ 𝑛 ∈ ( 0 ... ( 𝐾 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) = ( 𝑎 + ( 𝑛 · 𝑑 ) ) )
44 40 43 mpan2 ⊢ ( 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) → ∃ 𝑛 ∈ ( 0 ... ( 𝐾 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) = ( 𝑎 + ( 𝑛 · 𝑑 ) ) )
45 44 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ ) ∧ ( 𝑑 ∈ ℕ ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐺 “ { 𝑐 } ) ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → ∃ 𝑛 ∈ ( 0 ... ( 𝐾 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) = ( 𝑎 + ( 𝑛 · 𝑑 ) ) )
46 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ ) ∧ ( 𝑑 ∈ ℕ ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐺 “ { 𝑐 } ) ) ) → 𝐾 ∈ ℕ0 )
47 46 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ ) ∧ ( 𝑑 ∈ ℕ ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐺 “ { 𝑐 } ) ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → 𝐾 ∈ ℕ0 )
48 vdwapval ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) → ( ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ↔ ∃ 𝑛 ∈ ( 0 ... ( 𝐾 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) = ( 𝑎 + ( 𝑛 · 𝑑 ) ) ) )
49 47 11 18 48 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ ) ∧ ( 𝑑 ∈ ℕ ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐺 “ { 𝑐 } ) ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → ( ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ↔ ∃ 𝑛 ∈ ( 0 ... ( 𝐾 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) = ( 𝑎 + ( 𝑛 · 𝑑 ) ) ) )
50 45 49 mpbird ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ ) ∧ ( 𝑑 ∈ ℕ ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐺 “ { 𝑐 } ) ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) )
51 39 50 sseldd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ ) ∧ ( 𝑑 ∈ ℕ ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐺 “ { 𝑐 } ) ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐺 “ { 𝑐 } ) )
52 5 ffvelrnda ⊢ ( ( 𝜑 ∧ ( 𝑥 + 𝑁 ) ∈ ( 1 ... 𝑀 ) ) → ( 𝐹 ‘ ( 𝑥 + 𝑁 ) ) ∈ 𝑅 )
53 36 52 syldan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑊 ) ) → ( 𝐹 ‘ ( 𝑥 + 𝑁 ) ) ∈ 𝑅 )
54 53 7 fmptd ⊢ ( 𝜑 → 𝐺 : ( 1 ... 𝑊 ) ⟶ 𝑅 )
55 54 ffnd ⊢ ( 𝜑 → 𝐺 Fn ( 1 ... 𝑊 ) )
56 55 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ ) ∧ ( 𝑑 ∈ ℕ ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐺 “ { 𝑐 } ) ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → 𝐺 Fn ( 1 ... 𝑊 ) )
57 fniniseg ⊢ ( 𝐺 Fn ( 1 ... 𝑊 ) → ( ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐺 “ { 𝑐 } ) ↔ ( ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( 1 ... 𝑊 ) ∧ ( 𝐺 ‘ ( 𝑎 + ( 𝑚 · 𝑑 ) ) ) = 𝑐 ) ) )
58 56 57 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ ) ∧ ( 𝑑 ∈ ℕ ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐺 “ { 𝑐 } ) ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → ( ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐺 “ { 𝑐 } ) ↔ ( ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( 1 ... 𝑊 ) ∧ ( 𝐺 ‘ ( 𝑎 + ( 𝑚 · 𝑑 ) ) ) = 𝑐 ) ) )
59 51 58 mpbid ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ ) ∧ ( 𝑑 ∈ ℕ ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐺 “ { 𝑐 } ) ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → ( ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( 1 ... 𝑊 ) ∧ ( 𝐺 ‘ ( 𝑎 + ( 𝑚 · 𝑑 ) ) ) = 𝑐 ) )
60 59 simpld ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ ) ∧ ( 𝑑 ∈ ℕ ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐺 “ { 𝑐 } ) ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( 1 ... 𝑊 ) )
61 23 38 60 rspcdva ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ ) ∧ ( 𝑑 ∈ ℕ ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐺 “ { 𝑐 } ) ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → ( ( 𝑎 + ( 𝑚 · 𝑑 ) ) + 𝑁 ) ∈ ( 1 ... 𝑀 ) )
62 21 61 eqeltrd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ ) ∧ ( 𝑑 ∈ ℕ ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐺 “ { 𝑐 } ) ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → ( ( 𝑎 + 𝑁 ) + ( 𝑚 · 𝑑 ) ) ∈ ( 1 ... 𝑀 ) )
63 21 fveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ ) ∧ ( 𝑑 ∈ ℕ ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐺 “ { 𝑐 } ) ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → ( 𝐹 ‘ ( ( 𝑎 + 𝑁 ) + ( 𝑚 · 𝑑 ) ) ) = ( 𝐹 ‘ ( ( 𝑎 + ( 𝑚 · 𝑑 ) ) + 𝑁 ) ) )
64 22 fveq2d ⊢ ( 𝑥 = ( 𝑎 + ( 𝑚 · 𝑑 ) ) → ( 𝐹 ‘ ( 𝑥 + 𝑁 ) ) = ( 𝐹 ‘ ( ( 𝑎 + ( 𝑚 · 𝑑 ) ) + 𝑁 ) ) )
65 fvex ⊢ ( 𝐹 ‘ ( ( 𝑎 + ( 𝑚 · 𝑑 ) ) + 𝑁 ) ) ∈ V
66 64 7 65 fvmpt ⊢ ( ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( 1 ... 𝑊 ) → ( 𝐺 ‘ ( 𝑎 + ( 𝑚 · 𝑑 ) ) ) = ( 𝐹 ‘ ( ( 𝑎 + ( 𝑚 · 𝑑 ) ) + 𝑁 ) ) )
67 60 66 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ ) ∧ ( 𝑑 ∈ ℕ ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐺 “ { 𝑐 } ) ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → ( 𝐺 ‘ ( 𝑎 + ( 𝑚 · 𝑑 ) ) ) = ( 𝐹 ‘ ( ( 𝑎 + ( 𝑚 · 𝑑 ) ) + 𝑁 ) ) )
68 59 simprd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ ) ∧ ( 𝑑 ∈ ℕ ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐺 “ { 𝑐 } ) ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → ( 𝐺 ‘ ( 𝑎 + ( 𝑚 · 𝑑 ) ) ) = 𝑐 )
69 63 67 68 3eqtr2d ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ ) ∧ ( 𝑑 ∈ ℕ ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐺 “ { 𝑐 } ) ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → ( 𝐹 ‘ ( ( 𝑎 + 𝑁 ) + ( 𝑚 · 𝑑 ) ) ) = 𝑐 )
70 62 69 jca ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ ) ∧ ( 𝑑 ∈ ℕ ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐺 “ { 𝑐 } ) ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → ( ( ( 𝑎 + 𝑁 ) + ( 𝑚 · 𝑑 ) ) ∈ ( 1 ... 𝑀 ) ∧ ( 𝐹 ‘ ( ( 𝑎 + 𝑁 ) + ( 𝑚 · 𝑑 ) ) ) = 𝑐 ) )
71 eleq1 ⊢ ( 𝑥 = ( ( 𝑎 + 𝑁 ) + ( 𝑚 · 𝑑 ) ) → ( 𝑥 ∈ ( 1 ... 𝑀 ) ↔ ( ( 𝑎 + 𝑁 ) + ( 𝑚 · 𝑑 ) ) ∈ ( 1 ... 𝑀 ) ) )
72 fveqeq2 ⊢ ( 𝑥 = ( ( 𝑎 + 𝑁 ) + ( 𝑚 · 𝑑 ) ) → ( ( 𝐹 ‘ 𝑥 ) = 𝑐 ↔ ( 𝐹 ‘ ( ( 𝑎 + 𝑁 ) + ( 𝑚 · 𝑑 ) ) ) = 𝑐 ) )
73 71 72 anbi12d ⊢ ( 𝑥 = ( ( 𝑎 + 𝑁 ) + ( 𝑚 · 𝑑 ) ) → ( ( 𝑥 ∈ ( 1 ... 𝑀 ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑐 ) ↔ ( ( ( 𝑎 + 𝑁 ) + ( 𝑚 · 𝑑 ) ) ∈ ( 1 ... 𝑀 ) ∧ ( 𝐹 ‘ ( ( 𝑎 + 𝑁 ) + ( 𝑚 · 𝑑 ) ) ) = 𝑐 ) ) )
74 70 73 syl5ibrcom ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ ) ∧ ( 𝑑 ∈ ℕ ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐺 “ { 𝑐 } ) ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → ( 𝑥 = ( ( 𝑎 + 𝑁 ) + ( 𝑚 · 𝑑 ) ) → ( 𝑥 ∈ ( 1 ... 𝑀 ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑐 ) ) )
75 74 rexlimdva ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ ) ∧ ( 𝑑 ∈ ℕ ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐺 “ { 𝑐 } ) ) ) → ( ∃ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) 𝑥 = ( ( 𝑎 + 𝑁 ) + ( 𝑚 · 𝑑 ) ) → ( 𝑥 ∈ ( 1 ... 𝑀 ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑐 ) ) )
76 10 adantr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ ) ∧ ( 𝑑 ∈ ℕ ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐺 “ { 𝑐 } ) ) ) → ( 𝑎 + 𝑁 ) ∈ ℕ )
77 simprl ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ ) ∧ ( 𝑑 ∈ ℕ ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐺 “ { 𝑐 } ) ) ) → 𝑑 ∈ ℕ )
78 vdwapval ⊢ ( ( 𝐾 ∈ ℕ0 ∧ ( 𝑎 + 𝑁 ) ∈ ℕ ∧ 𝑑 ∈ ℕ ) → ( 𝑥 ∈ ( ( 𝑎 + 𝑁 ) ( AP ‘ 𝐾 ) 𝑑 ) ↔ ∃ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) 𝑥 = ( ( 𝑎 + 𝑁 ) + ( 𝑚 · 𝑑 ) ) ) )
79 46 76 77 78 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ ) ∧ ( 𝑑 ∈ ℕ ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐺 “ { 𝑐 } ) ) ) → ( 𝑥 ∈ ( ( 𝑎 + 𝑁 ) ( AP ‘ 𝐾 ) 𝑑 ) ↔ ∃ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) 𝑥 = ( ( 𝑎 + 𝑁 ) + ( 𝑚 · 𝑑 ) ) ) )
80 5 ffnd ⊢ ( 𝜑 → 𝐹 Fn ( 1 ... 𝑀 ) )
81 80 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ ) ∧ ( 𝑑 ∈ ℕ ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐺 “ { 𝑐 } ) ) ) → 𝐹 Fn ( 1 ... 𝑀 ) )
82 fniniseg ⊢ ( 𝐹 Fn ( 1 ... 𝑀 ) → ( 𝑥 ∈ ( ◡ 𝐹 “ { 𝑐 } ) ↔ ( 𝑥 ∈ ( 1 ... 𝑀 ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑐 ) ) )
83 81 82 syl ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ ) ∧ ( 𝑑 ∈ ℕ ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐺 “ { 𝑐 } ) ) ) → ( 𝑥 ∈ ( ◡ 𝐹 “ { 𝑐 } ) ↔ ( 𝑥 ∈ ( 1 ... 𝑀 ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑐 ) ) )
84 75 79 83 3imtr4d ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ ) ∧ ( 𝑑 ∈ ℕ ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐺 “ { 𝑐 } ) ) ) → ( 𝑥 ∈ ( ( 𝑎 + 𝑁 ) ( AP ‘ 𝐾 ) 𝑑 ) → 𝑥 ∈ ( ◡ 𝐹 “ { 𝑐 } ) ) )
85 84 ssrdv ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ ) ∧ ( 𝑑 ∈ ℕ ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐺 “ { 𝑐 } ) ) ) → ( ( 𝑎 + 𝑁 ) ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑐 } ) )
86 85 expr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ ) ∧ 𝑑 ∈ ℕ ) → ( ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐺 “ { 𝑐 } ) → ( ( 𝑎 + 𝑁 ) ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑐 } ) ) )
87 86 reximdva ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℕ ) → ( ∃ 𝑑 ∈ ℕ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐺 “ { 𝑐 } ) → ∃ 𝑑 ∈ ℕ ( ( 𝑎 + 𝑁 ) ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑐 } ) ) )
88 oveq1 ⊢ ( 𝑏 = ( 𝑎 + 𝑁 ) → ( 𝑏 ( AP ‘ 𝐾 ) 𝑑 ) = ( ( 𝑎 + 𝑁 ) ( AP ‘ 𝐾 ) 𝑑 ) )
89 88 sseq1d ⊢ ( 𝑏 = ( 𝑎 + 𝑁 ) → ( ( 𝑏 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑐 } ) ↔ ( ( 𝑎 + 𝑁 ) ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑐 } ) ) )
90 89 rexbidv ⊢ ( 𝑏 = ( 𝑎 + 𝑁 ) → ( ∃ 𝑑 ∈ ℕ ( 𝑏 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑐 } ) ↔ ∃ 𝑑 ∈ ℕ ( ( 𝑎 + 𝑁 ) ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑐 } ) ) )
91 90 rspcev ⊢ ( ( ( 𝑎 + 𝑁 ) ∈ ℕ ∧ ∃ 𝑑 ∈ ℕ ( ( 𝑎 + 𝑁 ) ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑐 } ) ) → ∃ 𝑏 ∈ ℕ ∃ 𝑑 ∈ ℕ ( 𝑏 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑐 } ) )
92 10 87 91 syl6an ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℕ ) → ( ∃ 𝑑 ∈ ℕ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐺 “ { 𝑐 } ) → ∃ 𝑏 ∈ ℕ ∃ 𝑑 ∈ ℕ ( 𝑏 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑐 } ) ) )
93 92 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐺 “ { 𝑐 } ) → ∃ 𝑏 ∈ ℕ ∃ 𝑑 ∈ ℕ ( 𝑏 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑐 } ) ) )
94 93 eximdv ⊢ ( 𝜑 → ( ∃ 𝑐 ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐺 “ { 𝑐 } ) → ∃ 𝑐 ∃ 𝑏 ∈ ℕ ∃ 𝑑 ∈ ℕ ( 𝑏 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑐 } ) ) )
95 ovex ⊢ ( 1 ... 𝑊 ) ∈ V
96 95 2 54 vdwmc ⊢ ( 𝜑 → ( 𝐾 MonoAP 𝐺 ↔ ∃ 𝑐 ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐺 “ { 𝑐 } ) ) )
97 ovex ⊢ ( 1 ... 𝑀 ) ∈ V
98 97 2 5 vdwmc ⊢ ( 𝜑 → ( 𝐾 MonoAP 𝐹 ↔ ∃ 𝑐 ∃ 𝑏 ∈ ℕ ∃ 𝑑 ∈ ℕ ( 𝑏 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑐 } ) ) )
99 94 96 98 3imtr4d ⊢ ( 𝜑 → ( 𝐾 MonoAP 𝐺 → 𝐾 MonoAP 𝐹 ) )