vdwlem11

	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$
Assertion	vdwlem11	$⊢ φ \to \exists n \in ℕ \forall f \in (R^{(1 \dots n)}) (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		hashcl	$⊢ R \in Fin \to \|R\| \in ℕ_{0}$
5	1 4	syl	$⊢ φ \to \|R\| \in ℕ_{0}$
6		nn0p1nn	$⊢ \|R\| \in ℕ_{0} \to \|R\| + 1 \in ℕ$
7	5 6	syl	$⊢ φ \to \|R\| + 1 \in ℕ$
8	1 2 3 7	vdwlem10	$⊢ φ \to \exists n \in ℕ \forall f \in (R^{(1 \dots n)}) (⟨\|R\| + 1, K⟩ PolyAP f \lor (K + 1) MonoAP f)$
9	1	adantr	$⊢ (φ \land n \in ℕ) \to R \in Fin$
10		ovex	$⊢ (1 \dots n) \in V$
11		elmapg	$⊢ (R \in Fin \land (1 \dots n) \in V) \to (f \in (R^{(1 \dots n)}) \leftrightarrow f : (1 \dots n) ⟶ R)$
12	9 10 11	sylancl	$⊢ (φ \land n \in ℕ) \to (f \in (R^{(1 \dots n)}) \leftrightarrow f : (1 \dots n) ⟶ R)$
13	12	biimpa	$⊢ ((φ \land n \in ℕ) \land f \in (R^{(1 \dots n)})) \to f : (1 \dots n) ⟶ R$
14	5	nn0red	$⊢ φ \to \|R\| \in ℝ$
15	14	ltp1d	$⊢ φ \to \|R\| < \|R\| + 1$
16		peano2re	$⊢ \|R\| \in ℝ \to \|R\| + 1 \in ℝ$
17	14 16	syl	$⊢ φ \to \|R\| + 1 \in ℝ$
18	14 17	ltnled	$⊢ φ \to (\|R\| < \|R\| + 1 \leftrightarrow \neg \|R\| + 1 \leq \|R\|)$
19	15 18	mpbid	$⊢ φ \to \neg \|R\| + 1 \leq \|R\|$
20	19	adantr	$⊢ (φ \land (n \in ℕ \land f : (1 \dots n) ⟶ R)) \to \neg \|R\| + 1 \leq \|R\|$
21		eluz2nn	$⊢ K \in ℤ_{\geq 2} \to K \in ℕ$
22	2 21	syl	$⊢ φ \to K \in ℕ$
23	22	adantr	$⊢ (φ \land (n \in ℕ \land f : (1 \dots n) ⟶ R)) \to K \in ℕ$
24	23	nnnn0d	$⊢ (φ \land (n \in ℕ \land f : (1 \dots n) ⟶ R)) \to K \in ℕ_{0}$
25		simprr	$⊢ (φ \land (n \in ℕ \land f : (1 \dots n) ⟶ R)) \to f : (1 \dots n) ⟶ R$
26	7	adantr	$⊢ (φ \land (n \in ℕ \land f : (1 \dots n) ⟶ R)) \to \|R\| + 1 \in ℕ$
27		eqid	$⊢ (1 \dots \|R\| + 1) = (1 \dots \|R\| + 1)$
28	10 24 25 26 27	vdwpc	$⊢ (φ \land (n \in ℕ \land f : (1 \dots n) ⟶ R)) \to (⟨\|R\| + 1, K⟩ PolyAP f \leftrightarrow \exists a \in ℕ \exists d \in (ℕ^{(1 \dots \|R\| + 1)}) (\forall i \in (1 \dots \|R\| + 1) (a + d (i)) AP (K) d (i) \subseteq f^{-1} [\{f (a + d (i))\}] \land \|ran (i \in (1 \dots \|R\| + 1) ⟼ f (a + d (i)))\| = \|R\| + 1))$
29	1	ad3antrrr	$⊢ (((φ \land (n \in ℕ \land f : (1 \dots n) ⟶ R)) \land (a \in ℕ \land d \in (ℕ^{(1 \dots \|R\| + 1)}))) \land \forall i \in (1 \dots \|R\| + 1) (a + d (i)) AP (K) d (i) \subseteq f^{-1} [\{f (a + d (i))\}]) \to R \in Fin$
30	25	ad2antrr	$⊢ (((φ \land (n \in ℕ \land f : (1 \dots n) ⟶ R)) \land (a \in ℕ \land d \in (ℕ^{(1 \dots \|R\| + 1)}))) \land i \in (1 \dots \|R\| + 1)) \to f : (1 \dots n) ⟶ R$
31	25	ad3antrrr	$⊢ ((((φ \land (n \in ℕ \land f : (1 \dots n) ⟶ R)) \land (a \in ℕ \land d \in (ℕ^{(1 \dots \|R\| + 1)}))) \land i \in (1 \dots \|R\| + 1)) \land (a + d (i)) AP (K) d (i) \subseteq f^{-1} [\{f (a + d (i))\}]) \to f : (1 \dots n) ⟶ R$
32		simpr	$⊢ ((((φ \land (n \in ℕ \land f : (1 \dots n) ⟶ R)) \land (a \in ℕ \land d \in (ℕ^{(1 \dots \|R\| + 1)}))) \land i \in (1 \dots \|R\| + 1)) \land (a + d (i)) AP (K) d (i) \subseteq f^{-1} [\{f (a + d (i))\}]) \to (a + d (i)) AP (K) d (i) \subseteq f^{-1} [\{f (a + d (i))\}]$
33		cnvimass	$⊢ f^{-1} [\{f (a + d (i))\}] \subseteq dom f$
34	32 33	sstrdi	$⊢ ((((φ \land (n \in ℕ \land f : (1 \dots n) ⟶ R)) \land (a \in ℕ \land d \in (ℕ^{(1 \dots \|R\| + 1)}))) \land i \in (1 \dots \|R\| + 1)) \land (a + d (i)) AP (K) d (i) \subseteq f^{-1} [\{f (a + d (i))\}]) \to (a + d (i)) AP (K) d (i) \subseteq dom f$
35	31 34	fssdmd	$⊢ ((((φ \land (n \in ℕ \land f : (1 \dots n) ⟶ R)) \land (a \in ℕ \land d \in (ℕ^{(1 \dots \|R\| + 1)}))) \land i \in (1 \dots \|R\| + 1)) \land (a + d (i)) AP (K) d (i) \subseteq f^{-1} [\{f (a + d (i))\}]) \to (a + d (i)) AP (K) d (i) \subseteq (1 \dots n)$
36	22	ad3antrrr	$⊢ (((φ \land (n \in ℕ \land f : (1 \dots n) ⟶ R)) \land (a \in ℕ \land d \in (ℕ^{(1 \dots \|R\| + 1)}))) \land i \in (1 \dots \|R\| + 1)) \to K \in ℕ$
37		simplrl	$⊢ (((φ \land (n \in ℕ \land f : (1 \dots n) ⟶ R)) \land (a \in ℕ \land d \in (ℕ^{(1 \dots \|R\| + 1)}))) \land i \in (1 \dots \|R\| + 1)) \to a \in ℕ$
38		simprr	$⊢ ((φ \land (n \in ℕ \land f : (1 \dots n) ⟶ R)) \land (a \in ℕ \land d \in (ℕ^{(1 \dots \|R\| + 1)}))) \to d \in (ℕ^{(1 \dots \|R\| + 1)})$
39		nnex	$⊢ ℕ \in V$
40		ovex	$⊢ (1 \dots \|R\| + 1) \in V$
41	39 40	elmap	$⊢ d \in (ℕ^{(1 \dots \|R\| + 1)}) \leftrightarrow d : (1 \dots \|R\| + 1) ⟶ ℕ$
42	38 41	sylib	$⊢ ((φ \land (n \in ℕ \land f : (1 \dots n) ⟶ R)) \land (a \in ℕ \land d \in (ℕ^{(1 \dots \|R\| + 1)}))) \to d : (1 \dots \|R\| + 1) ⟶ ℕ$
43	42	ffvelcdmda	$⊢ (((φ \land (n \in ℕ \land f : (1 \dots n) ⟶ R)) \land (a \in ℕ \land d \in (ℕ^{(1 \dots \|R\| + 1)}))) \land i \in (1 \dots \|R\| + 1)) \to d (i) \in ℕ$
44	37 43	nnaddcld	$⊢ (((φ \land (n \in ℕ \land f : (1 \dots n) ⟶ R)) \land (a \in ℕ \land d \in (ℕ^{(1 \dots \|R\| + 1)}))) \land i \in (1 \dots \|R\| + 1)) \to a + d (i) \in ℕ$
45		vdwapid1	$⊢ (K \in ℕ \land a + d (i) \in ℕ \land d (i) \in ℕ) \to a + d (i) \in ((a + d (i)) AP (K) d (i))$
46	36 44 43 45	syl3anc	$⊢ (((φ \land (n \in ℕ \land f : (1 \dots n) ⟶ R)) \land (a \in ℕ \land d \in (ℕ^{(1 \dots \|R\| + 1)}))) \land i \in (1 \dots \|R\| + 1)) \to a + d (i) \in ((a + d (i)) AP (K) d (i))$
47	46	adantr	$⊢ ((((φ \land (n \in ℕ \land f : (1 \dots n) ⟶ R)) \land (a \in ℕ \land d \in (ℕ^{(1 \dots \|R\| + 1)}))) \land i \in (1 \dots \|R\| + 1)) \land (a + d (i)) AP (K) d (i) \subseteq f^{-1} [\{f (a + d (i))\}]) \to a + d (i) \in ((a + d (i)) AP (K) d (i))$
48	35 47	sseldd	$⊢ ((((φ \land (n \in ℕ \land f : (1 \dots n) ⟶ R)) \land (a \in ℕ \land d \in (ℕ^{(1 \dots \|R\| + 1)}))) \land i \in (1 \dots \|R\| + 1)) \land (a + d (i)) AP (K) d (i) \subseteq f^{-1} [\{f (a + d (i))\}]) \to a + d (i) \in (1 \dots n)$
49	48	ex	$⊢ (((φ \land (n \in ℕ \land f : (1 \dots n) ⟶ R)) \land (a \in ℕ \land d \in (ℕ^{(1 \dots \|R\| + 1)}))) \land i \in (1 \dots \|R\| + 1)) \to ((a + d (i)) AP (K) d (i) \subseteq f^{-1} [\{f (a + d (i))\}] \to a + d (i) \in (1 \dots n))$
50		ffvelcdm	$⊢ (f : (1 \dots n) ⟶ R \land a + d (i) \in (1 \dots n)) \to f (a + d (i)) \in R$
51	30 49 50	syl6an	$⊢ (((φ \land (n \in ℕ \land f : (1 \dots n) ⟶ R)) \land (a \in ℕ \land d \in (ℕ^{(1 \dots \|R\| + 1)}))) \land i \in (1 \dots \|R\| + 1)) \to ((a + d (i)) AP (K) d (i) \subseteq f^{-1} [\{f (a + d (i))\}] \to f (a + d (i)) \in R)$
52	51	ralimdva	$⊢ ((φ \land (n \in ℕ \land f : (1 \dots n) ⟶ R)) \land (a \in ℕ \land d \in (ℕ^{(1 \dots \|R\| + 1)}))) \to (\forall i \in (1 \dots \|R\| + 1) (a + d (i)) AP (K) d (i) \subseteq f^{-1} [\{f (a + d (i))\}] \to \forall i \in (1 \dots \|R\| + 1) f (a + d (i)) \in R)$
53	52	imp	$⊢ (((φ \land (n \in ℕ \land f : (1 \dots n) ⟶ R)) \land (a \in ℕ \land d \in (ℕ^{(1 \dots \|R\| + 1)}))) \land \forall i \in (1 \dots \|R\| + 1) (a + d (i)) AP (K) d (i) \subseteq f^{-1} [\{f (a + d (i))\}]) \to \forall i \in (1 \dots \|R\| + 1) f (a + d (i)) \in R$
54		eqid	$⊢ (i \in (1 \dots \|R\| + 1) ⟼ f (a + d (i))) = (i \in (1 \dots \|R\| + 1) ⟼ f (a + d (i)))$
55	54	fmpt	$⊢ \forall i \in (1 \dots \|R\| + 1) f (a + d (i)) \in R \leftrightarrow (i \in (1 \dots \|R\| + 1) ⟼ f (a + d (i))) : (1 \dots \|R\| + 1) ⟶ R$
56	53 55	sylib	$⊢ (((φ \land (n \in ℕ \land f : (1 \dots n) ⟶ R)) \land (a \in ℕ \land d \in (ℕ^{(1 \dots \|R\| + 1)}))) \land \forall i \in (1 \dots \|R\| + 1) (a + d (i)) AP (K) d (i) \subseteq f^{-1} [\{f (a + d (i))\}]) \to (i \in (1 \dots \|R\| + 1) ⟼ f (a + d (i))) : (1 \dots \|R\| + 1) ⟶ R$
57	56	frnd	$⊢ (((φ \land (n \in ℕ \land f : (1 \dots n) ⟶ R)) \land (a \in ℕ \land d \in (ℕ^{(1 \dots \|R\| + 1)}))) \land \forall i \in (1 \dots \|R\| + 1) (a + d (i)) AP (K) d (i) \subseteq f^{-1} [\{f (a + d (i))\}]) \to ran (i \in (1 \dots \|R\| + 1) ⟼ f (a + d (i))) \subseteq R$
58		ssdomg	$⊢ R \in Fin \to (ran (i \in (1 \dots \|R\| + 1) ⟼ f (a + d (i))) \subseteq R \to ran (i \in (1 \dots \|R\| + 1) ⟼ f (a + d (i))) ≼ R)$
59	29 57 58	sylc	$⊢ (((φ \land (n \in ℕ \land f : (1 \dots n) ⟶ R)) \land (a \in ℕ \land d \in (ℕ^{(1 \dots \|R\| + 1)}))) \land \forall i \in (1 \dots \|R\| + 1) (a + d (i)) AP (K) d (i) \subseteq f^{-1} [\{f (a + d (i))\}]) \to ran (i \in (1 \dots \|R\| + 1) ⟼ f (a + d (i))) ≼ R$
60	29 57	ssfid	$⊢ (((φ \land (n \in ℕ \land f : (1 \dots n) ⟶ R)) \land (a \in ℕ \land d \in (ℕ^{(1 \dots \|R\| + 1)}))) \land \forall i \in (1 \dots \|R\| + 1) (a + d (i)) AP (K) d (i) \subseteq f^{-1} [\{f (a + d (i))\}]) \to ran (i \in (1 \dots \|R\| + 1) ⟼ f (a + d (i))) \in Fin$
61		hashdom	$⊢ (ran (i \in (1 \dots \|R\| + 1) ⟼ f (a + d (i))) \in Fin \land R \in Fin) \to (\|ran (i \in (1 \dots \|R\| + 1) ⟼ f (a + d (i)))\| \leq \|R\| \leftrightarrow ran (i \in (1 \dots \|R\| + 1) ⟼ f (a + d (i))) ≼ R)$
62	60 29 61	syl2anc	$⊢ (((φ \land (n \in ℕ \land f : (1 \dots n) ⟶ R)) \land (a \in ℕ \land d \in (ℕ^{(1 \dots \|R\| + 1)}))) \land \forall i \in (1 \dots \|R\| + 1) (a + d (i)) AP (K) d (i) \subseteq f^{-1} [\{f (a + d (i))\}]) \to (\|ran (i \in (1 \dots \|R\| + 1) ⟼ f (a + d (i)))\| \leq \|R\| \leftrightarrow ran (i \in (1 \dots \|R\| + 1) ⟼ f (a + d (i))) ≼ R)$
63	59 62	mpbird	$⊢ (((φ \land (n \in ℕ \land f : (1 \dots n) ⟶ R)) \land (a \in ℕ \land d \in (ℕ^{(1 \dots \|R\| + 1)}))) \land \forall i \in (1 \dots \|R\| + 1) (a + d (i)) AP (K) d (i) \subseteq f^{-1} [\{f (a + d (i))\}]) \to \|ran (i \in (1 \dots \|R\| + 1) ⟼ f (a + d (i)))\| \leq \|R\|$
64		breq1	$⊢ \|ran (i \in (1 \dots \|R\| + 1) ⟼ f (a + d (i)))\| = \|R\| + 1 \to (\|ran (i \in (1 \dots \|R\| + 1) ⟼ f (a + d (i)))\| \leq \|R\| \leftrightarrow \|R\| + 1 \leq \|R\|)$
65	63 64	syl5ibcom	$⊢ (((φ \land (n \in ℕ \land f : (1 \dots n) ⟶ R)) \land (a \in ℕ \land d \in (ℕ^{(1 \dots \|R\| + 1)}))) \land \forall i \in (1 \dots \|R\| + 1) (a + d (i)) AP (K) d (i) \subseteq f^{-1} [\{f (a + d (i))\}]) \to (\|ran (i \in (1 \dots \|R\| + 1) ⟼ f (a + d (i)))\| = \|R\| + 1 \to \|R\| + 1 \leq \|R\|)$
66	65	expimpd	$⊢ ((φ \land (n \in ℕ \land f : (1 \dots n) ⟶ R)) \land (a \in ℕ \land d \in (ℕ^{(1 \dots \|R\| + 1)}))) \to ((\forall i \in (1 \dots \|R\| + 1) (a + d (i)) AP (K) d (i) \subseteq f^{-1} [\{f (a + d (i))\}] \land \|ran (i \in (1 \dots \|R\| + 1) ⟼ f (a + d (i)))\| = \|R\| + 1) \to \|R\| + 1 \leq \|R\|)$
67	66	rexlimdvva	$⊢ (φ \land (n \in ℕ \land f : (1 \dots n) ⟶ R)) \to (\exists a \in ℕ \exists d \in (ℕ^{(1 \dots \|R\| + 1)}) (\forall i \in (1 \dots \|R\| + 1) (a + d (i)) AP (K) d (i) \subseteq f^{-1} [\{f (a + d (i))\}] \land \|ran (i \in (1 \dots \|R\| + 1) ⟼ f (a + d (i)))\| = \|R\| + 1) \to \|R\| + 1 \leq \|R\|)$
68	28 67	sylbid	$⊢ (φ \land (n \in ℕ \land f : (1 \dots n) ⟶ R)) \to (⟨\|R\| + 1, K⟩ PolyAP f \to \|R\| + 1 \leq \|R\|)$
69	20 68	mtod	$⊢ (φ \land (n \in ℕ \land f : (1 \dots n) ⟶ R)) \to \neg ⟨\|R\| + 1, K⟩ PolyAP f$
70		biorf	$⊢ \neg ⟨\|R\| + 1, K⟩ PolyAP f \to ((K + 1) MonoAP f \leftrightarrow (⟨\|R\| + 1, K⟩ PolyAP f \lor (K + 1) MonoAP f))$
71	69 70	syl	$⊢ (φ \land (n \in ℕ \land f : (1 \dots n) ⟶ R)) \to ((K + 1) MonoAP f \leftrightarrow (⟨\|R\| + 1, K⟩ PolyAP f \lor (K + 1) MonoAP f))$
72	71	anassrs	$⊢ ((φ \land n \in ℕ) \land f : (1 \dots n) ⟶ R) \to ((K + 1) MonoAP f \leftrightarrow (⟨\|R\| + 1, K⟩ PolyAP f \lor (K + 1) MonoAP f))$
73	13 72	syldan	$⊢ ((φ \land n \in ℕ) \land f \in (R^{(1 \dots n)})) \to ((K + 1) MonoAP f \leftrightarrow (⟨\|R\| + 1, K⟩ PolyAP f \lor (K + 1) MonoAP f))$
74	73	ralbidva	$⊢ (φ \land n \in ℕ) \to (\forall f \in (R^{(1 \dots n)}) (K + 1) MonoAP f \leftrightarrow \forall f \in (R^{(1 \dots n)}) (⟨\|R\| + 1, K⟩ PolyAP f \lor (K + 1) MonoAP f))$
75	74	rexbidva	$⊢ φ \to (\exists n \in ℕ \forall f \in (R^{(1 \dots n)}) (K + 1) MonoAP f \leftrightarrow \exists n \in ℕ \forall f \in (R^{(1 \dots n)}) (⟨\|R\| + 1, K⟩ PolyAP f \lor (K + 1) MonoAP f))$
76	8 75	mpbird	$⊢ φ \to \exists n \in ℕ \forall f \in (R^{(1 \dots n)}) (K + 1) MonoAP f$

Metamath Proof Explorer

Theorem vdwlem11

Proof