vdwlem1

	Ref	Expression
Hypotheses	vdwlem1.r	$⊢ φ \to R \in Fin$
	vdwlem1.k	$⊢ φ \to K \in ℕ$
	vdwlem1.w	$⊢ φ \to W \in ℕ$
	vdwlem1.f	$⊢ φ \to F : (1 \dots W) ⟶ R$
	vdwlem1.a	$⊢ φ \to A \in ℕ$
	vdwlem1.m	$⊢ φ \to M \in ℕ$
	vdwlem1.d	$⊢ φ \to D : (1 \dots M) ⟶ ℕ$
	vdwlem1.s	$⊢ φ \to \forall i \in (1 \dots M) (A + D (i)) AP (K) D (i) \subseteq F^{-1} [\{F (A + D (i))\}]$
	vdwlem1.i	$⊢ φ \to I \in (1 \dots M)$
	vdwlem1.e	$⊢ φ \to F (A) = F (A + D (I))$
Assertion	vdwlem1	$⊢ φ \to (K + 1) MonoAP F$

Proof

Step	Hyp	Ref	Expression
1		vdwlem1.r	$⊢ φ \to R \in Fin$
2		vdwlem1.k	$⊢ φ \to K \in ℕ$
3		vdwlem1.w	$⊢ φ \to W \in ℕ$
4		vdwlem1.f	$⊢ φ \to F : (1 \dots W) ⟶ R$
5		vdwlem1.a	$⊢ φ \to A \in ℕ$
6		vdwlem1.m	$⊢ φ \to M \in ℕ$
7		vdwlem1.d	$⊢ φ \to D : (1 \dots M) ⟶ ℕ$
8		vdwlem1.s	$⊢ φ \to \forall i \in (1 \dots M) (A + D (i)) AP (K) D (i) \subseteq F^{-1} [\{F (A + D (i))\}]$
9		vdwlem1.i	$⊢ φ \to I \in (1 \dots M)$
10		vdwlem1.e	$⊢ φ \to F (A) = F (A + D (I))$
11	7 9	ffvelrnd	$⊢ φ \to D (I) \in ℕ$
12	2	nnnn0d	$⊢ φ \to K \in ℕ_{0}$
13		vdwapun	$⊢ (K \in ℕ_{0} \land A \in ℕ \land D (I) \in ℕ) \to A AP (K + 1) D (I) = \{A\} \cup ((A + D (I)) AP (K) D (I))$
14	12 5 11 13	syl3anc	$⊢ φ \to A AP (K + 1) D (I) = \{A\} \cup ((A + D (I)) AP (K) D (I))$
15	5	nnred	$⊢ φ \to A \in ℝ$
16		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
17	6 16	eleqtrdi	$⊢ φ \to M \in ℤ_{\geq 1}$
18		eluzfz1	$⊢ M \in ℤ_{\geq 1} \to 1 \in (1 \dots M)$
19	17 18	syl	$⊢ φ \to 1 \in (1 \dots M)$
20	7 19	ffvelrnd	$⊢ φ \to D (1) \in ℕ$
21	5 20	nnaddcld	$⊢ φ \to A + D (1) \in ℕ$
22	21	nnred	$⊢ φ \to A + D (1) \in ℝ$
23	3	nnred	$⊢ φ \to W \in ℝ$
24	20	nnrpd	$⊢ φ \to D (1) \in ℝ^{+}$
25	15 24	ltaddrpd	$⊢ φ \to A < A + D (1)$
26	15 22 25	ltled	$⊢ φ \to A \leq A + D (1)$
27		fveq2	$⊢ i = 1 \to D (i) = D (1)$
28	27	oveq2d	$⊢ i = 1 \to A + D (i) = A + D (1)$
29	28	eleq1d	$⊢ i = 1 \to (A + D (i) \in (1 \dots W) \leftrightarrow A + D (1) \in (1 \dots W))$
30	8	r19.21bi	$⊢ (φ \land i \in (1 \dots M)) \to (A + D (i)) AP (K) D (i) \subseteq F^{-1} [\{F (A + D (i))\}]$
31		cnvimass	$⊢ F^{-1} [\{F (A + D (i))\}] \subseteq dom F$
32	31 4	fssdm	$⊢ φ \to F^{-1} [\{F (A + D (i))\}] \subseteq (1 \dots W)$
33	32	adantr	$⊢ (φ \land i \in (1 \dots M)) \to F^{-1} [\{F (A + D (i))\}] \subseteq (1 \dots W)$
34	30 33	sstrd	$⊢ (φ \land i \in (1 \dots M)) \to (A + D (i)) AP (K) D (i) \subseteq (1 \dots W)$
35		nnm1nn0	$⊢ K \in ℕ \to K - 1 \in ℕ_{0}$
36	2 35	syl	$⊢ φ \to K - 1 \in ℕ_{0}$
37		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
38	36 37	eleqtrdi	$⊢ φ \to K - 1 \in ℤ_{\geq 0}$
39		eluzfz1	$⊢ K - 1 \in ℤ_{\geq 0} \to 0 \in (0 \dots K - 1)$
40	38 39	syl	$⊢ φ \to 0 \in (0 \dots K - 1)$
41	40	adantr	$⊢ (φ \land i \in (1 \dots M)) \to 0 \in (0 \dots K - 1)$
42	7	ffvelrnda	$⊢ (φ \land i \in (1 \dots M)) \to D (i) \in ℕ$
43	42	nncnd	$⊢ (φ \land i \in (1 \dots M)) \to D (i) \in ℂ$
44	43	mul02d	$⊢ (φ \land i \in (1 \dots M)) \to 0 \cdot D (i) = 0$
45	44	oveq2d	$⊢ (φ \land i \in (1 \dots M)) \to A + D (i) + 0 \cdot D (i) = A + D (i) + 0$
46	5	adantr	$⊢ (φ \land i \in (1 \dots M)) \to A \in ℕ$
47	46 42	nnaddcld	$⊢ (φ \land i \in (1 \dots M)) \to A + D (i) \in ℕ$
48	47	nncnd	$⊢ (φ \land i \in (1 \dots M)) \to A + D (i) \in ℂ$
49	48	addid1d	$⊢ (φ \land i \in (1 \dots M)) \to A + D (i) + 0 = A + D (i)$
50	45 49	eqtr2d	$⊢ (φ \land i \in (1 \dots M)) \to A + D (i) = A + D (i) + 0 \cdot D (i)$
51		oveq1	$⊢ m = 0 \to m D (i) = 0 \cdot D (i)$
52	51	oveq2d	$⊢ m = 0 \to A + D (i) + m D (i) = A + D (i) + 0 \cdot D (i)$
53	52	rspceeqv	$⊢ (0 \in (0 \dots K - 1) \land A + D (i) = A + D (i) + 0 \cdot D (i)) \to \exists m \in (0 \dots K - 1) A + D (i) = A + D (i) + m D (i)$
54	41 50 53	syl2anc	$⊢ (φ \land i \in (1 \dots M)) \to \exists m \in (0 \dots K - 1) A + D (i) = A + D (i) + m D (i)$
55	2	adantr	$⊢ (φ \land i \in (1 \dots M)) \to K \in ℕ$
56	55	nnnn0d	$⊢ (φ \land i \in (1 \dots M)) \to K \in ℕ_{0}$
57		vdwapval	$⊢ (K \in ℕ_{0} \land A + D (i) \in ℕ \land D (i) \in ℕ) \to (A + D (i) \in ((A + D (i)) AP (K) D (i)) \leftrightarrow \exists m \in (0 \dots K - 1) A + D (i) = A + D (i) + m D (i))$
58	56 47 42 57	syl3anc	$⊢ (φ \land i \in (1 \dots M)) \to (A + D (i) \in ((A + D (i)) AP (K) D (i)) \leftrightarrow \exists m \in (0 \dots K - 1) A + D (i) = A + D (i) + m D (i))$
59	54 58	mpbird	$⊢ (φ \land i \in (1 \dots M)) \to A + D (i) \in ((A + D (i)) AP (K) D (i))$
60	34 59	sseldd	$⊢ (φ \land i \in (1 \dots M)) \to A + D (i) \in (1 \dots W)$
61	60	ralrimiva	$⊢ φ \to \forall i \in (1 \dots M) A + D (i) \in (1 \dots W)$
62	29 61 19	rspcdva	$⊢ φ \to A + D (1) \in (1 \dots W)$
63		elfzle2	$⊢ A + D (1) \in (1 \dots W) \to A + D (1) \leq W$
64	62 63	syl	$⊢ φ \to A + D (1) \leq W$
65	15 22 23 26 64	letrd	$⊢ φ \to A \leq W$
66	5 16	eleqtrdi	$⊢ φ \to A \in ℤ_{\geq 1}$
67	3	nnzd	$⊢ φ \to W \in ℤ$
68		elfz5	$⊢ (A \in ℤ_{\geq 1} \land W \in ℤ) \to (A \in (1 \dots W) \leftrightarrow A \leq W)$
69	66 67 68	syl2anc	$⊢ φ \to (A \in (1 \dots W) \leftrightarrow A \leq W)$
70	65 69	mpbird	$⊢ φ \to A \in (1 \dots W)$
71		eqidd	$⊢ φ \to F (A) = F (A)$
72		ffn	$⊢ F : (1 \dots W) ⟶ R \to F Fn (1 \dots W)$
73		fniniseg	$⊢ F Fn (1 \dots W) \to (A \in F^{-1} [\{F (A)\}] \leftrightarrow (A \in (1 \dots W) \land F (A) = F (A)))$
74	4 72 73	3syl	$⊢ φ \to (A \in F^{-1} [\{F (A)\}] \leftrightarrow (A \in (1 \dots W) \land F (A) = F (A)))$
75	70 71 74	mpbir2and	$⊢ φ \to A \in F^{-1} [\{F (A)\}]$
76	75	snssd	$⊢ φ \to \{A\} \subseteq F^{-1} [\{F (A)\}]$
77		fveq2	$⊢ i = I \to D (i) = D (I)$
78	77	oveq2d	$⊢ i = I \to A + D (i) = A + D (I)$
79	78 77	oveq12d	$⊢ i = I \to (A + D (i)) AP (K) D (i) = (A + D (I)) AP (K) D (I)$
80	78	fveq2d	$⊢ i = I \to F (A + D (i)) = F (A + D (I))$
81	80	sneqd	$⊢ i = I \to \{F (A + D (i))\} = \{F (A + D (I))\}$
82	81	imaeq2d	$⊢ i = I \to F^{-1} [\{F (A + D (i))\}] = F^{-1} [\{F (A + D (I))\}]$
83	79 82	sseq12d	$⊢ i = I \to ((A + D (i)) AP (K) D (i) \subseteq F^{-1} [\{F (A + D (i))\}] \leftrightarrow (A + D (I)) AP (K) D (I) \subseteq F^{-1} [\{F (A + D (I))\}])$
84	83 8 9	rspcdva	$⊢ φ \to (A + D (I)) AP (K) D (I) \subseteq F^{-1} [\{F (A + D (I))\}]$
85	10	sneqd	$⊢ φ \to \{F (A)\} = \{F (A + D (I))\}$
86	85	imaeq2d	$⊢ φ \to F^{-1} [\{F (A)\}] = F^{-1} [\{F (A + D (I))\}]$
87	84 86	sseqtrrd	$⊢ φ \to (A + D (I)) AP (K) D (I) \subseteq F^{-1} [\{F (A)\}]$
88	76 87	unssd	$⊢ φ \to \{A\} \cup ((A + D (I)) AP (K) D (I)) \subseteq F^{-1} [\{F (A)\}]$
89	14 88	eqsstrd	$⊢ φ \to A AP (K + 1) D (I) \subseteq F^{-1} [\{F (A)\}]$
90		oveq1	$⊢ a = A \to a AP (K + 1) d = A AP (K + 1) d$
91	90	sseq1d	$⊢ a = A \to (a AP (K + 1) d \subseteq F^{-1} [\{F (A)\}] \leftrightarrow A AP (K + 1) d \subseteq F^{-1} [\{F (A)\}])$
92		oveq2	$⊢ d = D (I) \to A AP (K + 1) d = A AP (K + 1) D (I)$
93	92	sseq1d	$⊢ d = D (I) \to (A AP (K + 1) d \subseteq F^{-1} [\{F (A)\}] \leftrightarrow A AP (K + 1) D (I) \subseteq F^{-1} [\{F (A)\}])$
94	91 93	rspc2ev	$⊢ (A \in ℕ \land D (I) \in ℕ \land A AP (K + 1) D (I) \subseteq F^{-1} [\{F (A)\}]) \to \exists a \in ℕ \exists d \in ℕ a AP (K + 1) d \subseteq F^{-1} [\{F (A)\}]$
95	5 11 89 94	syl3anc	$⊢ φ \to \exists a \in ℕ \exists d \in ℕ a AP (K + 1) d \subseteq F^{-1} [\{F (A)\}]$
96		fvex	$⊢ F (A) \in V$
97		sneq	$⊢ c = F (A) \to \{c\} = \{F (A)\}$
98	97	imaeq2d	$⊢ c = F (A) \to F^{-1} [\{c\}] = F^{-1} [\{F (A)\}]$
99	98	sseq2d	$⊢ c = F (A) \to (a AP (K + 1) d \subseteq F^{-1} [\{c\}] \leftrightarrow a AP (K + 1) d \subseteq F^{-1} [\{F (A)\}])$
100	99	2rexbidv	$⊢ c = F (A) \to (\exists a \in ℕ \exists d \in ℕ a AP (K + 1) d \subseteq F^{-1} [\{c\}] \leftrightarrow \exists a \in ℕ \exists d \in ℕ a AP (K + 1) d \subseteq F^{-1} [\{F (A)\}])$
101	96 100	spcev	$⊢ \exists a \in ℕ \exists d \in ℕ a AP (K + 1) d \subseteq F^{-1} [\{F (A)\}] \to \exists c \exists a \in ℕ \exists d \in ℕ a AP (K + 1) d \subseteq F^{-1} [\{c\}]$
102	95 101	syl	$⊢ φ \to \exists c \exists a \in ℕ \exists d \in ℕ a AP (K + 1) d \subseteq F^{-1} [\{c\}]$
103		ovex	$⊢ (1 \dots W) \in V$
104		peano2nn0	$⊢ K \in ℕ_{0} \to K + 1 \in ℕ_{0}$
105	12 104	syl	$⊢ φ \to K + 1 \in ℕ_{0}$
106	103 105 4	vdwmc	$⊢ φ \to ((K + 1) MonoAP F \leftrightarrow \exists c \exists a \in ℕ \exists d \in ℕ a AP (K + 1) d \subseteq F^{-1} [\{c\}])$
107	102 106	mpbird	$⊢ φ \to (K + 1) MonoAP F$

Metamath Proof Explorer

Theorem vdwlem1

Proof