vdwlem10

Description: Lemma for vdw . Set up secondary induction on M . (Contributed by Mario Carneiro, 18-Aug-2014)

	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$
	vdwlem10.m	$⊢ φ \to M \in ℕ$
Assertion	vdwlem10	$⊢ φ \to \exists n \in ℕ \forall f \in (R^{(1 \dots n)}) (⟨M, K⟩ PolyAP f \lor (K + 1) MonoAP f)$

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		vdwlem10.m	$⊢ φ \to M \in ℕ$
5		opeq1	$⊢ x = 1 \to ⟨x, K⟩ = ⟨1, K⟩$
6	5	breq1d	$⊢ x = 1 \to (⟨x, K⟩ PolyAP f \leftrightarrow ⟨1, K⟩ PolyAP f)$
7	6	orbi1d	$⊢ x = 1 \to ((⟨x, K⟩ PolyAP f \lor (K + 1) MonoAP f) \leftrightarrow (⟨1, K⟩ PolyAP f \lor (K + 1) MonoAP f))$
8	7	rexralbidv	$⊢ x = 1 \to (\exists n \in ℕ \forall f \in (R^{(1 \dots n)}) (⟨x, K⟩ PolyAP f \lor (K + 1) MonoAP f) \leftrightarrow \exists n \in ℕ \forall f \in (R^{(1 \dots n)}) (⟨1, K⟩ PolyAP f \lor (K + 1) MonoAP f))$
9	8	imbi2d	$⊢ x = 1 \to ((φ \to \exists n \in ℕ \forall f \in (R^{(1 \dots n)}) (⟨x, K⟩ PolyAP f \lor (K + 1) MonoAP f)) \leftrightarrow (φ \to \exists n \in ℕ \forall f \in (R^{(1 \dots n)}) (⟨1, K⟩ PolyAP f \lor (K + 1) MonoAP f)))$
10		opeq1	$⊢ x = m \to ⟨x, K⟩ = ⟨m, K⟩$
11	10	breq1d	$⊢ x = m \to (⟨x, K⟩ PolyAP f \leftrightarrow ⟨m, K⟩ PolyAP f)$
12	11	orbi1d	$⊢ x = m \to ((⟨x, K⟩ PolyAP f \lor (K + 1) MonoAP f) \leftrightarrow (⟨m, K⟩ PolyAP f \lor (K + 1) MonoAP f))$
13	12	rexralbidv	$⊢ x = m \to (\exists n \in ℕ \forall f \in (R^{(1 \dots n)}) (⟨x, K⟩ PolyAP f \lor (K + 1) MonoAP f) \leftrightarrow \exists n \in ℕ \forall f \in (R^{(1 \dots n)}) (⟨m, K⟩ PolyAP f \lor (K + 1) MonoAP f))$
14	13	imbi2d	$⊢ x = m \to ((φ \to \exists n \in ℕ \forall f \in (R^{(1 \dots n)}) (⟨x, K⟩ PolyAP f \lor (K + 1) MonoAP f)) \leftrightarrow (φ \to \exists n \in ℕ \forall f \in (R^{(1 \dots n)}) (⟨m, K⟩ PolyAP f \lor (K + 1) MonoAP f)))$
15		opeq1	$⊢ x = m + 1 \to ⟨x, K⟩ = ⟨m + 1, K⟩$
16	15	breq1d	$⊢ x = m + 1 \to (⟨x, K⟩ PolyAP f \leftrightarrow ⟨m + 1, K⟩ PolyAP f)$
17	16	orbi1d	$⊢ x = m + 1 \to ((⟨x, K⟩ PolyAP f \lor (K + 1) MonoAP f) \leftrightarrow (⟨m + 1, K⟩ PolyAP f \lor (K + 1) MonoAP f))$
18	17	rexralbidv	$⊢ x = m + 1 \to (\exists n \in ℕ \forall f \in (R^{(1 \dots n)}) (⟨x, K⟩ PolyAP f \lor (K + 1) MonoAP f) \leftrightarrow \exists n \in ℕ \forall f \in (R^{(1 \dots n)}) (⟨m + 1, K⟩ PolyAP f \lor (K + 1) MonoAP f))$
19	18	imbi2d	$⊢ x = m + 1 \to ((φ \to \exists n \in ℕ \forall f \in (R^{(1 \dots n)}) (⟨x, K⟩ PolyAP f \lor (K + 1) MonoAP f)) \leftrightarrow (φ \to \exists n \in ℕ \forall f \in (R^{(1 \dots n)}) (⟨m + 1, K⟩ PolyAP f \lor (K + 1) MonoAP f)))$
20		opeq1	$⊢ x = M \to ⟨x, K⟩ = ⟨M, K⟩$
21	20	breq1d	$⊢ x = M \to (⟨x, K⟩ PolyAP f \leftrightarrow ⟨M, K⟩ PolyAP f)$
22	21	orbi1d	$⊢ x = M \to ((⟨x, K⟩ PolyAP f \lor (K + 1) MonoAP f) \leftrightarrow (⟨M, K⟩ PolyAP f \lor (K + 1) MonoAP f))$
23	22	rexralbidv	$⊢ x = M \to (\exists n \in ℕ \forall f \in (R^{(1 \dots n)}) (⟨x, K⟩ PolyAP f \lor (K + 1) MonoAP f) \leftrightarrow \exists n \in ℕ \forall f \in (R^{(1 \dots n)}) (⟨M, K⟩ PolyAP f \lor (K + 1) MonoAP f))$
24	23	imbi2d	$⊢ x = M \to ((φ \to \exists n \in ℕ \forall f \in (R^{(1 \dots n)}) (⟨x, K⟩ PolyAP f \lor (K + 1) MonoAP f)) \leftrightarrow (φ \to \exists n \in ℕ \forall f \in (R^{(1 \dots n)}) (⟨M, K⟩ PolyAP f \lor (K + 1) MonoAP f)))$
25		oveq1	$⊢ s = R \to s^{(1 \dots n)} = R^{(1 \dots n)}$
26	25	raleqdv	$⊢ s = R \to (\forall f \in (s^{(1 \dots n)}) K MonoAP f \leftrightarrow \forall f \in (R^{(1 \dots n)}) K MonoAP f)$
27	26	rexbidv	$⊢ s = R \to (\exists n \in ℕ \forall f \in (s^{(1 \dots n)}) K MonoAP f \leftrightarrow \exists n \in ℕ \forall f \in (R^{(1 \dots n)}) K MonoAP f)$
28	27 3 1	rspcdva	$⊢ φ \to \exists n \in ℕ \forall f \in (R^{(1 \dots n)}) K MonoAP f$
29		oveq2	$⊢ n = w \to (1 \dots n) = (1 \dots w)$
30	29	oveq2d	$⊢ n = w \to R^{(1 \dots n)} = R^{(1 \dots w)}$
31	30	raleqdv	$⊢ n = w \to (\forall f \in (R^{(1 \dots n)}) K MonoAP f \leftrightarrow \forall f \in (R^{(1 \dots w)}) K MonoAP f)$
32	31	cbvrexvw	$⊢ \exists n \in ℕ \forall f \in (R^{(1 \dots n)}) K MonoAP f \leftrightarrow \exists w \in ℕ \forall f \in (R^{(1 \dots w)}) K MonoAP f$
33	28 32	sylib	$⊢ φ \to \exists w \in ℕ \forall f \in (R^{(1 \dots w)}) K MonoAP f$
34		breq2	$⊢ f = g \to (K MonoAP f \leftrightarrow K MonoAP g)$
35	34	cbvralvw	$⊢ \forall f \in (R^{(1 \dots w)}) K MonoAP f \leftrightarrow \forall g \in (R^{(1 \dots w)}) K MonoAP g$
36		2nn	$⊢ 2 \in ℕ$
37		simpr	$⊢ (φ \land w \in ℕ) \to w \in ℕ$
38		nnmulcl	$⊢ (2 \in ℕ \land w \in ℕ) \to 2 w \in ℕ$
39	36 37 38	sylancr	$⊢ (φ \land w \in ℕ) \to 2 w \in ℕ$
40	1	adantr	$⊢ (φ \land w \in ℕ) \to R \in Fin$
41		ovex	$⊢ (1 \dots 2 w) \in V$
42		elmapg	$⊢ (R \in Fin \land (1 \dots 2 w) \in V) \to (f \in (R^{(1 \dots 2 w)}) \leftrightarrow f : (1 \dots 2 w) ⟶ R)$
43	40 41 42	sylancl	$⊢ (φ \land w \in ℕ) \to (f \in (R^{(1 \dots 2 w)}) \leftrightarrow f : (1 \dots 2 w) ⟶ R)$
44	43	biimpa	$⊢ ((φ \land w \in ℕ) \land f \in (R^{(1 \dots 2 w)})) \to f : (1 \dots 2 w) ⟶ R$
45		simplr	$⊢ (((φ \land w \in ℕ) \land f : (1 \dots 2 w) ⟶ R) \land y \in (1 \dots w)) \to f : (1 \dots 2 w) ⟶ R$
46		elfznn	$⊢ y \in (1 \dots w) \to y \in ℕ$
47	46	adantl	$⊢ (((φ \land w \in ℕ) \land f : (1 \dots 2 w) ⟶ R) \land y \in (1 \dots w)) \to y \in ℕ$
48	47	nnred	$⊢ (((φ \land w \in ℕ) \land f : (1 \dots 2 w) ⟶ R) \land y \in (1 \dots w)) \to y \in ℝ$
49		simpllr	$⊢ (((φ \land w \in ℕ) \land f : (1 \dots 2 w) ⟶ R) \land y \in (1 \dots w)) \to w \in ℕ$
50	49	nnred	$⊢ (((φ \land w \in ℕ) \land f : (1 \dots 2 w) ⟶ R) \land y \in (1 \dots w)) \to w \in ℝ$
51		elfzle2	$⊢ y \in (1 \dots w) \to y \leq w$
52	51	adantl	$⊢ (((φ \land w \in ℕ) \land f : (1 \dots 2 w) ⟶ R) \land y \in (1 \dots w)) \to y \leq w$
53	48 50 50 52	leadd1dd	$⊢ (((φ \land w \in ℕ) \land f : (1 \dots 2 w) ⟶ R) \land y \in (1 \dots w)) \to y + w \leq w + w$
54	49	nncnd	$⊢ (((φ \land w \in ℕ) \land f : (1 \dots 2 w) ⟶ R) \land y \in (1 \dots w)) \to w \in ℂ$
55	54	2timesd	$⊢ (((φ \land w \in ℕ) \land f : (1 \dots 2 w) ⟶ R) \land y \in (1 \dots w)) \to 2 w = w + w$
56	53 55	breqtrrd	$⊢ (((φ \land w \in ℕ) \land f : (1 \dots 2 w) ⟶ R) \land y \in (1 \dots w)) \to y + w \leq 2 w$
57	47 49	nnaddcld	$⊢ (((φ \land w \in ℕ) \land f : (1 \dots 2 w) ⟶ R) \land y \in (1 \dots w)) \to y + w \in ℕ$
58		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
59	57 58	eleqtrdi	$⊢ (((φ \land w \in ℕ) \land f : (1 \dots 2 w) ⟶ R) \land y \in (1 \dots w)) \to y + w \in ℤ_{\geq 1}$
60	39	ad2antrr	$⊢ (((φ \land w \in ℕ) \land f : (1 \dots 2 w) ⟶ R) \land y \in (1 \dots w)) \to 2 w \in ℕ$
61	60	nnzd	$⊢ (((φ \land w \in ℕ) \land f : (1 \dots 2 w) ⟶ R) \land y \in (1 \dots w)) \to 2 w \in ℤ$
62		elfz5	$⊢ (y + w \in ℤ_{\geq 1} \land 2 w \in ℤ) \to (y + w \in (1 \dots 2 w) \leftrightarrow y + w \leq 2 w)$
63	59 61 62	syl2anc	$⊢ (((φ \land w \in ℕ) \land f : (1 \dots 2 w) ⟶ R) \land y \in (1 \dots w)) \to (y + w \in (1 \dots 2 w) \leftrightarrow y + w \leq 2 w)$
64	56 63	mpbird	$⊢ (((φ \land w \in ℕ) \land f : (1 \dots 2 w) ⟶ R) \land y \in (1 \dots w)) \to y + w \in (1 \dots 2 w)$
65	45 64	ffvelrnd	$⊢ (((φ \land w \in ℕ) \land f : (1 \dots 2 w) ⟶ R) \land y \in (1 \dots w)) \to f (y + w) \in R$
66		fvoveq1	$⊢ x = y \to f (x + w) = f (y + w)$
67	66	cbvmptv	$⊢ (x \in (1 \dots w) ⟼ f (x + w)) = (y \in (1 \dots w) ⟼ f (y + w))$
68	65 67	fmptd	$⊢ ((φ \land w \in ℕ) \land f : (1 \dots 2 w) ⟶ R) \to (x \in (1 \dots w) ⟼ f (x + w)) : (1 \dots w) ⟶ R$
69		ovex	$⊢ (1 \dots w) \in V$
70		elmapg	$⊢ (R \in Fin \land (1 \dots w) \in V) \to ((x \in (1 \dots w) ⟼ f (x + w)) \in (R^{(1 \dots w)}) \leftrightarrow (x \in (1 \dots w) ⟼ f (x + w)) : (1 \dots w) ⟶ R)$
71	40 69 70	sylancl	$⊢ (φ \land w \in ℕ) \to ((x \in (1 \dots w) ⟼ f (x + w)) \in (R^{(1 \dots w)}) \leftrightarrow (x \in (1 \dots w) ⟼ f (x + w)) : (1 \dots w) ⟶ R)$
72	71	biimpar	$⊢ ((φ \land w \in ℕ) \land (x \in (1 \dots w) ⟼ f (x + w)) : (1 \dots w) ⟶ R) \to (x \in (1 \dots w) ⟼ f (x + w)) \in (R^{(1 \dots w)})$
73	68 72	syldan	$⊢ ((φ \land w \in ℕ) \land f : (1 \dots 2 w) ⟶ R) \to (x \in (1 \dots w) ⟼ f (x + w)) \in (R^{(1 \dots w)})$
74		breq2	$⊢ g = (x \in (1 \dots w) ⟼ f (x + w)) \to (K MonoAP g \leftrightarrow K MonoAP (x \in (1 \dots w) ⟼ f (x + w)))$
75	74	rspcv	$⊢ (x \in (1 \dots w) ⟼ f (x + w)) \in (R^{(1 \dots w)}) \to (\forall g \in (R^{(1 \dots w)}) K MonoAP g \to K MonoAP (x \in (1 \dots w) ⟼ f (x + w)))$
76	73 75	syl	$⊢ ((φ \land w \in ℕ) \land f : (1 \dots 2 w) ⟶ R) \to (\forall g \in (R^{(1 \dots w)}) K MonoAP g \to K MonoAP (x \in (1 \dots w) ⟼ f (x + w)))$
77		2nn0	$⊢ 2 \in ℕ_{0}$
78	2	ad2antrr	$⊢ ((φ \land w \in ℕ) \land f : (1 \dots 2 w) ⟶ R) \to K \in ℤ_{\geq 2}$
79		eluznn0	$⊢ (2 \in ℕ_{0} \land K \in ℤ_{\geq 2}) \to K \in ℕ_{0}$
80	77 78 79	sylancr	$⊢ ((φ \land w \in ℕ) \land f : (1 \dots 2 w) ⟶ R) \to K \in ℕ_{0}$
81	69 80 68	vdwmc	$⊢ ((φ \land w \in ℕ) \land f : (1 \dots 2 w) ⟶ R) \to (K MonoAP (x \in (1 \dots w) ⟼ f (x + w)) \leftrightarrow \exists c \exists a \in ℕ \exists d \in ℕ a AP (K) d \subseteq {(x \in (1 \dots w) ⟼ f (x + w))}^{-1} [\{c\}])$
82	40	ad2antrr	$⊢ (((φ \land w \in ℕ) \land f : (1 \dots 2 w) ⟶ R) \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq {(x \in (1 \dots w) ⟼ f (x + w))}^{-1} [\{c\}])) \to R \in Fin$
83	78	adantr	$⊢ (((φ \land w \in ℕ) \land f : (1 \dots 2 w) ⟶ R) \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq {(x \in (1 \dots w) ⟼ f (x + w))}^{-1} [\{c\}])) \to K \in ℤ_{\geq 2}$
84		simpllr	$⊢ (((φ \land w \in ℕ) \land f : (1 \dots 2 w) ⟶ R) \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq {(x \in (1 \dots w) ⟼ f (x + w))}^{-1} [\{c\}])) \to w \in ℕ$
85		simplr	$⊢ (((φ \land w \in ℕ) \land f : (1 \dots 2 w) ⟶ R) \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq {(x \in (1 \dots w) ⟼ f (x + w))}^{-1} [\{c\}])) \to f : (1 \dots 2 w) ⟶ R$
86		vex	$⊢ c \in V$
87		simprll	$⊢ (((φ \land w \in ℕ) \land f : (1 \dots 2 w) ⟶ R) \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq {(x \in (1 \dots w) ⟼ f (x + w))}^{-1} [\{c\}])) \to a \in ℕ$
88		simprlr	$⊢ (((φ \land w \in ℕ) \land f : (1 \dots 2 w) ⟶ R) \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq {(x \in (1 \dots w) ⟼ f (x + w))}^{-1} [\{c\}])) \to d \in ℕ$
89		simprr	$⊢ (((φ \land w \in ℕ) \land f : (1 \dots 2 w) ⟶ R) \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq {(x \in (1 \dots w) ⟼ f (x + w))}^{-1} [\{c\}])) \to a AP (K) d \subseteq {(x \in (1 \dots w) ⟼ f (x + w))}^{-1} [\{c\}]$
90	82 83 84 85 86 87 88 89 67	vdwlem8	$⊢ (((φ \land w \in ℕ) \land f : (1 \dots 2 w) ⟶ R) \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq {(x \in (1 \dots w) ⟼ f (x + w))}^{-1} [\{c\}])) \to ⟨1, K⟩ PolyAP f$
91	90	orcd	$⊢ (((φ \land w \in ℕ) \land f : (1 \dots 2 w) ⟶ R) \land ((a \in ℕ \land d \in ℕ) \land a AP (K) d \subseteq {(x \in (1 \dots w) ⟼ f (x + w))}^{-1} [\{c\}])) \to (⟨1, K⟩ PolyAP f \lor (K + 1) MonoAP f)$
92	91	expr	$⊢ (((φ \land w \in ℕ) \land f : (1 \dots 2 w) ⟶ R) \land (a \in ℕ \land d \in ℕ)) \to (a AP (K) d \subseteq {(x \in (1 \dots w) ⟼ f (x + w))}^{-1} [\{c\}] \to (⟨1, K⟩ PolyAP f \lor (K + 1) MonoAP f))$
93	92	rexlimdvva	$⊢ ((φ \land w \in ℕ) \land f : (1 \dots 2 w) ⟶ R) \to (\exists a \in ℕ \exists d \in ℕ a AP (K) d \subseteq {(x \in (1 \dots w) ⟼ f (x + w))}^{-1} [\{c\}] \to (⟨1, K⟩ PolyAP f \lor (K + 1) MonoAP f))$
94	93	exlimdv	$⊢ ((φ \land w \in ℕ) \land f : (1 \dots 2 w) ⟶ R) \to (\exists c \exists a \in ℕ \exists d \in ℕ a AP (K) d \subseteq {(x \in (1 \dots w) ⟼ f (x + w))}^{-1} [\{c\}] \to (⟨1, K⟩ PolyAP f \lor (K + 1) MonoAP f))$
95	81 94	sylbid	$⊢ ((φ \land w \in ℕ) \land f : (1 \dots 2 w) ⟶ R) \to (K MonoAP (x \in (1 \dots w) ⟼ f (x + w)) \to (⟨1, K⟩ PolyAP f \lor (K + 1) MonoAP f))$
96	76 95	syld	$⊢ ((φ \land w \in ℕ) \land f : (1 \dots 2 w) ⟶ R) \to (\forall g \in (R^{(1 \dots w)}) K MonoAP g \to (⟨1, K⟩ PolyAP f \lor (K + 1) MonoAP f))$
97	44 96	syldan	$⊢ ((φ \land w \in ℕ) \land f \in (R^{(1 \dots 2 w)})) \to (\forall g \in (R^{(1 \dots w)}) K MonoAP g \to (⟨1, K⟩ PolyAP f \lor (K + 1) MonoAP f))$
98	97	ralrimdva	$⊢ (φ \land w \in ℕ) \to (\forall g \in (R^{(1 \dots w)}) K MonoAP g \to \forall f \in (R^{(1 \dots 2 w)}) (⟨1, K⟩ PolyAP f \lor (K + 1) MonoAP f))$
99		oveq2	$⊢ n = 2 w \to (1 \dots n) = (1 \dots 2 w)$
100	99	oveq2d	$⊢ n = 2 w \to R^{(1 \dots n)} = R^{(1 \dots 2 w)}$
101	100	raleqdv	$⊢ n = 2 w \to (\forall f \in (R^{(1 \dots n)}) (⟨1, K⟩ PolyAP f \lor (K + 1) MonoAP f) \leftrightarrow \forall f \in (R^{(1 \dots 2 w)}) (⟨1, K⟩ PolyAP f \lor (K + 1) MonoAP f))$
102	101	rspcev	$⊢ (2 w \in ℕ \land \forall f \in (R^{(1 \dots 2 w)}) (⟨1, K⟩ PolyAP f \lor (K + 1) MonoAP f)) \to \exists n \in ℕ \forall f \in (R^{(1 \dots n)}) (⟨1, K⟩ PolyAP f \lor (K + 1) MonoAP f)$
103	39 98 102	syl6an	$⊢ (φ \land w \in ℕ) \to (\forall g \in (R^{(1 \dots w)}) K MonoAP g \to \exists n \in ℕ \forall f \in (R^{(1 \dots n)}) (⟨1, K⟩ PolyAP f \lor (K + 1) MonoAP f))$
104	35 103	syl5bi	$⊢ (φ \land w \in ℕ) \to (\forall f \in (R^{(1 \dots w)}) K MonoAP f \to \exists n \in ℕ \forall f \in (R^{(1 \dots n)}) (⟨1, K⟩ PolyAP f \lor (K + 1) MonoAP f))$
105	104	rexlimdva	$⊢ φ \to (\exists w \in ℕ \forall f \in (R^{(1 \dots w)}) K MonoAP f \to \exists n \in ℕ \forall f \in (R^{(1 \dots n)}) (⟨1, K⟩ PolyAP f \lor (K + 1) MonoAP f))$
106	33 105	mpd	$⊢ φ \to \exists n \in ℕ \forall f \in (R^{(1 \dots n)}) (⟨1, K⟩ PolyAP f \lor (K + 1) MonoAP f)$
107		breq2	$⊢ f = g \to (⟨m, K⟩ PolyAP f \leftrightarrow ⟨m, K⟩ PolyAP g)$
108		breq2	$⊢ f = g \to ((K + 1) MonoAP f \leftrightarrow (K + 1) MonoAP g)$
109	107 108	orbi12d	$⊢ f = g \to ((⟨m, K⟩ PolyAP f \lor (K + 1) MonoAP f) \leftrightarrow (⟨m, K⟩ PolyAP g \lor (K + 1) MonoAP g))$
110	109	cbvralvw	$⊢ \forall f \in (R^{(1 \dots n)}) (⟨m, K⟩ PolyAP f \lor (K + 1) MonoAP f) \leftrightarrow \forall g \in (R^{(1 \dots n)}) (⟨m, K⟩ PolyAP g \lor (K + 1) MonoAP g)$
111	30	raleqdv	$⊢ n = w \to (\forall g \in (R^{(1 \dots n)}) (⟨m, K⟩ PolyAP g \lor (K + 1) MonoAP g) \leftrightarrow \forall g \in (R^{(1 \dots w)}) (⟨m, K⟩ PolyAP g \lor (K + 1) MonoAP g))$
112	110 111	syl5bb	$⊢ n = w \to (\forall f \in (R^{(1 \dots n)}) (⟨m, K⟩ PolyAP f \lor (K + 1) MonoAP f) \leftrightarrow \forall g \in (R^{(1 \dots w)}) (⟨m, K⟩ PolyAP g \lor (K + 1) MonoAP g))$
113	112	cbvrexvw	$⊢ \exists n \in ℕ \forall f \in (R^{(1 \dots n)}) (⟨m, K⟩ PolyAP f \lor (K + 1) MonoAP f) \leftrightarrow \exists w \in ℕ \forall g \in (R^{(1 \dots w)}) (⟨m, K⟩ PolyAP g \lor (K + 1) MonoAP g)$
114		oveq2	$⊢ n = v \to (1 \dots n) = (1 \dots v)$
115	114	oveq2d	$⊢ n = v \to s^{(1 \dots n)} = s^{(1 \dots v)}$
116	115	raleqdv	$⊢ n = v \to (\forall f \in (s^{(1 \dots n)}) K MonoAP f \leftrightarrow \forall f \in (s^{(1 \dots v)}) K MonoAP f)$
117	116	cbvrexvw	$⊢ \exists n \in ℕ \forall f \in (s^{(1 \dots n)}) K MonoAP f \leftrightarrow \exists v \in ℕ \forall f \in (s^{(1 \dots v)}) K MonoAP f$
118		oveq1	$⊢ s = R^{(1 \dots w)} \to s^{(1 \dots v)} = {(R^{(1 \dots w)})}^{(1 \dots v)}$
119	118	raleqdv	$⊢ s = R^{(1 \dots w)} \to (\forall f \in (s^{(1 \dots v)}) K MonoAP f \leftrightarrow \forall f \in ({(R^{(1 \dots w)})}^{(1 \dots v)}) K MonoAP f)$
120	119	rexbidv	$⊢ s = R^{(1 \dots w)} \to (\exists v \in ℕ \forall f \in (s^{(1 \dots v)}) K MonoAP f \leftrightarrow \exists v \in ℕ \forall f \in ({(R^{(1 \dots w)})}^{(1 \dots v)}) K MonoAP f)$
121	117 120	syl5bb	$⊢ s = R^{(1 \dots w)} \to (\exists n \in ℕ \forall f \in (s^{(1 \dots n)}) K MonoAP f \leftrightarrow \exists v \in ℕ \forall f \in ({(R^{(1 \dots w)})}^{(1 \dots v)}) K MonoAP f)$
122	3	ad2antrr	$⊢ ((φ \land m \in ℕ) \land (w \in ℕ \land \forall g \in (R^{(1 \dots w)}) (⟨m, K⟩ PolyAP g \lor (K + 1) MonoAP g))) \to \forall s \in Fin \exists n \in ℕ \forall f \in (s^{(1 \dots n)}) K MonoAP f$
123	1	ad2antrr	$⊢ ((φ \land m \in ℕ) \land (w \in ℕ \land \forall g \in (R^{(1 \dots w)}) (⟨m, K⟩ PolyAP g \lor (K + 1) MonoAP g))) \to R \in Fin$
124		fzfi	$⊢ (1 \dots w) \in Fin$
125		mapfi	$⊢ (R \in Fin \land (1 \dots w) \in Fin) \to R^{(1 \dots w)} \in Fin$
126	123 124 125	sylancl	$⊢ ((φ \land m \in ℕ) \land (w \in ℕ \land \forall g \in (R^{(1 \dots w)}) (⟨m, K⟩ PolyAP g \lor (K + 1) MonoAP g))) \to R^{(1 \dots w)} \in Fin$
127	121 122 126	rspcdva	$⊢ ((φ \land m \in ℕ) \land (w \in ℕ \land \forall g \in (R^{(1 \dots w)}) (⟨m, K⟩ PolyAP g \lor (K + 1) MonoAP g))) \to \exists v \in ℕ \forall f \in ({(R^{(1 \dots w)})}^{(1 \dots v)}) K MonoAP f$
128		simprll	$⊢ ((φ \land m \in ℕ) \land ((w \in ℕ \land \forall g \in (R^{(1 \dots w)}) (⟨m, K⟩ PolyAP g \lor (K + 1) MonoAP g)) \land (v \in ℕ \land \forall f \in ({(R^{(1 \dots w)})}^{(1 \dots v)}) K MonoAP f))) \to w \in ℕ$
129		simprrl	$⊢ ((φ \land m \in ℕ) \land ((w \in ℕ \land \forall g \in (R^{(1 \dots w)}) (⟨m, K⟩ PolyAP g \lor (K + 1) MonoAP g)) \land (v \in ℕ \land \forall f \in ({(R^{(1 \dots w)})}^{(1 \dots v)}) K MonoAP f))) \to v \in ℕ$
130		nnmulcl	$⊢ (2 \in ℕ \land v \in ℕ) \to 2 v \in ℕ$
131	36 130	mpan	$⊢ v \in ℕ \to 2 v \in ℕ$
132		nnmulcl	$⊢ (w \in ℕ \land 2 v \in ℕ) \to w 2 v \in ℕ$
133	131 132	sylan2	$⊢ (w \in ℕ \land v \in ℕ) \to w 2 v \in ℕ$
134	128 129 133	syl2anc	$⊢ ((φ \land m \in ℕ) \land ((w \in ℕ \land \forall g \in (R^{(1 \dots w)}) (⟨m, K⟩ PolyAP g \lor (K + 1) MonoAP g)) \land (v \in ℕ \land \forall f \in ({(R^{(1 \dots w)})}^{(1 \dots v)}) K MonoAP f))) \to w 2 v \in ℕ$
135		simp1l	$⊢ ((φ \land m \in ℕ) \land ((w \in ℕ \land \forall g \in (R^{(1 \dots w)}) (⟨m, K⟩ PolyAP g \lor (K + 1) MonoAP g)) \land (v \in ℕ \land \forall f \in ({(R^{(1 \dots w)})}^{(1 \dots v)}) K MonoAP f)) \land h \in (R^{(1 \dots w 2 v)})) \to φ$
136	135 1	syl	$⊢ ((φ \land m \in ℕ) \land ((w \in ℕ \land \forall g \in (R^{(1 \dots w)}) (⟨m, K⟩ PolyAP g \lor (K + 1) MonoAP g)) \land (v \in ℕ \land \forall f \in ({(R^{(1 \dots w)})}^{(1 \dots v)}) K MonoAP f)) \land h \in (R^{(1 \dots w 2 v)})) \to R \in Fin$
137	135 2	syl	$⊢ ((φ \land m \in ℕ) \land ((w \in ℕ \land \forall g \in (R^{(1 \dots w)}) (⟨m, K⟩ PolyAP g \lor (K + 1) MonoAP g)) \land (v \in ℕ \land \forall f \in ({(R^{(1 \dots w)})}^{(1 \dots v)}) K MonoAP f)) \land h \in (R^{(1 \dots w 2 v)})) \to K \in ℤ_{\geq 2}$
138	135 3	syl	$⊢ ((φ \land m \in ℕ) \land ((w \in ℕ \land \forall g \in (R^{(1 \dots w)}) (⟨m, K⟩ PolyAP g \lor (K + 1) MonoAP g)) \land (v \in ℕ \land \forall f \in ({(R^{(1 \dots w)})}^{(1 \dots v)}) K MonoAP f)) \land h \in (R^{(1 \dots w 2 v)})) \to \forall s \in Fin \exists n \in ℕ \forall f \in (s^{(1 \dots n)}) K MonoAP f$
139		simp1r	$⊢ ((φ \land m \in ℕ) \land ((w \in ℕ \land \forall g \in (R^{(1 \dots w)}) (⟨m, K⟩ PolyAP g \lor (K + 1) MonoAP g)) \land (v \in ℕ \land \forall f \in ({(R^{(1 \dots w)})}^{(1 \dots v)}) K MonoAP f)) \land h \in (R^{(1 \dots w 2 v)})) \to m \in ℕ$
140		simp2ll	$⊢ ((φ \land m \in ℕ) \land ((w \in ℕ \land \forall g \in (R^{(1 \dots w)}) (⟨m, K⟩ PolyAP g \lor (K + 1) MonoAP g)) \land (v \in ℕ \land \forall f \in ({(R^{(1 \dots w)})}^{(1 \dots v)}) K MonoAP f)) \land h \in (R^{(1 \dots w 2 v)})) \to w \in ℕ$
141		simp2lr	$⊢ ((φ \land m \in ℕ) \land ((w \in ℕ \land \forall g \in (R^{(1 \dots w)}) (⟨m, K⟩ PolyAP g \lor (K + 1) MonoAP g)) \land (v \in ℕ \land \forall f \in ({(R^{(1 \dots w)})}^{(1 \dots v)}) K MonoAP f)) \land h \in (R^{(1 \dots w 2 v)})) \to \forall g \in (R^{(1 \dots w)}) (⟨m, K⟩ PolyAP g \lor (K + 1) MonoAP g)$
142		breq2	$⊢ g = k \to (⟨m, K⟩ PolyAP g \leftrightarrow ⟨m, K⟩ PolyAP k)$
143		breq2	$⊢ g = k \to ((K + 1) MonoAP g \leftrightarrow (K + 1) MonoAP k)$
144	142 143	orbi12d	$⊢ g = k \to ((⟨m, K⟩ PolyAP g \lor (K + 1) MonoAP g) \leftrightarrow (⟨m, K⟩ PolyAP k \lor (K + 1) MonoAP k))$
145	144	cbvralvw	$⊢ \forall g \in (R^{(1 \dots w)}) (⟨m, K⟩ PolyAP g \lor (K + 1) MonoAP g) \leftrightarrow \forall k \in (R^{(1 \dots w)}) (⟨m, K⟩ PolyAP k \lor (K + 1) MonoAP k)$
146	141 145	sylib	$⊢ ((φ \land m \in ℕ) \land ((w \in ℕ \land \forall g \in (R^{(1 \dots w)}) (⟨m, K⟩ PolyAP g \lor (K + 1) MonoAP g)) \land (v \in ℕ \land \forall f \in ({(R^{(1 \dots w)})}^{(1 \dots v)}) K MonoAP f)) \land h \in (R^{(1 \dots w 2 v)})) \to \forall k \in (R^{(1 \dots w)}) (⟨m, K⟩ PolyAP k \lor (K + 1) MonoAP k)$
147		simp2rl	$⊢ ((φ \land m \in ℕ) \land ((w \in ℕ \land \forall g \in (R^{(1 \dots w)}) (⟨m, K⟩ PolyAP g \lor (K + 1) MonoAP g)) \land (v \in ℕ \land \forall f \in ({(R^{(1 \dots w)})}^{(1 \dots v)}) K MonoAP f)) \land h \in (R^{(1 \dots w 2 v)})) \to v \in ℕ$
148		simp2rr	$⊢ ((φ \land m \in ℕ) \land ((w \in ℕ \land \forall g \in (R^{(1 \dots w)}) (⟨m, K⟩ PolyAP g \lor (K + 1) MonoAP g)) \land (v \in ℕ \land \forall f \in ({(R^{(1 \dots w)})}^{(1 \dots v)}) K MonoAP f)) \land h \in (R^{(1 \dots w 2 v)})) \to \forall f \in ({(R^{(1 \dots w)})}^{(1 \dots v)}) K MonoAP f$
149		simp3	$⊢ ((φ \land m \in ℕ) \land ((w \in ℕ \land \forall g \in (R^{(1 \dots w)}) (⟨m, K⟩ PolyAP g \lor (K + 1) MonoAP g)) \land (v \in ℕ \land \forall f \in ({(R^{(1 \dots w)})}^{(1 \dots v)}) K MonoAP f)) \land h \in (R^{(1 \dots w 2 v)})) \to h \in (R^{(1 \dots w 2 v)})$
150		ovex	$⊢ (1 \dots w 2 v) \in V$
151		elmapg	$⊢ (R \in Fin \land (1 \dots w 2 v) \in V) \to (h \in (R^{(1 \dots w 2 v)}) \leftrightarrow h : (1 \dots w 2 v) ⟶ R)$
152	136 150 151	sylancl	$⊢ ((φ \land m \in ℕ) \land ((w \in ℕ \land \forall g \in (R^{(1 \dots w)}) (⟨m, K⟩ PolyAP g \lor (K + 1) MonoAP g)) \land (v \in ℕ \land \forall f \in ({(R^{(1 \dots w)})}^{(1 \dots v)}) K MonoAP f)) \land h \in (R^{(1 \dots w 2 v)})) \to (h \in (R^{(1 \dots w 2 v)}) \leftrightarrow h : (1 \dots w 2 v) ⟶ R)$
153	149 152	mpbid	$⊢ ((φ \land m \in ℕ) \land ((w \in ℕ \land \forall g \in (R^{(1 \dots w)}) (⟨m, K⟩ PolyAP g \lor (K + 1) MonoAP g)) \land (v \in ℕ \land \forall f \in ({(R^{(1 \dots w)})}^{(1 \dots v)}) K MonoAP f)) \land h \in (R^{(1 \dots w 2 v)})) \to h : (1 \dots w 2 v) ⟶ R$
154		fvoveq1	$⊢ y = u \to h (y + w (x - 1 + v)) = h (u + w (x - 1 + v))$
155	154	cbvmptv	$⊢ (y \in (1 \dots w) ⟼ h (y + w (x - 1 + v))) = (u \in (1 \dots w) ⟼ h (u + w (x - 1 + v)))$
156		oveq1	$⊢ x = z \to x - 1 = z - 1$
157	156	oveq1d	$⊢ x = z \to x - 1 + v = z - 1 + v$
158	157	oveq2d	$⊢ x = z \to w (x - 1 + v) = w (z - 1 + v)$
159	158	oveq2d	$⊢ x = z \to u + w (x - 1 + v) = u + w (z - 1 + v)$
160	159	fveq2d	$⊢ x = z \to h (u + w (x - 1 + v)) = h (u + w (z - 1 + v))$
161	160	mpteq2dv	$⊢ x = z \to (u \in (1 \dots w) ⟼ h (u + w (x - 1 + v))) = (u \in (1 \dots w) ⟼ h (u + w (z - 1 + v)))$
162	155 161	eqtrid	$⊢ x = z \to (y \in (1 \dots w) ⟼ h (y + w (x - 1 + v))) = (u \in (1 \dots w) ⟼ h (u + w (z - 1 + v)))$
163	162	cbvmptv	$⊢ (x \in (1 \dots v) ⟼ (y \in (1 \dots w) ⟼ h (y + w (x - 1 + v)))) = (z \in (1 \dots v) ⟼ (u \in (1 \dots w) ⟼ h (u + w (z - 1 + v))))$
164	136 137 138 139 140 146 147 148 153 163	vdwlem9	$⊢ ((φ \land m \in ℕ) \land ((w \in ℕ \land \forall g \in (R^{(1 \dots w)}) (⟨m, K⟩ PolyAP g \lor (K + 1) MonoAP g)) \land (v \in ℕ \land \forall f \in ({(R^{(1 \dots w)})}^{(1 \dots v)}) K MonoAP f)) \land h \in (R^{(1 \dots w 2 v)})) \to (⟨m + 1, K⟩ PolyAP h \lor (K + 1) MonoAP h)$
165	164	3expia	$⊢ ((φ \land m \in ℕ) \land ((w \in ℕ \land \forall g \in (R^{(1 \dots w)}) (⟨m, K⟩ PolyAP g \lor (K + 1) MonoAP g)) \land (v \in ℕ \land \forall f \in ({(R^{(1 \dots w)})}^{(1 \dots v)}) K MonoAP f))) \to (h \in (R^{(1 \dots w 2 v)}) \to (⟨m + 1, K⟩ PolyAP h \lor (K + 1) MonoAP h))$
166	165	ralrimiv	$⊢ ((φ \land m \in ℕ) \land ((w \in ℕ \land \forall g \in (R^{(1 \dots w)}) (⟨m, K⟩ PolyAP g \lor (K + 1) MonoAP g)) \land (v \in ℕ \land \forall f \in ({(R^{(1 \dots w)})}^{(1 \dots v)}) K MonoAP f))) \to \forall h \in (R^{(1 \dots w 2 v)}) (⟨m + 1, K⟩ PolyAP h \lor (K + 1) MonoAP h)$
167		oveq2	$⊢ n = w 2 v \to (1 \dots n) = (1 \dots w 2 v)$
168	167	oveq2d	$⊢ n = w 2 v \to R^{(1 \dots n)} = R^{(1 \dots w 2 v)}$
169	168	raleqdv	$⊢ n = w 2 v \to (\forall f \in (R^{(1 \dots n)}) (⟨m + 1, K⟩ PolyAP f \lor (K + 1) MonoAP f) \leftrightarrow \forall f \in (R^{(1 \dots w 2 v)}) (⟨m + 1, K⟩ PolyAP f \lor (K + 1) MonoAP f))$
170		breq2	$⊢ f = h \to (⟨m + 1, K⟩ PolyAP f \leftrightarrow ⟨m + 1, K⟩ PolyAP h)$
171		breq2	$⊢ f = h \to ((K + 1) MonoAP f \leftrightarrow (K + 1) MonoAP h)$
172	170 171	orbi12d	$⊢ f = h \to ((⟨m + 1, K⟩ PolyAP f \lor (K + 1) MonoAP f) \leftrightarrow (⟨m + 1, K⟩ PolyAP h \lor (K + 1) MonoAP h))$
173	172	cbvralvw	$⊢ \forall f \in (R^{(1 \dots w 2 v)}) (⟨m + 1, K⟩ PolyAP f \lor (K + 1) MonoAP f) \leftrightarrow \forall h \in (R^{(1 \dots w 2 v)}) (⟨m + 1, K⟩ PolyAP h \lor (K + 1) MonoAP h)$
174	169 173	bitrdi	$⊢ n = w 2 v \to (\forall f \in (R^{(1 \dots n)}) (⟨m + 1, K⟩ PolyAP f \lor (K + 1) MonoAP f) \leftrightarrow \forall h \in (R^{(1 \dots w 2 v)}) (⟨m + 1, K⟩ PolyAP h \lor (K + 1) MonoAP h))$
175	174	rspcev	$⊢ (w 2 v \in ℕ \land \forall h \in (R^{(1 \dots w 2 v)}) (⟨m + 1, K⟩ PolyAP h \lor (K + 1) MonoAP h)) \to \exists n \in ℕ \forall f \in (R^{(1 \dots n)}) (⟨m + 1, K⟩ PolyAP f \lor (K + 1) MonoAP f)$
176	134 166 175	syl2anc	$⊢ ((φ \land m \in ℕ) \land ((w \in ℕ \land \forall g \in (R^{(1 \dots w)}) (⟨m, K⟩ PolyAP g \lor (K + 1) MonoAP g)) \land (v \in ℕ \land \forall f \in ({(R^{(1 \dots w)})}^{(1 \dots v)}) K MonoAP f))) \to \exists n \in ℕ \forall f \in (R^{(1 \dots n)}) (⟨m + 1, K⟩ PolyAP f \lor (K + 1) MonoAP f)$
177	176	anassrs	$⊢ (((φ \land m \in ℕ) \land (w \in ℕ \land \forall g \in (R^{(1 \dots w)}) (⟨m, K⟩ PolyAP g \lor (K + 1) MonoAP g))) \land (v \in ℕ \land \forall f \in ({(R^{(1 \dots w)})}^{(1 \dots v)}) K MonoAP f)) \to \exists n \in ℕ \forall f \in (R^{(1 \dots n)}) (⟨m + 1, K⟩ PolyAP f \lor (K + 1) MonoAP f)$
178	127 177	rexlimddv	$⊢ ((φ \land m \in ℕ) \land (w \in ℕ \land \forall g \in (R^{(1 \dots w)}) (⟨m, K⟩ PolyAP g \lor (K + 1) MonoAP g))) \to \exists n \in ℕ \forall f \in (R^{(1 \dots n)}) (⟨m + 1, K⟩ PolyAP f \lor (K + 1) MonoAP f)$
179	178	rexlimdvaa	$⊢ (φ \land m \in ℕ) \to (\exists w \in ℕ \forall g \in (R^{(1 \dots w)}) (⟨m, K⟩ PolyAP g \lor (K + 1) MonoAP g) \to \exists n \in ℕ \forall f \in (R^{(1 \dots n)}) (⟨m + 1, K⟩ PolyAP f \lor (K + 1) MonoAP f))$
180	113 179	syl5bi	$⊢ (φ \land m \in ℕ) \to (\exists n \in ℕ \forall f \in (R^{(1 \dots n)}) (⟨m, K⟩ PolyAP f \lor (K + 1) MonoAP f) \to \exists n \in ℕ \forall f \in (R^{(1 \dots n)}) (⟨m + 1, K⟩ PolyAP f \lor (K + 1) MonoAP f))$
181	180	expcom	$⊢ m \in ℕ \to (φ \to (\exists n \in ℕ \forall f \in (R^{(1 \dots n)}) (⟨m, K⟩ PolyAP f \lor (K + 1) MonoAP f) \to \exists n \in ℕ \forall f \in (R^{(1 \dots n)}) (⟨m + 1, K⟩ PolyAP f \lor (K + 1) MonoAP f)))$
182	181	a2d	$⊢ m \in ℕ \to ((φ \to \exists n \in ℕ \forall f \in (R^{(1 \dots n)}) (⟨m, K⟩ PolyAP f \lor (K + 1) MonoAP f)) \to (φ \to \exists n \in ℕ \forall f \in (R^{(1 \dots n)}) (⟨m + 1, K⟩ PolyAP f \lor (K + 1) MonoAP f)))$
183	9 14 19 24 106 182	nnind	$⊢ M \in ℕ \to (φ \to \exists n \in ℕ \forall f \in (R^{(1 \dots n)}) (⟨M, K⟩ PolyAP f \lor (K + 1) MonoAP f))$
184	4 183	mpcom	$⊢ φ \to \exists n \in ℕ \forall f \in (R^{(1 \dots n)}) (⟨M, K⟩ PolyAP f \lor (K + 1) MonoAP f)$

Metamath Proof Explorer

Theorem vdwlem10

Proof