vdwlem13

Description: Lemma for vdw . Main induction on K ; K = 0 , K = 1 base cases. (Contributed by Mario Carneiro, 18-Aug-2014)

	Ref	Expression
Hypotheses	vdw.r	$⊢ φ \to R \in Fin$
	vdw.k	$⊢ φ \to K \in ℕ_{0}$
Assertion	vdwlem13	$⊢ φ \to \exists n \in ℕ \forall f \in (R^{(1 \dots n)}) K MonoAP f$

Proof

Step	Hyp	Ref	Expression
1		vdw.r	$⊢ φ \to R \in Fin$
2		vdw.k	$⊢ φ \to K \in ℕ_{0}$
3		elnn1uz2	$⊢ K \in ℕ \leftrightarrow (K = 1 \lor K \in ℤ_{\geq 2})$
4		ovex	$⊢ (1 \dots 1) \in V$
5		elmapg	$⊢ (R \in Fin \land (1 \dots 1) \in V) \to (f \in (R^{(1 \dots 1)}) \leftrightarrow f : (1 \dots 1) ⟶ R)$
6	1 4 5	sylancl	$⊢ φ \to (f \in (R^{(1 \dots 1)}) \leftrightarrow f : (1 \dots 1) ⟶ R)$
7	6	biimpa	$⊢ (φ \land f \in (R^{(1 \dots 1)})) \to f : (1 \dots 1) ⟶ R$
8		1nn	$⊢ 1 \in ℕ$
9		vdwap1	$⊢ (1 \in ℕ \land 1 \in ℕ) \to 1 AP (1) 1 = \{1\}$
10	8 8 9	mp2an	$⊢ 1 AP (1) 1 = \{1\}$
11		1z	$⊢ 1 \in ℤ$
12		elfz3	$⊢ 1 \in ℤ \to 1 \in (1 \dots 1)$
13	11 12	mp1i	$⊢ (φ \land f : (1 \dots 1) ⟶ R) \to 1 \in (1 \dots 1)$
14		eqidd	$⊢ (φ \land f : (1 \dots 1) ⟶ R) \to f (1) = f (1)$
15		ffn	$⊢ f : (1 \dots 1) ⟶ R \to f Fn (1 \dots 1)$
16	15	adantl	$⊢ (φ \land f : (1 \dots 1) ⟶ R) \to f Fn (1 \dots 1)$
17		fniniseg	$⊢ f Fn (1 \dots 1) \to (1 \in f^{-1} [\{f (1)\}] \leftrightarrow (1 \in (1 \dots 1) \land f (1) = f (1)))$
18	16 17	syl	$⊢ (φ \land f : (1 \dots 1) ⟶ R) \to (1 \in f^{-1} [\{f (1)\}] \leftrightarrow (1 \in (1 \dots 1) \land f (1) = f (1)))$
19	13 14 18	mpbir2and	$⊢ (φ \land f : (1 \dots 1) ⟶ R) \to 1 \in f^{-1} [\{f (1)\}]$
20	19	snssd	$⊢ (φ \land f : (1 \dots 1) ⟶ R) \to \{1\} \subseteq f^{-1} [\{f (1)\}]$
21	10 20	eqsstrid	$⊢ (φ \land f : (1 \dots 1) ⟶ R) \to 1 AP (1) 1 \subseteq f^{-1} [\{f (1)\}]$
22	7 21	syldan	$⊢ (φ \land f \in (R^{(1 \dots 1)})) \to 1 AP (1) 1 \subseteq f^{-1} [\{f (1)\}]$
23	22	ralrimiva	$⊢ φ \to \forall f \in (R^{(1 \dots 1)}) 1 AP (1) 1 \subseteq f^{-1} [\{f (1)\}]$
24		fveq2	$⊢ K = 1 \to AP (K) = AP (1)$
25	24	oveqd	$⊢ K = 1 \to 1 AP (K) 1 = 1 AP (1) 1$
26	25	sseq1d	$⊢ K = 1 \to (1 AP (K) 1 \subseteq f^{-1} [\{f (1)\}] \leftrightarrow 1 AP (1) 1 \subseteq f^{-1} [\{f (1)\}])$
27	26	ralbidv	$⊢ K = 1 \to (\forall f \in (R^{(1 \dots 1)}) 1 AP (K) 1 \subseteq f^{-1} [\{f (1)\}] \leftrightarrow \forall f \in (R^{(1 \dots 1)}) 1 AP (1) 1 \subseteq f^{-1} [\{f (1)\}])$
28	23 27	syl5ibrcom	$⊢ φ \to (K = 1 \to \forall f \in (R^{(1 \dots 1)}) 1 AP (K) 1 \subseteq f^{-1} [\{f (1)\}])$
29		oveq1	$⊢ a = 1 \to a AP (K) d = 1 AP (K) d$
30	29	sseq1d	$⊢ a = 1 \to (a AP (K) d \subseteq f^{-1} [\{f (1)\}] \leftrightarrow 1 AP (K) d \subseteq f^{-1} [\{f (1)\}])$
31		oveq2	$⊢ d = 1 \to 1 AP (K) d = 1 AP (K) 1$
32	31	sseq1d	$⊢ d = 1 \to (1 AP (K) d \subseteq f^{-1} [\{f (1)\}] \leftrightarrow 1 AP (K) 1 \subseteq f^{-1} [\{f (1)\}])$
33	30 32	rspc2ev	$⊢ (1 \in ℕ \land 1 \in ℕ \land 1 AP (K) 1 \subseteq f^{-1} [\{f (1)\}]) \to \exists a \in ℕ \exists d \in ℕ a AP (K) d \subseteq f^{-1} [\{f (1)\}]$
34	8 8 33	mp3an12	$⊢ 1 AP (K) 1 \subseteq f^{-1} [\{f (1)\}] \to \exists a \in ℕ \exists d \in ℕ a AP (K) d \subseteq f^{-1} [\{f (1)\}]$
35		fvex	$⊢ f (1) \in V$
36		sneq	$⊢ c = f (1) \to \{c\} = \{f (1)\}$
37	36	imaeq2d	$⊢ c = f (1) \to f^{-1} [\{c\}] = f^{-1} [\{f (1)\}]$
38	37	sseq2d	$⊢ c = f (1) \to (a AP (K) d \subseteq f^{-1} [\{c\}] \leftrightarrow a AP (K) d \subseteq f^{-1} [\{f (1)\}])$
39	38	2rexbidv	$⊢ c = f (1) \to (\exists a \in ℕ \exists d \in ℕ a AP (K) d \subseteq f^{-1} [\{c\}] \leftrightarrow \exists a \in ℕ \exists d \in ℕ a AP (K) d \subseteq f^{-1} [\{f (1)\}])$
40	35 39	spcev	$⊢ \exists a \in ℕ \exists d \in ℕ a AP (K) d \subseteq f^{-1} [\{f (1)\}] \to \exists c \exists a \in ℕ \exists d \in ℕ a AP (K) d \subseteq f^{-1} [\{c\}]$
41	34 40	syl	$⊢ 1 AP (K) 1 \subseteq f^{-1} [\{f (1)\}] \to \exists c \exists a \in ℕ \exists d \in ℕ a AP (K) d \subseteq f^{-1} [\{c\}]$
42	2	adantr	$⊢ (φ \land f \in (R^{(1 \dots 1)})) \to K \in ℕ_{0}$
43	4 42 7	vdwmc	$⊢ (φ \land f \in (R^{(1 \dots 1)})) \to (K MonoAP f \leftrightarrow \exists c \exists a \in ℕ \exists d \in ℕ a AP (K) d \subseteq f^{-1} [\{c\}])$
44	41 43	syl5ibr	$⊢ (φ \land f \in (R^{(1 \dots 1)})) \to (1 AP (K) 1 \subseteq f^{-1} [\{f (1)\}] \to K MonoAP f)$
45	44	ralimdva	$⊢ φ \to (\forall f \in (R^{(1 \dots 1)}) 1 AP (K) 1 \subseteq f^{-1} [\{f (1)\}] \to \forall f \in (R^{(1 \dots 1)}) K MonoAP f)$
46		oveq2	$⊢ n = 1 \to (1 \dots n) = (1 \dots 1)$
47	46	oveq2d	$⊢ n = 1 \to R^{(1 \dots n)} = R^{(1 \dots 1)}$
48	47	raleqdv	$⊢ n = 1 \to (\forall f \in (R^{(1 \dots n)}) K MonoAP f \leftrightarrow \forall f \in (R^{(1 \dots 1)}) K MonoAP f)$
49	48	rspcev	$⊢ (1 \in ℕ \land \forall f \in (R^{(1 \dots 1)}) K MonoAP f) \to \exists n \in ℕ \forall f \in (R^{(1 \dots n)}) K MonoAP f$
50	8 49	mpan	$⊢ \forall f \in (R^{(1 \dots 1)}) K MonoAP f \to \exists n \in ℕ \forall f \in (R^{(1 \dots n)}) K MonoAP f$
51	45 50	syl6	$⊢ φ \to (\forall f \in (R^{(1 \dots 1)}) 1 AP (K) 1 \subseteq f^{-1} [\{f (1)\}] \to \exists n \in ℕ \forall f \in (R^{(1 \dots n)}) K MonoAP f)$
52	28 51	syld	$⊢ φ \to (K = 1 \to \exists n \in ℕ \forall f \in (R^{(1 \dots n)}) K MonoAP f)$
53		breq1	$⊢ x = 2 \to (x MonoAP f \leftrightarrow 2 MonoAP f)$
54	53	rexralbidv	$⊢ x = 2 \to (\exists n \in ℕ \forall f \in (r^{(1 \dots n)}) x MonoAP f \leftrightarrow \exists n \in ℕ \forall f \in (r^{(1 \dots n)}) 2 MonoAP f)$
55	54	ralbidv	$⊢ x = 2 \to (\forall r \in Fin \exists n \in ℕ \forall f \in (r^{(1 \dots n)}) x MonoAP f \leftrightarrow \forall r \in Fin \exists n \in ℕ \forall f \in (r^{(1 \dots n)}) 2 MonoAP f)$
56		breq1	$⊢ x = k \to (x MonoAP f \leftrightarrow k MonoAP f)$
57	56	rexralbidv	$⊢ x = k \to (\exists n \in ℕ \forall f \in (r^{(1 \dots n)}) x MonoAP f \leftrightarrow \exists n \in ℕ \forall f \in (r^{(1 \dots n)}) k MonoAP f)$
58	57	ralbidv	$⊢ x = k \to (\forall r \in Fin \exists n \in ℕ \forall f \in (r^{(1 \dots n)}) x MonoAP f \leftrightarrow \forall r \in Fin \exists n \in ℕ \forall f \in (r^{(1 \dots n)}) k MonoAP f)$
59		breq1	$⊢ x = k + 1 \to (x MonoAP f \leftrightarrow (k + 1) MonoAP f)$
60	59	rexralbidv	$⊢ x = k + 1 \to (\exists n \in ℕ \forall f \in (r^{(1 \dots n)}) x MonoAP f \leftrightarrow \exists n \in ℕ \forall f \in (r^{(1 \dots n)}) (k + 1) MonoAP f)$
61	60	ralbidv	$⊢ x = k + 1 \to (\forall r \in Fin \exists n \in ℕ \forall f \in (r^{(1 \dots n)}) x MonoAP f \leftrightarrow \forall r \in Fin \exists n \in ℕ \forall f \in (r^{(1 \dots n)}) (k + 1) MonoAP f)$
62		breq1	$⊢ x = K \to (x MonoAP f \leftrightarrow K MonoAP f)$
63	62	rexralbidv	$⊢ x = K \to (\exists n \in ℕ \forall f \in (r^{(1 \dots n)}) x MonoAP f \leftrightarrow \exists n \in ℕ \forall f \in (r^{(1 \dots n)}) K MonoAP f)$
64	63	ralbidv	$⊢ x = K \to (\forall r \in Fin \exists n \in ℕ \forall f \in (r^{(1 \dots n)}) x MonoAP f \leftrightarrow \forall r \in Fin \exists n \in ℕ \forall f \in (r^{(1 \dots n)}) K MonoAP f)$
65		hashcl	$⊢ r \in Fin \to \|r\| \in ℕ_{0}$
66		nn0p1nn	$⊢ \|r\| \in ℕ_{0} \to \|r\| + 1 \in ℕ$
67	65 66	syl	$⊢ r \in Fin \to \|r\| + 1 \in ℕ$
68		simpll	$⊢ ((r \in Fin \land f \in (r^{(1 \dots \|r\| + 1)})) \land \neg 2 MonoAP f) \to r \in Fin$
69		simplr	$⊢ ((r \in Fin \land f \in (r^{(1 \dots \|r\| + 1)})) \land \neg 2 MonoAP f) \to f \in (r^{(1 \dots \|r\| + 1)})$
70		vex	$⊢ r \in V$
71		ovex	$⊢ (1 \dots \|r\| + 1) \in V$
72	70 71	elmap	$⊢ f \in (r^{(1 \dots \|r\| + 1)}) \leftrightarrow f : (1 \dots \|r\| + 1) ⟶ r$
73	69 72	sylib	$⊢ ((r \in Fin \land f \in (r^{(1 \dots \|r\| + 1)})) \land \neg 2 MonoAP f) \to f : (1 \dots \|r\| + 1) ⟶ r$
74		simpr	$⊢ ((r \in Fin \land f \in (r^{(1 \dots \|r\| + 1)})) \land \neg 2 MonoAP f) \to \neg 2 MonoAP f$
75	68 73 74	vdwlem12	$⊢ \neg ((r \in Fin \land f \in (r^{(1 \dots \|r\| + 1)})) \land \neg 2 MonoAP f)$
76		iman	$⊢ ((r \in Fin \land f \in (r^{(1 \dots \|r\| + 1)})) \to 2 MonoAP f) \leftrightarrow \neg ((r \in Fin \land f \in (r^{(1 \dots \|r\| + 1)})) \land \neg 2 MonoAP f)$
77	75 76	mpbir	$⊢ (r \in Fin \land f \in (r^{(1 \dots \|r\| + 1)})) \to 2 MonoAP f$
78	77	ralrimiva	$⊢ r \in Fin \to \forall f \in (r^{(1 \dots \|r\| + 1)}) 2 MonoAP f$
79		oveq2	$⊢ n = \|r\| + 1 \to (1 \dots n) = (1 \dots \|r\| + 1)$
80	79	oveq2d	$⊢ n = \|r\| + 1 \to r^{(1 \dots n)} = r^{(1 \dots \|r\| + 1)}$
81	80	raleqdv	$⊢ n = \|r\| + 1 \to (\forall f \in (r^{(1 \dots n)}) 2 MonoAP f \leftrightarrow \forall f \in (r^{(1 \dots \|r\| + 1)}) 2 MonoAP f)$
82	81	rspcev	$⊢ (\|r\| + 1 \in ℕ \land \forall f \in (r^{(1 \dots \|r\| + 1)}) 2 MonoAP f) \to \exists n \in ℕ \forall f \in (r^{(1 \dots n)}) 2 MonoAP f$
83	67 78 82	syl2anc	$⊢ r \in Fin \to \exists n \in ℕ \forall f \in (r^{(1 \dots n)}) 2 MonoAP f$
84	83	rgen	$⊢ \forall r \in Fin \exists n \in ℕ \forall f \in (r^{(1 \dots n)}) 2 MonoAP f$
85		oveq1	$⊢ r = s \to r^{(1 \dots n)} = s^{(1 \dots n)}$
86	85	raleqdv	$⊢ r = s \to (\forall f \in (r^{(1 \dots n)}) k MonoAP f \leftrightarrow \forall f \in (s^{(1 \dots n)}) k MonoAP f)$
87	86	rexbidv	$⊢ r = s \to (\exists n \in ℕ \forall f \in (r^{(1 \dots n)}) k MonoAP f \leftrightarrow \exists n \in ℕ \forall f \in (s^{(1 \dots n)}) k MonoAP f)$
88		oveq2	$⊢ n = m \to (1 \dots n) = (1 \dots m)$
89	88	oveq2d	$⊢ n = m \to s^{(1 \dots n)} = s^{(1 \dots m)}$
90	89	raleqdv	$⊢ n = m \to (\forall f \in (s^{(1 \dots n)}) k MonoAP f \leftrightarrow \forall f \in (s^{(1 \dots m)}) k MonoAP f)$
91		breq2	$⊢ f = g \to (k MonoAP f \leftrightarrow k MonoAP g)$
92	91	cbvralvw	$⊢ \forall f \in (s^{(1 \dots m)}) k MonoAP f \leftrightarrow \forall g \in (s^{(1 \dots m)}) k MonoAP g$
93	90 92	bitrdi	$⊢ n = m \to (\forall f \in (s^{(1 \dots n)}) k MonoAP f \leftrightarrow \forall g \in (s^{(1 \dots m)}) k MonoAP g)$
94	93	cbvrexvw	$⊢ \exists n \in ℕ \forall f \in (s^{(1 \dots n)}) k MonoAP f \leftrightarrow \exists m \in ℕ \forall g \in (s^{(1 \dots m)}) k MonoAP g$
95	87 94	bitrdi	$⊢ r = s \to (\exists n \in ℕ \forall f \in (r^{(1 \dots n)}) k MonoAP f \leftrightarrow \exists m \in ℕ \forall g \in (s^{(1 \dots m)}) k MonoAP g)$
96	95	cbvralvw	$⊢ \forall r \in Fin \exists n \in ℕ \forall f \in (r^{(1 \dots n)}) k MonoAP f \leftrightarrow \forall s \in Fin \exists m \in ℕ \forall g \in (s^{(1 \dots m)}) k MonoAP g$
97		simplr	$⊢ ((k \in ℤ_{\geq 2} \land r \in Fin) \land \forall s \in Fin \exists m \in ℕ \forall g \in (s^{(1 \dots m)}) k MonoAP g) \to r \in Fin$
98		simpll	$⊢ ((k \in ℤ_{\geq 2} \land r \in Fin) \land \forall s \in Fin \exists m \in ℕ \forall g \in (s^{(1 \dots m)}) k MonoAP g) \to k \in ℤ_{\geq 2}$
99		simpr	$⊢ ((k \in ℤ_{\geq 2} \land r \in Fin) \land \forall s \in Fin \exists m \in ℕ \forall g \in (s^{(1 \dots m)}) k MonoAP g) \to \forall s \in Fin \exists m \in ℕ \forall g \in (s^{(1 \dots m)}) k MonoAP g$
100	94	ralbii	$⊢ \forall s \in Fin \exists n \in ℕ \forall f \in (s^{(1 \dots n)}) k MonoAP f \leftrightarrow \forall s \in Fin \exists m \in ℕ \forall g \in (s^{(1 \dots m)}) k MonoAP g$
101	99 100	sylibr	$⊢ ((k \in ℤ_{\geq 2} \land r \in Fin) \land \forall s \in Fin \exists m \in ℕ \forall g \in (s^{(1 \dots m)}) k MonoAP g) \to \forall s \in Fin \exists n \in ℕ \forall f \in (s^{(1 \dots n)}) k MonoAP f$
102	97 98 101	vdwlem11	$⊢ ((k \in ℤ_{\geq 2} \land r \in Fin) \land \forall s \in Fin \exists m \in ℕ \forall g \in (s^{(1 \dots m)}) k MonoAP g) \to \exists n \in ℕ \forall f \in (r^{(1 \dots n)}) (k + 1) MonoAP f$
103	102	ex	$⊢ (k \in ℤ_{\geq 2} \land r \in Fin) \to (\forall s \in Fin \exists m \in ℕ \forall g \in (s^{(1 \dots m)}) k MonoAP g \to \exists n \in ℕ \forall f \in (r^{(1 \dots n)}) (k + 1) MonoAP f)$
104	103	ralrimdva	$⊢ k \in ℤ_{\geq 2} \to (\forall s \in Fin \exists m \in ℕ \forall g \in (s^{(1 \dots m)}) k MonoAP g \to \forall r \in Fin \exists n \in ℕ \forall f \in (r^{(1 \dots n)}) (k + 1) MonoAP f)$
105	96 104	syl5bi	$⊢ k \in ℤ_{\geq 2} \to (\forall r \in Fin \exists n \in ℕ \forall f \in (r^{(1 \dots n)}) k MonoAP f \to \forall r \in Fin \exists n \in ℕ \forall f \in (r^{(1 \dots n)}) (k + 1) MonoAP f)$
106	55 58 61 64 84 105	uzind4i	$⊢ K \in ℤ_{\geq 2} \to \forall r \in Fin \exists n \in ℕ \forall f \in (r^{(1 \dots n)}) K MonoAP f$
107		oveq1	$⊢ r = R \to r^{(1 \dots n)} = R^{(1 \dots n)}$
108	107	raleqdv	$⊢ r = R \to (\forall f \in (r^{(1 \dots n)}) K MonoAP f \leftrightarrow \forall f \in (R^{(1 \dots n)}) K MonoAP f)$
109	108	rexbidv	$⊢ r = R \to (\exists n \in ℕ \forall f \in (r^{(1 \dots n)}) K MonoAP f \leftrightarrow \exists n \in ℕ \forall f \in (R^{(1 \dots n)}) K MonoAP f)$
110	109	rspcv	$⊢ R \in Fin \to (\forall r \in Fin \exists n \in ℕ \forall f \in (r^{(1 \dots n)}) K MonoAP f \to \exists n \in ℕ \forall f \in (R^{(1 \dots n)}) K MonoAP f)$
111	1 106 110	syl2im	$⊢ φ \to (K \in ℤ_{\geq 2} \to \exists n \in ℕ \forall f \in (R^{(1 \dots n)}) K MonoAP f)$
112	52 111	jaod	$⊢ φ \to ((K = 1 \lor K \in ℤ_{\geq 2}) \to \exists n \in ℕ \forall f \in (R^{(1 \dots n)}) K MonoAP f)$
113	3 112	syl5bi	$⊢ φ \to (K \in ℕ \to \exists n \in ℕ \forall f \in (R^{(1 \dots n)}) K MonoAP f)$
114		fveq2	$⊢ K = 0 \to AP (K) = AP (0)$
115	114	oveqd	$⊢ K = 0 \to 1 AP (K) 1 = 1 AP (0) 1$
116		vdwap0	$⊢ (1 \in ℕ \land 1 \in ℕ) \to 1 AP (0) 1 = \emptyset$
117	8 8 116	mp2an	$⊢ 1 AP (0) 1 = \emptyset$
118	115 117	eqtrdi	$⊢ K = 0 \to 1 AP (K) 1 = \emptyset$
119		0ss	$⊢ \emptyset \subseteq f^{-1} [\{f (1)\}]$
120	118 119	eqsstrdi	$⊢ K = 0 \to 1 AP (K) 1 \subseteq f^{-1} [\{f (1)\}]$
121	120	ralrimivw	$⊢ K = 0 \to \forall f \in (R^{(1 \dots 1)}) 1 AP (K) 1 \subseteq f^{-1} [\{f (1)\}]$
122	121 51	syl5	$⊢ φ \to (K = 0 \to \exists n \in ℕ \forall f \in (R^{(1 \dots n)}) K MonoAP f)$
123		elnn0	$⊢ K \in ℕ_{0} \leftrightarrow (K \in ℕ \lor K = 0)$
124	2 123	sylib	$⊢ φ \to (K \in ℕ \lor K = 0)$
125	113 122 124	mpjaod	$⊢ φ \to \exists n \in ℕ \forall f \in (R^{(1 \dots n)}) K MonoAP f$

Metamath Proof Explorer

Theorem vdwlem13

Proof