Metamath Proof Explorer

Theorem vdwlem11

Description: Lemma for vdw . (Contributed by Mario Carneiro, 18-Aug-2014)

Ref Expression
Hypotheses vdw.r ⊢ ( 𝜑 → 𝑅 ∈ Fin )
vdwlem9.k ⊢ ( 𝜑 → 𝐾 ∈ ( ℤ≥ ‘ 2 ) )
vdwlem9.s ⊢ ( 𝜑 → ∀ 𝑠 ∈ Fin ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑠 ↑m ( 1 ... 𝑛 ) ) 𝐾 MonoAP 𝑓 )
Assertion vdwlem11 ( 𝜑 → ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) ( 𝐾 + 1 ) MonoAP 𝑓 )

Proof

Step Hyp Ref Expression
1 vdw.r ⊢ ( 𝜑 → 𝑅 ∈ Fin )
2 vdwlem9.k ⊢ ( 𝜑 → 𝐾 ∈ ( ℤ≥ ‘ 2 ) )
3 vdwlem9.s ⊢ ( 𝜑 → ∀ 𝑠 ∈ Fin ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑠 ↑m ( 1 ... 𝑛 ) ) 𝐾 MonoAP 𝑓 )
4 hashcl ⊢ ( 𝑅 ∈ Fin → ( ♯ ‘ 𝑅 ) ∈ ℕ0 )
5 1 4 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝑅 ) ∈ ℕ0 )
6 nn0p1nn ⊢ ( ( ♯ ‘ 𝑅 ) ∈ ℕ0 → ( ( ♯ ‘ 𝑅 ) + 1 ) ∈ ℕ )
7 5 6 syl ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑅 ) + 1 ) ∈ ℕ )
8 1 2 3 7 vdwlem10 ⊢ ( 𝜑 → ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) ( ⟨ ( ( ♯ ‘ 𝑅 ) + 1 ) , 𝐾 ⟩ PolyAP 𝑓 ∨ ( 𝐾 + 1 ) MonoAP 𝑓 ) )
9 1 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑅 ∈ Fin )
10 ovex ⊢ ( 1 ... 𝑛 ) ∈ V
11 elmapg ⊢ ( ( 𝑅 ∈ Fin ∧ ( 1 ... 𝑛 ) ∈ V ) → ( 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) ↔ 𝑓 : ( 1 ... 𝑛 ) ⟶ 𝑅 ) )
12 9 10 11 sylancl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) ↔ 𝑓 : ( 1 ... 𝑛 ) ⟶ 𝑅 ) )
13 12 biimpa ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) ) → 𝑓 : ( 1 ... 𝑛 ) ⟶ 𝑅 )
14 5 nn0red ⊢ ( 𝜑 → ( ♯ ‘ 𝑅 ) ∈ ℝ )
15 14 ltp1d ⊢ ( 𝜑 → ( ♯ ‘ 𝑅 ) < ( ( ♯ ‘ 𝑅 ) + 1 ) )
16 peano2re ⊢ ( ( ♯ ‘ 𝑅 ) ∈ ℝ → ( ( ♯ ‘ 𝑅 ) + 1 ) ∈ ℝ )
17 14 16 syl ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑅 ) + 1 ) ∈ ℝ )
18 14 17 ltnled ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑅 ) < ( ( ♯ ‘ 𝑅 ) + 1 ) ↔ ¬ ( ( ♯ ‘ 𝑅 ) + 1 ) ≤ ( ♯ ‘ 𝑅 ) ) )
19 15 18 mpbid ⊢ ( 𝜑 → ¬ ( ( ♯ ‘ 𝑅 ) + 1 ) ≤ ( ♯ ‘ 𝑅 ) )
20 19 adantr ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑓 : ( 1 ... 𝑛 ) ⟶ 𝑅 ) ) → ¬ ( ( ♯ ‘ 𝑅 ) + 1 ) ≤ ( ♯ ‘ 𝑅 ) )
21 eluz2nn ⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 2 ) → 𝐾 ∈ ℕ )
22 2 21 syl ⊢ ( 𝜑 → 𝐾 ∈ ℕ )
23 22 adantr ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑓 : ( 1 ... 𝑛 ) ⟶ 𝑅 ) ) → 𝐾 ∈ ℕ )
24 23 nnnn0d ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑓 : ( 1 ... 𝑛 ) ⟶ 𝑅 ) ) → 𝐾 ∈ ℕ0 )
25 simprr ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑓 : ( 1 ... 𝑛 ) ⟶ 𝑅 ) ) → 𝑓 : ( 1 ... 𝑛 ) ⟶ 𝑅 )
26 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑓 : ( 1 ... 𝑛 ) ⟶ 𝑅 ) ) → ( ( ♯ ‘ 𝑅 ) + 1 ) ∈ ℕ )
27 eqid ⊢ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) = ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) )
28 10 24 25 26 27 vdwpc ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑓 : ( 1 ... 𝑛 ) ⟶ 𝑅 ) ) → ( ⟨ ( ( ♯ ‘ 𝑅 ) + 1 ) , 𝐾 ⟩ PolyAP 𝑓 ↔ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ( ℕ ↑m ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) ( ∀ 𝑖 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝑓 “ { ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ∧ ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ↦ ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) = ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) )
29 1 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑓 : ( 1 ... 𝑛 ) ⟶ 𝑅 ) ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ( ℕ ↑m ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝑓 “ { ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ) → 𝑅 ∈ Fin )
30 25 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑓 : ( 1 ... 𝑛 ) ⟶ 𝑅 ) ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ( ℕ ↑m ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) ) ) ∧ 𝑖 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) → 𝑓 : ( 1 ... 𝑛 ) ⟶ 𝑅 )
31 25 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑓 : ( 1 ... 𝑛 ) ⟶ 𝑅 ) ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ( ℕ ↑m ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) ) ) ∧ 𝑖 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) ∧ ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝑓 “ { ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ) → 𝑓 : ( 1 ... 𝑛 ) ⟶ 𝑅 )
32 simpr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑓 : ( 1 ... 𝑛 ) ⟶ 𝑅 ) ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ( ℕ ↑m ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) ) ) ∧ 𝑖 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) ∧ ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝑓 “ { ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ) → ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝑓 “ { ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) )
33 cnvimass ⊢ ( ◡ 𝑓 “ { ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ⊆ dom 𝑓
34 32 33 sstrdi ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑓 : ( 1 ... 𝑛 ) ⟶ 𝑅 ) ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ( ℕ ↑m ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) ) ) ∧ 𝑖 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) ∧ ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝑓 “ { ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ) → ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ dom 𝑓 )
35 31 34 fssdmd ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑓 : ( 1 ... 𝑛 ) ⟶ 𝑅 ) ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ( ℕ ↑m ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) ) ) ∧ 𝑖 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) ∧ ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝑓 “ { ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ) → ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( 1 ... 𝑛 ) )
36 22 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑓 : ( 1 ... 𝑛 ) ⟶ 𝑅 ) ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ( ℕ ↑m ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) ) ) ∧ 𝑖 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) → 𝐾 ∈ ℕ )
37 simplrl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑓 : ( 1 ... 𝑛 ) ⟶ 𝑅 ) ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ( ℕ ↑m ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) ) ) ∧ 𝑖 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) → 𝑎 ∈ ℕ )
38 simprr ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑓 : ( 1 ... 𝑛 ) ⟶ 𝑅 ) ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ( ℕ ↑m ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) ) ) → 𝑑 ∈ ( ℕ ↑m ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) )
39 nnex ⊢ ℕ ∈ V
40 ovex ⊢ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ∈ V
41 39 40 elmap ⊢ ( 𝑑 ∈ ( ℕ ↑m ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) ↔ 𝑑 : ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ⟶ ℕ )
42 38 41 sylib ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑓 : ( 1 ... 𝑛 ) ⟶ 𝑅 ) ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ( ℕ ↑m ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) ) ) → 𝑑 : ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ⟶ ℕ )
43 42 ffvelcdmda ⊢ ( ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑓 : ( 1 ... 𝑛 ) ⟶ 𝑅 ) ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ( ℕ ↑m ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) ) ) ∧ 𝑖 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) → ( 𝑑 ‘ 𝑖 ) ∈ ℕ )
44 37 43 nnaddcld ⊢ ( ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑓 : ( 1 ... 𝑛 ) ⟶ 𝑅 ) ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ( ℕ ↑m ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) ) ) ∧ 𝑖 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) → ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ∈ ℕ )
45 vdwapid1 ⊢ ( ( 𝐾 ∈ ℕ ∧ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ∈ ℕ ∧ ( 𝑑 ‘ 𝑖 ) ∈ ℕ ) → ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ∈ ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) )
46 36 44 43 45 syl3anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑓 : ( 1 ... 𝑛 ) ⟶ 𝑅 ) ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ( ℕ ↑m ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) ) ) ∧ 𝑖 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) → ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ∈ ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) )
47 46 adantr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑓 : ( 1 ... 𝑛 ) ⟶ 𝑅 ) ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ( ℕ ↑m ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) ) ) ∧ 𝑖 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) ∧ ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝑓 “ { ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ) → ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ∈ ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) )
48 35 47 sseldd ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑓 : ( 1 ... 𝑛 ) ⟶ 𝑅 ) ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ( ℕ ↑m ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) ) ) ∧ 𝑖 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) ∧ ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝑓 “ { ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ) → ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ∈ ( 1 ... 𝑛 ) )
49 48 ex ⊢ ( ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑓 : ( 1 ... 𝑛 ) ⟶ 𝑅 ) ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ( ℕ ↑m ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) ) ) ∧ 𝑖 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) → ( ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝑓 “ { ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) → ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ∈ ( 1 ... 𝑛 ) ) )
50 ffvelcdm ⊢ ( ( 𝑓 : ( 1 ... 𝑛 ) ⟶ 𝑅 ∧ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ∈ ( 1 ... 𝑛 ) ) → ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ∈ 𝑅 )
51 30 49 50 syl6an ⊢ ( ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑓 : ( 1 ... 𝑛 ) ⟶ 𝑅 ) ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ( ℕ ↑m ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) ) ) ∧ 𝑖 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) → ( ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝑓 “ { ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) → ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ∈ 𝑅 ) )
52 51 ralimdva ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑓 : ( 1 ... 𝑛 ) ⟶ 𝑅 ) ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ( ℕ ↑m ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) ) ) → ( ∀ 𝑖 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝑓 “ { ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) → ∀ 𝑖 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ∈ 𝑅 ) )
53 52 imp ⊢ ( ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑓 : ( 1 ... 𝑛 ) ⟶ 𝑅 ) ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ( ℕ ↑m ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝑓 “ { ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ) → ∀ 𝑖 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ∈ 𝑅 )
54 eqid ⊢ ( 𝑖 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ↦ ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) = ( 𝑖 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ↦ ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) )
55 54 fmpt ⊢ ( ∀ 𝑖 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ∈ 𝑅 ↔ ( 𝑖 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ↦ ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) : ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ⟶ 𝑅 )
56 53 55 sylib ⊢ ( ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑓 : ( 1 ... 𝑛 ) ⟶ 𝑅 ) ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ( ℕ ↑m ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝑓 “ { ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ) → ( 𝑖 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ↦ ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) : ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ⟶ 𝑅 )
57 56 frnd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑓 : ( 1 ... 𝑛 ) ⟶ 𝑅 ) ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ( ℕ ↑m ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝑓 “ { ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ) → ran ( 𝑖 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ↦ ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ⊆ 𝑅 )
58 ssdomg ⊢ ( 𝑅 ∈ Fin → ( ran ( 𝑖 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ↦ ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ⊆ 𝑅 → ran ( 𝑖 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ↦ ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ≼ 𝑅 ) )
59 29 57 58 sylc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑓 : ( 1 ... 𝑛 ) ⟶ 𝑅 ) ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ( ℕ ↑m ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝑓 “ { ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ) → ran ( 𝑖 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ↦ ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ≼ 𝑅 )
60 29 57 ssfid ⊢ ( ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑓 : ( 1 ... 𝑛 ) ⟶ 𝑅 ) ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ( ℕ ↑m ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝑓 “ { ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ) → ran ( 𝑖 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ↦ ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ∈ Fin )
61 hashdom ⊢ ( ( ran ( 𝑖 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ↦ ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ∈ Fin ∧ 𝑅 ∈ Fin ) → ( ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ↦ ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) ≤ ( ♯ ‘ 𝑅 ) ↔ ran ( 𝑖 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ↦ ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ≼ 𝑅 ) )
62 60 29 61 syl2anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑓 : ( 1 ... 𝑛 ) ⟶ 𝑅 ) ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ( ℕ ↑m ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝑓 “ { ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ) → ( ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ↦ ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) ≤ ( ♯ ‘ 𝑅 ) ↔ ran ( 𝑖 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ↦ ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ≼ 𝑅 ) )
63 59 62 mpbird ⊢ ( ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑓 : ( 1 ... 𝑛 ) ⟶ 𝑅 ) ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ( ℕ ↑m ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝑓 “ { ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ) → ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ↦ ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) ≤ ( ♯ ‘ 𝑅 ) )
64 breq1 ⊢ ( ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ↦ ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) = ( ( ♯ ‘ 𝑅 ) + 1 ) → ( ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ↦ ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) ≤ ( ♯ ‘ 𝑅 ) ↔ ( ( ♯ ‘ 𝑅 ) + 1 ) ≤ ( ♯ ‘ 𝑅 ) ) )
65 63 64 syl5ibcom ⊢ ( ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑓 : ( 1 ... 𝑛 ) ⟶ 𝑅 ) ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ( ℕ ↑m ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝑓 “ { ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ) → ( ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ↦ ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) = ( ( ♯ ‘ 𝑅 ) + 1 ) → ( ( ♯ ‘ 𝑅 ) + 1 ) ≤ ( ♯ ‘ 𝑅 ) ) )
66 65 expimpd ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑓 : ( 1 ... 𝑛 ) ⟶ 𝑅 ) ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ( ℕ ↑m ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) ) ) → ( ( ∀ 𝑖 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝑓 “ { ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ∧ ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ↦ ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) = ( ( ♯ ‘ 𝑅 ) + 1 ) ) → ( ( ♯ ‘ 𝑅 ) + 1 ) ≤ ( ♯ ‘ 𝑅 ) ) )
67 66 rexlimdvva ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑓 : ( 1 ... 𝑛 ) ⟶ 𝑅 ) ) → ( ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ( ℕ ↑m ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) ( ∀ 𝑖 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝑓 “ { ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ∧ ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ↦ ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) = ( ( ♯ ‘ 𝑅 ) + 1 ) ) → ( ( ♯ ‘ 𝑅 ) + 1 ) ≤ ( ♯ ‘ 𝑅 ) ) )
68 28 67 sylbid ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑓 : ( 1 ... 𝑛 ) ⟶ 𝑅 ) ) → ( ⟨ ( ( ♯ ‘ 𝑅 ) + 1 ) , 𝐾 ⟩ PolyAP 𝑓 → ( ( ♯ ‘ 𝑅 ) + 1 ) ≤ ( ♯ ‘ 𝑅 ) ) )
69 20 68 mtod ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑓 : ( 1 ... 𝑛 ) ⟶ 𝑅 ) ) → ¬ ⟨ ( ( ♯ ‘ 𝑅 ) + 1 ) , 𝐾 ⟩ PolyAP 𝑓 )
70 biorf ⊢ ( ¬ ⟨ ( ( ♯ ‘ 𝑅 ) + 1 ) , 𝐾 ⟩ PolyAP 𝑓 → ( ( 𝐾 + 1 ) MonoAP 𝑓 ↔ ( ⟨ ( ( ♯ ‘ 𝑅 ) + 1 ) , 𝐾 ⟩ PolyAP 𝑓 ∨ ( 𝐾 + 1 ) MonoAP 𝑓 ) ) )
71 69 70 syl ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑓 : ( 1 ... 𝑛 ) ⟶ 𝑅 ) ) → ( ( 𝐾 + 1 ) MonoAP 𝑓 ↔ ( ⟨ ( ( ♯ ‘ 𝑅 ) + 1 ) , 𝐾 ⟩ PolyAP 𝑓 ∨ ( 𝐾 + 1 ) MonoAP 𝑓 ) ) )
72 71 anassrs ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑓 : ( 1 ... 𝑛 ) ⟶ 𝑅 ) → ( ( 𝐾 + 1 ) MonoAP 𝑓 ↔ ( ⟨ ( ( ♯ ‘ 𝑅 ) + 1 ) , 𝐾 ⟩ PolyAP 𝑓 ∨ ( 𝐾 + 1 ) MonoAP 𝑓 ) ) )
73 13 72 syldan ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) ) → ( ( 𝐾 + 1 ) MonoAP 𝑓 ↔ ( ⟨ ( ( ♯ ‘ 𝑅 ) + 1 ) , 𝐾 ⟩ PolyAP 𝑓 ∨ ( 𝐾 + 1 ) MonoAP 𝑓 ) ) )
74 73 ralbidva ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) ( 𝐾 + 1 ) MonoAP 𝑓 ↔ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) ( ⟨ ( ( ♯ ‘ 𝑅 ) + 1 ) , 𝐾 ⟩ PolyAP 𝑓 ∨ ( 𝐾 + 1 ) MonoAP 𝑓 ) ) )
75 74 rexbidva ⊢ ( 𝜑 → ( ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) ( 𝐾 + 1 ) MonoAP 𝑓 ↔ ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) ( ⟨ ( ( ♯ ‘ 𝑅 ) + 1 ) , 𝐾 ⟩ PolyAP 𝑓 ∨ ( 𝐾 + 1 ) MonoAP 𝑓 ) ) )
76 8 75 mpbird ⊢ ( 𝜑 → ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) ( 𝐾 + 1 ) MonoAP 𝑓 )