vdwlem9

	Ref	Expression
Hypotheses	vdw.r	$⊢ φ \to R \in Fin$
	vdwlem9.k	$⊢ φ \to K \in ℤ_{\geq 2}$
	vdwlem9.s	$⊢ φ \to \forall s \in Fin \exists n \in ℕ \forall f \in (s^{(1 \dots n)}) K MonoAP f$
	vdwlem9.m	$⊢ φ \to M \in ℕ$
	vdwlem9.w	$⊢ φ \to W \in ℕ$
	vdwlem9.g	$⊢ φ \to \forall g \in (R^{(1 \dots W)}) (⟨M, K⟩ PolyAP g \lor (K + 1) MonoAP g)$
	vdwlem9.v	$⊢ φ \to V \in ℕ$
	vdwlem9.a	$⊢ φ \to \forall f \in ({(R^{(1 \dots W)})}^{(1 \dots V)}) K MonoAP f$
	vdwlem9.h	$⊢ φ \to H : (1 \dots W 2 V) ⟶ R$
	vdwlem9.f	$⊢ F = (x \in (1 \dots V) ⟼ (y \in (1 \dots W) ⟼ H (y + W (x - 1 + V))))$
Assertion	vdwlem9	$⊢ φ \to (⟨M + 1, K⟩ PolyAP H \lor (K + 1) MonoAP H)$

Proof

Step	Hyp	Ref	Expression
1		vdw.r	$⊢ φ \to R \in Fin$
2		vdwlem9.k	$⊢ φ \to K \in ℤ_{\geq 2}$
3		vdwlem9.s	$⊢ φ \to \forall s \in Fin \exists n \in ℕ \forall f \in (s^{(1 \dots n)}) K MonoAP f$
4		vdwlem9.m	$⊢ φ \to M \in ℕ$
5		vdwlem9.w	$⊢ φ \to W \in ℕ$
6		vdwlem9.g	$⊢ φ \to \forall g \in (R^{(1 \dots W)}) (⟨M, K⟩ PolyAP g \lor (K + 1) MonoAP g)$
7		vdwlem9.v	$⊢ φ \to V \in ℕ$
8		vdwlem9.a	$⊢ φ \to \forall f \in ({(R^{(1 \dots W)})}^{(1 \dots V)}) K MonoAP f$
9		vdwlem9.h	$⊢ φ \to H : (1 \dots W 2 V) ⟶ R$
10		vdwlem9.f	$⊢ F = (x \in (1 \dots V) ⟼ (y \in (1 \dots W) ⟼ H (y + W (x - 1 + V))))$
11		breq2	$⊢ f = F \to (K MonoAP f \leftrightarrow K MonoAP F)$
12	7 5 1 9 10	vdwlem4	$⊢ φ \to F : (1 \dots V) ⟶ R^{(1 \dots W)}$
13		ovex	$⊢ R^{(1 \dots W)} \in V$
14		ovex	$⊢ (1 \dots V) \in V$
15	13 14	elmap	$⊢ F \in ({(R^{(1 \dots W)})}^{(1 \dots V)}) \leftrightarrow F : (1 \dots V) ⟶ R^{(1 \dots W)}$
16	12 15	sylibr	$⊢ φ \to F \in ({(R^{(1 \dots W)})}^{(1 \dots V)})$
17	11 8 16	rspcdva	$⊢ φ \to K MonoAP F$
18		eluz2nn	$⊢ K \in ℤ_{\geq 2} \to K \in ℕ$
19	2 18	syl	$⊢ φ \to K \in ℕ$
20	19	nnnn0d	$⊢ φ \to K \in ℕ_{0}$
21	14 20 12	vdwmc	$⊢ φ \to (K MonoAP F \leftrightarrow \exists g \exists a \in ℕ \exists d \in ℕ a AP (K) d \subseteq F^{-1} [\{g\}])$
22	6	adantr	$⊢ (φ \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq F^{-1} [\{g\}])) \to \forall g \in (R^{(1 \dots W)}) (⟨M, K⟩ PolyAP g \lor (K + 1) MonoAP g)$
23		simprr	$⊢ (φ \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq F^{-1} [\{g\}])) \to a AP (K) d \subseteq F^{-1} [\{g\}]$
24	19	adantr	$⊢ (φ \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq F^{-1} [\{g\}])) \to K \in ℕ$
25		simprll	$⊢ (φ \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq F^{-1} [\{g\}])) \to a \in ℕ$
26		simprlr	$⊢ (φ \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq F^{-1} [\{g\}])) \to d \in ℕ$
27		vdwapid1	$⊢ (K \in ℕ \land a \in ℕ \land d \in ℕ) \to a \in (a AP (K) d)$
28	24 25 26 27	syl3anc	$⊢ (φ \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq F^{-1} [\{g\}])) \to a \in (a AP (K) d)$
29	23 28	sseldd	$⊢ (φ \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq F^{-1} [\{g\}])) \to a \in F^{-1} [\{g\}]$
30	12	ffnd	$⊢ φ \to F Fn (1 \dots V)$
31	30	adantr	$⊢ (φ \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq F^{-1} [\{g\}])) \to F Fn (1 \dots V)$
32		fniniseg	$⊢ F Fn (1 \dots V) \to (a \in F^{-1} [\{g\}] \leftrightarrow (a \in (1 \dots V) \land F (a) = g))$
33	31 32	syl	$⊢ (φ \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq F^{-1} [\{g\}])) \to (a \in F^{-1} [\{g\}] \leftrightarrow (a \in (1 \dots V) \land F (a) = g))$
34	29 33	mpbid	$⊢ (φ \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq F^{-1} [\{g\}])) \to (a \in (1 \dots V) \land F (a) = g)$
35	34	simprd	$⊢ (φ \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq F^{-1} [\{g\}])) \to F (a) = g$
36	12	adantr	$⊢ (φ \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq F^{-1} [\{g\}])) \to F : (1 \dots V) ⟶ R^{(1 \dots W)}$
37	34	simpld	$⊢ (φ \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq F^{-1} [\{g\}])) \to a \in (1 \dots V)$
38	36 37	ffvelcdmd	$⊢ (φ \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq F^{-1} [\{g\}])) \to F (a) \in (R^{(1 \dots W)})$
39	35 38	eqeltrrd	$⊢ (φ \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq F^{-1} [\{g\}])) \to g \in (R^{(1 \dots W)})$
40		rsp	$⊢ \forall g \in (R^{(1 \dots W)}) (⟨M, K⟩ PolyAP g \lor (K + 1) MonoAP g) \to (g \in (R^{(1 \dots W)}) \to (⟨M, K⟩ PolyAP g \lor (K + 1) MonoAP g))$
41	22 39 40	sylc	$⊢ (φ \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq F^{-1} [\{g\}])) \to (⟨M, K⟩ PolyAP g \lor (K + 1) MonoAP g)$
42	7	adantr	$⊢ (φ \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq F^{-1} [\{g\}])) \to V \in ℕ$
43	5	adantr	$⊢ (φ \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq F^{-1} [\{g\}])) \to W \in ℕ$
44	1	adantr	$⊢ (φ \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq F^{-1} [\{g\}])) \to R \in Fin$
45	9	adantr	$⊢ (φ \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq F^{-1} [\{g\}])) \to H : (1 \dots W 2 V) ⟶ R$
46	4	adantr	$⊢ (φ \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq F^{-1} [\{g\}])) \to M \in ℕ$
47		ovex	$⊢ (1 \dots W) \in V$
48		elmapg	$⊢ (R \in Fin \land (1 \dots W) \in V) \to (g \in (R^{(1 \dots W)}) \leftrightarrow g : (1 \dots W) ⟶ R)$
49	44 47 48	sylancl	$⊢ (φ \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq F^{-1} [\{g\}])) \to (g \in (R^{(1 \dots W)}) \leftrightarrow g : (1 \dots W) ⟶ R)$
50	39 49	mpbid	$⊢ (φ \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq F^{-1} [\{g\}])) \to g : (1 \dots W) ⟶ R$
51	2	adantr	$⊢ (φ \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq F^{-1} [\{g\}])) \to K \in ℤ_{\geq 2}$
52	42 43 44 45 10 46 50 51 25 26 23	vdwlem7	$⊢ (φ \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq F^{-1} [\{g\}])) \to (⟨M, K⟩ PolyAP g \to (⟨M + 1, K⟩ PolyAP H \lor (K + 1) MonoAP g))$
53		olc	$⊢ (K + 1) MonoAP g \to (⟨M + 1, K⟩ PolyAP H \lor (K + 1) MonoAP g)$
54	53	a1i	$⊢ (φ \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq F^{-1} [\{g\}])) \to ((K + 1) MonoAP g \to (⟨M + 1, K⟩ PolyAP H \lor (K + 1) MonoAP g))$
55	52 54	jaod	$⊢ (φ \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq F^{-1} [\{g\}])) \to ((⟨M, K⟩ PolyAP g \lor (K + 1) MonoAP g) \to (⟨M + 1, K⟩ PolyAP H \lor (K + 1) MonoAP g))$
56		oveq1	$⊢ x = a \to x - 1 = a - 1$
57	56	oveq1d	$⊢ x = a \to x - 1 + V = a - 1 + V$
58	57	oveq2d	$⊢ x = a \to W (x - 1 + V) = W (a - 1 + V)$
59	58	oveq2d	$⊢ x = a \to y + W (x - 1 + V) = y + W (a - 1 + V)$
60	59	fveq2d	$⊢ x = a \to H (y + W (x - 1 + V)) = H (y + W (a - 1 + V))$
61	60	mpteq2dv	$⊢ x = a \to (y \in (1 \dots W) ⟼ H (y + W (x - 1 + V))) = (y \in (1 \dots W) ⟼ H (y + W (a - 1 + V)))$
62	47	mptex	$⊢ (y \in (1 \dots W) ⟼ H (y + W (a - 1 + V))) \in V$
63	61 10 62	fvmpt	$⊢ a \in (1 \dots V) \to F (a) = (y \in (1 \dots W) ⟼ H (y + W (a - 1 + V)))$
64	37 63	syl	$⊢ (φ \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq F^{-1} [\{g\}])) \to F (a) = (y \in (1 \dots W) ⟼ H (y + W (a - 1 + V)))$
65	64 35	eqtr3d	$⊢ (φ \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq F^{-1} [\{g\}])) \to (y \in (1 \dots W) ⟼ H (y + W (a - 1 + V))) = g$
66	65	breq2d	$⊢ (φ \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq F^{-1} [\{g\}])) \to ((K + 1) MonoAP (y \in (1 \dots W) ⟼ H (y + W (a - 1 + V))) \leftrightarrow (K + 1) MonoAP g)$
67	20	adantr	$⊢ (φ \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq F^{-1} [\{g\}])) \to K \in ℕ_{0}$
68		peano2nn0	$⊢ K \in ℕ_{0} \to K + 1 \in ℕ_{0}$
69	67 68	syl	$⊢ (φ \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq F^{-1} [\{g\}])) \to K + 1 \in ℕ_{0}$
70		nnm1nn0	$⊢ a \in ℕ \to a - 1 \in ℕ_{0}$
71	25 70	syl	$⊢ (φ \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq F^{-1} [\{g\}])) \to a - 1 \in ℕ_{0}$
72		nn0nnaddcl	$⊢ (a - 1 \in ℕ_{0} \land V \in ℕ) \to a - 1 + V \in ℕ$
73	71 42 72	syl2anc	$⊢ (φ \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq F^{-1} [\{g\}])) \to a - 1 + V \in ℕ$
74	43 73	nnmulcld	$⊢ (φ \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq F^{-1} [\{g\}])) \to W (a - 1 + V) \in ℕ$
75	25 42	nnaddcld	$⊢ (φ \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq F^{-1} [\{g\}])) \to a + V \in ℕ$
76	43 75	nnmulcld	$⊢ (φ \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq F^{-1} [\{g\}])) \to W (a + V) \in ℕ$
77	76	nnzd	$⊢ (φ \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq F^{-1} [\{g\}])) \to W (a + V) \in ℤ$
78		2nn	$⊢ 2 \in ℕ$
79		nnmulcl	$⊢ (2 \in ℕ \land V \in ℕ) \to 2 V \in ℕ$
80	78 7 79	sylancr	$⊢ φ \to 2 V \in ℕ$
81	5 80	nnmulcld	$⊢ φ \to W 2 V \in ℕ$
82	81	nnzd	$⊢ φ \to W 2 V \in ℤ$
83	82	adantr	$⊢ (φ \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq F^{-1} [\{g\}])) \to W 2 V \in ℤ$
84	25	nnred	$⊢ (φ \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq F^{-1} [\{g\}])) \to a \in ℝ$
85	42	nnred	$⊢ (φ \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq F^{-1} [\{g\}])) \to V \in ℝ$
86		elfzle2	$⊢ a \in (1 \dots V) \to a \leq V$
87	37 86	syl	$⊢ (φ \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq F^{-1} [\{g\}])) \to a \leq V$
88	84 85 85 87	leadd1dd	$⊢ (φ \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq F^{-1} [\{g\}])) \to a + V \leq V + V$
89	42	nncnd	$⊢ (φ \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq F^{-1} [\{g\}])) \to V \in ℂ$
90	89	2timesd	$⊢ (φ \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq F^{-1} [\{g\}])) \to 2 V = V + V$
91	88 90	breqtrrd	$⊢ (φ \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq F^{-1} [\{g\}])) \to a + V \leq 2 V$
92	75	nnred	$⊢ (φ \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq F^{-1} [\{g\}])) \to a + V \in ℝ$
93	80	nnred	$⊢ φ \to 2 V \in ℝ$
94	93	adantr	$⊢ (φ \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq F^{-1} [\{g\}])) \to 2 V \in ℝ$
95	43	nnred	$⊢ (φ \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq F^{-1} [\{g\}])) \to W \in ℝ$
96	43	nngt0d	$⊢ (φ \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq F^{-1} [\{g\}])) \to 0 < W$
97		lemul2	$⊢ (a + V \in ℝ \land 2 V \in ℝ \land (W \in ℝ \land 0 < W)) \to (a + V \leq 2 V \leftrightarrow W (a + V) \leq W 2 V)$
98	92 94 95 96 97	syl112anc	$⊢ (φ \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq F^{-1} [\{g\}])) \to (a + V \leq 2 V \leftrightarrow W (a + V) \leq W 2 V)$
99	91 98	mpbid	$⊢ (φ \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq F^{-1} [\{g\}])) \to W (a + V) \leq W 2 V$
100		eluz2	$⊢ W 2 V \in ℤ_{\geq W (a + V)} \leftrightarrow (W (a + V) \in ℤ \land W 2 V \in ℤ \land W (a + V) \leq W 2 V)$
101	77 83 99 100	syl3anbrc	$⊢ (φ \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq F^{-1} [\{g\}])) \to W 2 V \in ℤ_{\geq W (a + V)}$
102	43	nncnd	$⊢ (φ \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq F^{-1} [\{g\}])) \to W \in ℂ$
103		1cnd	$⊢ (φ \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq F^{-1} [\{g\}])) \to 1 \in ℂ$
104	71	nn0cnd	$⊢ (φ \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq F^{-1} [\{g\}])) \to a - 1 \in ℂ$
105	104 89	addcld	$⊢ (φ \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq F^{-1} [\{g\}])) \to a - 1 + V \in ℂ$
106	102 103 105	adddid	$⊢ (φ \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq F^{-1} [\{g\}])) \to W (1 + (a - 1) + V) = W \cdot 1 + W (a - 1 + V)$
107	103 104 89	addassd	$⊢ (φ \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq F^{-1} [\{g\}])) \to 1 + (a - 1) + V = 1 + (a - 1) + V$
108		ax-1cn	$⊢ 1 \in ℂ$
109	25	nncnd	$⊢ (φ \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq F^{-1} [\{g\}])) \to a \in ℂ$
110		pncan3	$⊢ (1 \in ℂ \land a \in ℂ) \to 1 + a - 1 = a$
111	108 109 110	sylancr	$⊢ (φ \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq F^{-1} [\{g\}])) \to 1 + a - 1 = a$
112	111	oveq1d	$⊢ (φ \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq F^{-1} [\{g\}])) \to 1 + (a - 1) + V = a + V$
113	107 112	eqtr3d	$⊢ (φ \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq F^{-1} [\{g\}])) \to 1 + (a - 1) + V = a + V$
114	113	oveq2d	$⊢ (φ \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq F^{-1} [\{g\}])) \to W (1 + (a - 1) + V) = W (a + V)$
115	102	mulridd	$⊢ (φ \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq F^{-1} [\{g\}])) \to W \cdot 1 = W$
116	115	oveq1d	$⊢ (φ \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq F^{-1} [\{g\}])) \to W \cdot 1 + W (a - 1 + V) = W + W (a - 1 + V)$
117	106 114 116	3eqtr3d	$⊢ (φ \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq F^{-1} [\{g\}])) \to W (a + V) = W + W (a - 1 + V)$
118	117	fveq2d	$⊢ (φ \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq F^{-1} [\{g\}])) \to ℤ_{\geq W (a + V)} = ℤ_{\geq (W + W (a - 1 + V))}$
119	101 118	eleqtrd	$⊢ (φ \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq F^{-1} [\{g\}])) \to W 2 V \in ℤ_{\geq (W + W (a - 1 + V))}$
120		fvoveq1	$⊢ y = z \to H (y + W (a - 1 + V)) = H (z + W (a - 1 + V))$
121	120	cbvmptv	$⊢ (y \in (1 \dots W) ⟼ H (y + W (a - 1 + V))) = (z \in (1 \dots W) ⟼ H (z + W (a - 1 + V)))$
122	44 69 43 74 45 119 121	vdwlem2	$⊢ (φ \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq F^{-1} [\{g\}])) \to ((K + 1) MonoAP (y \in (1 \dots W) ⟼ H (y + W (a - 1 + V))) \to (K + 1) MonoAP H)$
123	66 122	sylbird	$⊢ (φ \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq F^{-1} [\{g\}])) \to ((K + 1) MonoAP g \to (K + 1) MonoAP H)$
124	123	orim2d	$⊢ (φ \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq F^{-1} [\{g\}])) \to ((⟨M + 1, K⟩ PolyAP H \lor (K + 1) MonoAP g) \to (⟨M + 1, K⟩ PolyAP H \lor (K + 1) MonoAP H))$
125	55 124	syld	$⊢ (φ \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq F^{-1} [\{g\}])) \to ((⟨M, K⟩ PolyAP g \lor (K + 1) MonoAP g) \to (⟨M + 1, K⟩ PolyAP H \lor (K + 1) MonoAP H))$
126	41 125	mpd	$⊢ (φ \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq F^{-1} [\{g\}])) \to (⟨M + 1, K⟩ PolyAP H \lor (K + 1) MonoAP H)$
127	126	expr	$⊢ (φ \land (a \in ℕ \land d \in ℕ)) \to (a AP (K) d \subseteq F^{-1} [\{g\}] \to (⟨M + 1, K⟩ PolyAP H \lor (K + 1) MonoAP H))$
128	127	rexlimdvva	$⊢ φ \to (\exists a \in ℕ \exists d \in ℕ a AP (K) d \subseteq F^{-1} [\{g\}] \to (⟨M + 1, K⟩ PolyAP H \lor (K + 1) MonoAP H))$
129	128	exlimdv	$⊢ φ \to (\exists g \exists a \in ℕ \exists d \in ℕ a AP (K) d \subseteq F^{-1} [\{g\}] \to (⟨M + 1, K⟩ PolyAP H \lor (K + 1) MonoAP H))$
130	21 129	sylbid	$⊢ φ \to (K MonoAP F \to (⟨M + 1, K⟩ PolyAP H \lor (K + 1) MonoAP H))$
131	17 130	mpd	$⊢ φ \to (⟨M + 1, K⟩ PolyAP H \lor (K + 1) MonoAP H)$

Metamath Proof Explorer

Theorem vdwlem9

Proof