Theorem vdwlem7

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

	Ref	Expression
Hypotheses	vdwlem3.v	⊢ ( 𝜑 → 𝑉 ∈ ℕ )
	vdwlem3.w	⊢ ( 𝜑 → 𝑊 ∈ ℕ )
	vdwlem4.r	⊢ ( 𝜑 → 𝑅 ∈ Fin )
	vdwlem4.h	⊢ ( 𝜑 → 𝐻 : ( 1 ... ( 𝑊 · ( 2 · 𝑉 ) ) ) ⟶ 𝑅 )
	vdwlem4.f	⊢ 𝐹 = ( 𝑥 ∈ ( 1 ... 𝑉 ) ↦ ( 𝑦 ∈ ( 1 ... 𝑊 ) ↦ ( 𝐻 ‘ ( 𝑦 + ( 𝑊 · ( ( 𝑥 − 1 ) + 𝑉 ) ) ) ) ) )
	vdwlem7.m	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
	vdwlem7.g	⊢ ( 𝜑 → 𝐺 : ( 1 ... 𝑊 ) ⟶ 𝑅 )
	vdwlem7.k	⊢ ( 𝜑 → 𝐾 ∈ ( ℤ≥ ‘ 2 ) )
	vdwlem7.a	⊢ ( 𝜑 → 𝐴 ∈ ℕ )
	vdwlem7.d	⊢ ( 𝜑 → 𝐷 ∈ ℕ )
	vdwlem7.s	⊢ ( 𝜑 → ( 𝐴 ( AP ‘ 𝐾 ) 𝐷 ) ⊆ ( ◡ 𝐹 “ { 𝐺 } ) )
Assertion	vdwlem7	⊢ ( 𝜑 → ( ⟨ 𝑀 , 𝐾 ⟩ PolyAP 𝐺 → ( ⟨ ( 𝑀 + 1 ) , 𝐾 ⟩ PolyAP 𝐻 ∨ ( 𝐾 + 1 ) MonoAP 𝐺 ) ) )

Proof

Step	Hyp	Ref	Expression
1		vdwlem3.v	⊢ ( 𝜑 → 𝑉 ∈ ℕ )
2		vdwlem3.w	⊢ ( 𝜑 → 𝑊 ∈ ℕ )
3		vdwlem4.r	⊢ ( 𝜑 → 𝑅 ∈ Fin )
4		vdwlem4.h	⊢ ( 𝜑 → 𝐻 : ( 1 ... ( 𝑊 · ( 2 · 𝑉 ) ) ) ⟶ 𝑅 )
5		vdwlem4.f	⊢ 𝐹 = ( 𝑥 ∈ ( 1 ... 𝑉 ) ↦ ( 𝑦 ∈ ( 1 ... 𝑊 ) ↦ ( 𝐻 ‘ ( 𝑦 + ( 𝑊 · ( ( 𝑥 − 1 ) + 𝑉 ) ) ) ) ) )
6		vdwlem7.m	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
7		vdwlem7.g	⊢ ( 𝜑 → 𝐺 : ( 1 ... 𝑊 ) ⟶ 𝑅 )
8		vdwlem7.k	⊢ ( 𝜑 → 𝐾 ∈ ( ℤ≥ ‘ 2 ) )
9		vdwlem7.a	⊢ ( 𝜑 → 𝐴 ∈ ℕ )
10		vdwlem7.d	⊢ ( 𝜑 → 𝐷 ∈ ℕ )
11		vdwlem7.s	⊢ ( 𝜑 → ( 𝐴 ( AP ‘ 𝐾 ) 𝐷 ) ⊆ ( ◡ 𝐹 “ { 𝐺 } ) )
12		ovex	⊢ ( 1 ... 𝑊 ) ∈ V
13		2nn0	⊢ 2 ∈ ℕ0
14		eluznn0	⊢ ( ( 2 ∈ ℕ0 ∧ 𝐾 ∈ ( ℤ≥ ‘ 2 ) ) → 𝐾 ∈ ℕ0 )
15	13 8 14	sylancr	⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
16		eqid	⊢ ( 1 ... 𝑀 ) = ( 1 ... 𝑀 )
17	12 15 7 6 16	vdwpc	⊢ ( 𝜑 → ( ⟨ 𝑀 , 𝐾 ⟩ PolyAP 𝐺 ↔ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ( ℕ ↑m ( 1 ... 𝑀 ) ) ( ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝐺 “ { ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ∧ ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) = 𝑀 ) ) )
18	1	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ( ℕ ↑m ( 1 ... 𝑀 ) ) ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝐺 “ { ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ∧ ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) = 𝑀 ) ) → 𝑉 ∈ ℕ )
19	2	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ( ℕ ↑m ( 1 ... 𝑀 ) ) ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝐺 “ { ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ∧ ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) = 𝑀 ) ) → 𝑊 ∈ ℕ )
20	3	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ( ℕ ↑m ( 1 ... 𝑀 ) ) ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝐺 “ { ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ∧ ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) = 𝑀 ) ) → 𝑅 ∈ Fin )
21	4	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ( ℕ ↑m ( 1 ... 𝑀 ) ) ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝐺 “ { ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ∧ ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) = 𝑀 ) ) → 𝐻 : ( 1 ... ( 𝑊 · ( 2 · 𝑉 ) ) ) ⟶ 𝑅 )
22	6	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ( ℕ ↑m ( 1 ... 𝑀 ) ) ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝐺 “ { ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ∧ ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) = 𝑀 ) ) → 𝑀 ∈ ℕ )
23	7	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ( ℕ ↑m ( 1 ... 𝑀 ) ) ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝐺 “ { ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ∧ ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) = 𝑀 ) ) → 𝐺 : ( 1 ... 𝑊 ) ⟶ 𝑅 )
24	8	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ( ℕ ↑m ( 1 ... 𝑀 ) ) ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝐺 “ { ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ∧ ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) = 𝑀 ) ) → 𝐾 ∈ ( ℤ≥ ‘ 2 ) )
25	9	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ( ℕ ↑m ( 1 ... 𝑀 ) ) ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝐺 “ { ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ∧ ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) = 𝑀 ) ) → 𝐴 ∈ ℕ )
26	10	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ( ℕ ↑m ( 1 ... 𝑀 ) ) ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝐺 “ { ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ∧ ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) = 𝑀 ) ) → 𝐷 ∈ ℕ )
27	11	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ( ℕ ↑m ( 1 ... 𝑀 ) ) ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝐺 “ { ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ∧ ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) = 𝑀 ) ) → ( 𝐴 ( AP ‘ 𝐾 ) 𝐷 ) ⊆ ( ◡ 𝐹 “ { 𝐺 } ) )
28		simplrl	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ( ℕ ↑m ( 1 ... 𝑀 ) ) ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝐺 “ { ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ∧ ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) = 𝑀 ) ) → 𝑎 ∈ ℕ )
29		simplrr	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ( ℕ ↑m ( 1 ... 𝑀 ) ) ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝐺 “ { ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ∧ ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) = 𝑀 ) ) → 𝑑 ∈ ( ℕ ↑m ( 1 ... 𝑀 ) ) )
30		nnex	⊢ ℕ ∈ V
31		ovex	⊢ ( 1 ... 𝑀 ) ∈ V
32	30 31	elmap	⊢ ( 𝑑 ∈ ( ℕ ↑m ( 1 ... 𝑀 ) ) ↔ 𝑑 : ( 1 ... 𝑀 ) ⟶ ℕ )
33	29 32	sylib	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ( ℕ ↑m ( 1 ... 𝑀 ) ) ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝐺 “ { ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ∧ ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) = 𝑀 ) ) → 𝑑 : ( 1 ... 𝑀 ) ⟶ ℕ )
34		simprl	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ( ℕ ↑m ( 1 ... 𝑀 ) ) ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝐺 “ { ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ∧ ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) = 𝑀 ) ) → ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝐺 “ { ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) )
35		fveq2	⊢ ( 𝑖 = 𝑘 → ( 𝑑 ‘ 𝑖 ) = ( 𝑑 ‘ 𝑘 ) )
36	35	oveq2d	⊢ ( 𝑖 = 𝑘 → ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) = ( 𝑎 + ( 𝑑 ‘ 𝑘 ) ) )
37	36 35	oveq12d	⊢ ( 𝑖 = 𝑘 → ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) = ( ( 𝑎 + ( 𝑑 ‘ 𝑘 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑘 ) ) )
38	36	fveq2d	⊢ ( 𝑖 = 𝑘 → ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) = ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑘 ) ) ) )
39	38	sneqd	⊢ ( 𝑖 = 𝑘 → { ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } = { ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑘 ) ) ) } )
40	39	imaeq2d	⊢ ( 𝑖 = 𝑘 → ( ◡ 𝐺 “ { ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) = ( ◡ 𝐺 “ { ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑘 ) ) ) } ) )
41	37 40	sseq12d	⊢ ( 𝑖 = 𝑘 → ( ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝐺 “ { ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ↔ ( ( 𝑎 + ( 𝑑 ‘ 𝑘 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑘 ) ) ⊆ ( ◡ 𝐺 “ { ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑘 ) ) ) } ) ) )
42	41	cbvralvw	⊢ ( ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝐺 “ { ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ↔ ∀ 𝑘 ∈ ( 1 ... 𝑀 ) ( ( 𝑎 + ( 𝑑 ‘ 𝑘 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑘 ) ) ⊆ ( ◡ 𝐺 “ { ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑘 ) ) ) } ) )
43	34 42	sylib	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ( ℕ ↑m ( 1 ... 𝑀 ) ) ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝐺 “ { ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ∧ ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) = 𝑀 ) ) → ∀ 𝑘 ∈ ( 1 ... 𝑀 ) ( ( 𝑎 + ( 𝑑 ‘ 𝑘 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑘 ) ) ⊆ ( ◡ 𝐺 “ { ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑘 ) ) ) } ) )
44	38	cbvmptv	⊢ ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) = ( 𝑘 ∈ ( 1 ... 𝑀 ) ↦ ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑘 ) ) ) )
45		simprr	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ( ℕ ↑m ( 1 ... 𝑀 ) ) ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝐺 “ { ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ∧ ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) = 𝑀 ) ) → ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) = 𝑀 )
46		eqid	⊢ ( 𝑎 + ( 𝑊 · ( ( 𝐴 + ( 𝑉 − 𝐷 ) ) − 1 ) ) ) = ( 𝑎 + ( 𝑊 · ( ( 𝐴 + ( 𝑉 − 𝐷 ) ) − 1 ) ) )
47		eqid	⊢ ( 𝑗 ∈ ( 1 ... ( 𝑀 + 1 ) ) ↦ ( if ( 𝑗 = ( 𝑀 + 1 ) , 0 , ( 𝑑 ‘ 𝑗 ) ) + ( 𝑊 · 𝐷 ) ) ) = ( 𝑗 ∈ ( 1 ... ( 𝑀 + 1 ) ) ↦ ( if ( 𝑗 = ( 𝑀 + 1 ) , 0 , ( 𝑑 ‘ 𝑗 ) ) + ( 𝑊 · 𝐷 ) ) )
48	18 19 20 21 5 22 23 24 25 26 27 28 33 43 44 45 46 47	vdwlem6	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ( ℕ ↑m ( 1 ... 𝑀 ) ) ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝐺 “ { ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ∧ ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) = 𝑀 ) ) → ( ⟨ ( 𝑀 + 1 ) , 𝐾 ⟩ PolyAP 𝐻 ∨ ( 𝐾 + 1 ) MonoAP 𝐺 ) )
49	48	ex	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ( ℕ ↑m ( 1 ... 𝑀 ) ) ) ) → ( ( ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝐺 “ { ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ∧ ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) = 𝑀 ) → ( ⟨ ( 𝑀 + 1 ) , 𝐾 ⟩ PolyAP 𝐻 ∨ ( 𝐾 + 1 ) MonoAP 𝐺 ) ) )
50	49	rexlimdvva	⊢ ( 𝜑 → ( ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ( ℕ ↑m ( 1 ... 𝑀 ) ) ( ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝐺 “ { ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ∧ ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) = 𝑀 ) → ( ⟨ ( 𝑀 + 1 ) , 𝐾 ⟩ PolyAP 𝐻 ∨ ( 𝐾 + 1 ) MonoAP 𝐺 ) ) )
51	17 50	sylbid	⊢ ( 𝜑 → ( ⟨ 𝑀 , 𝐾 ⟩ PolyAP 𝐺 → ( ⟨ ( 𝑀 + 1 ) , 𝐾 ⟩ PolyAP 𝐻 ∨ ( 𝐾 + 1 ) MonoAP 𝐺 ) ) )