vdwlem12

Description: Lemma for vdw . K = 2 base case of induction. (Contributed by Mario Carneiro, 18-Aug-2014)

	Ref	Expression
Hypotheses	vdw.r	$⊢ φ \to R \in Fin$
	vdwlem12.f	$⊢ φ \to F : (1 \dots \|R\| + 1) ⟶ R$
	vdwlem12.2	$⊢ φ \to \neg 2 MonoAP F$
Assertion	vdwlem12	$⊢ \neg φ$

Proof

Step	Hyp	Ref	Expression
1		vdw.r	$⊢ φ \to R \in Fin$
2		vdwlem12.f	$⊢ φ \to F : (1 \dots \|R\| + 1) ⟶ R$
3		vdwlem12.2	$⊢ φ \to \neg 2 MonoAP F$
4		hashcl	$⊢ R \in Fin \to \|R\| \in ℕ_{0}$
5	1 4	syl	$⊢ φ \to \|R\| \in ℕ_{0}$
6	5	nn0red	$⊢ φ \to \|R\| \in ℝ$
7	6	ltp1d	$⊢ φ \to \|R\| < \|R\| + 1$
8		nn0p1nn	$⊢ \|R\| \in ℕ_{0} \to \|R\| + 1 \in ℕ$
9	5 8	syl	$⊢ φ \to \|R\| + 1 \in ℕ$
10	9	nnnn0d	$⊢ φ \to \|R\| + 1 \in ℕ_{0}$
11		hashfz1	$⊢ \|R\| + 1 \in ℕ_{0} \to \|(1 \dots \|R\| + 1)\| = \|R\| + 1$
12	10 11	syl	$⊢ φ \to \|(1 \dots \|R\| + 1)\| = \|R\| + 1$
13	7 12	breqtrrd	$⊢ φ \to \|R\| < \|(1 \dots \|R\| + 1)\|$
14		fzfi	$⊢ (1 \dots \|R\| + 1) \in Fin$
15		hashsdom	$⊢ (R \in Fin \land (1 \dots \|R\| + 1) \in Fin) \to (\|R\| < \|(1 \dots \|R\| + 1)\| \leftrightarrow R ≺ (1 \dots \|R\| + 1))$
16	1 14 15	sylancl	$⊢ φ \to (\|R\| < \|(1 \dots \|R\| + 1)\| \leftrightarrow R ≺ (1 \dots \|R\| + 1))$
17	13 16	mpbid	$⊢ φ \to R ≺ (1 \dots \|R\| + 1)$
18		fveq2	$⊢ z = x \to F (z) = F (x)$
19		fveq2	$⊢ w = y \to F (w) = F (y)$
20	18 19	eqeqan12d	$⊢ (z = x \land w = y) \to (F (z) = F (w) \leftrightarrow F (x) = F (y))$
21		eqeq12	$⊢ (z = x \land w = y) \to (z = w \leftrightarrow x = y)$
22	20 21	imbi12d	$⊢ (z = x \land w = y) \to ((F (z) = F (w) \to z = w) \leftrightarrow (F (x) = F (y) \to x = y))$
23		fveq2	$⊢ z = y \to F (z) = F (y)$
24		fveq2	$⊢ w = x \to F (w) = F (x)$
25	23 24	eqeqan12d	$⊢ (z = y \land w = x) \to (F (z) = F (w) \leftrightarrow F (y) = F (x))$
26		eqcom	$⊢ F (y) = F (x) \leftrightarrow F (x) = F (y)$
27	25 26	bitrdi	$⊢ (z = y \land w = x) \to (F (z) = F (w) \leftrightarrow F (x) = F (y))$
28		eqeq12	$⊢ (z = y \land w = x) \to (z = w \leftrightarrow y = x)$
29		eqcom	$⊢ y = x \leftrightarrow x = y$
30	28 29	bitrdi	$⊢ (z = y \land w = x) \to (z = w \leftrightarrow x = y)$
31	27 30	imbi12d	$⊢ (z = y \land w = x) \to ((F (z) = F (w) \to z = w) \leftrightarrow (F (x) = F (y) \to x = y))$
32		elfznn	$⊢ x \in (1 \dots \|R\| + 1) \to x \in ℕ$
33	32	nnred	$⊢ x \in (1 \dots \|R\| + 1) \to x \in ℝ$
34	33	ssriv	$⊢ (1 \dots \|R\| + 1) \subseteq ℝ$
35	34	a1i	$⊢ φ \to (1 \dots \|R\| + 1) \subseteq ℝ$
36		biidd	$⊢ (φ \land (x \in (1 \dots \|R\| + 1) \land y \in (1 \dots \|R\| + 1))) \to ((F (x) = F (y) \to x = y) \leftrightarrow (F (x) = F (y) \to x = y))$
37		simplr3	$⊢ ((φ \land (x \in (1 \dots \|R\| + 1) \land y \in (1 \dots \|R\| + 1) \land x \leq y)) \land F (x) = F (y)) \to x \leq y$
38	3	ad2antrr	$⊢ ((φ \land (x \in (1 \dots \|R\| + 1) \land y \in (1 \dots \|R\| + 1) \land x \leq y)) \land F (x) = F (y)) \to \neg 2 MonoAP F$
39		3simpa	$⊢ (x \in (1 \dots \|R\| + 1) \land y \in (1 \dots \|R\| + 1) \land x \leq y) \to (x \in (1 \dots \|R\| + 1) \land y \in (1 \dots \|R\| + 1))$
40		simplrl	$⊢ ((φ \land (x \in (1 \dots \|R\| + 1) \land y \in (1 \dots \|R\| + 1))) \land (F (x) = F (y) \land x < y)) \to x \in (1 \dots \|R\| + 1)$
41	40 32	syl	$⊢ ((φ \land (x \in (1 \dots \|R\| + 1) \land y \in (1 \dots \|R\| + 1))) \land (F (x) = F (y) \land x < y)) \to x \in ℕ$
42		simprr	$⊢ ((φ \land (x \in (1 \dots \|R\| + 1) \land y \in (1 \dots \|R\| + 1))) \land (F (x) = F (y) \land x < y)) \to x < y$
43		simplrr	$⊢ ((φ \land (x \in (1 \dots \|R\| + 1) \land y \in (1 \dots \|R\| + 1))) \land (F (x) = F (y) \land x < y)) \to y \in (1 \dots \|R\| + 1)$
44		elfznn	$⊢ y \in (1 \dots \|R\| + 1) \to y \in ℕ$
45	43 44	syl	$⊢ ((φ \land (x \in (1 \dots \|R\| + 1) \land y \in (1 \dots \|R\| + 1))) \land (F (x) = F (y) \land x < y)) \to y \in ℕ$
46		nnsub	$⊢ (x \in ℕ \land y \in ℕ) \to (x < y \leftrightarrow y - x \in ℕ)$
47	41 45 46	syl2anc	$⊢ ((φ \land (x \in (1 \dots \|R\| + 1) \land y \in (1 \dots \|R\| + 1))) \land (F (x) = F (y) \land x < y)) \to (x < y \leftrightarrow y - x \in ℕ)$
48	42 47	mpbid	$⊢ ((φ \land (x \in (1 \dots \|R\| + 1) \land y \in (1 \dots \|R\| + 1))) \land (F (x) = F (y) \land x < y)) \to y - x \in ℕ$
49		df-2	$⊢ 2 = 1 + 1$
50	49	fveq2i	$⊢ AP (2) = AP (1 + 1)$
51	50	oveqi	$⊢ x AP (2) (y - x) = x AP (1 + 1) (y - x)$
52		1nn0	$⊢ 1 \in ℕ_{0}$
53		vdwapun	$⊢ (1 \in ℕ_{0} \land x \in ℕ \land y - x \in ℕ) \to x AP (1 + 1) (y - x) = \{x\} \cup ((x + y - x) AP (1) (y - x))$
54	52 41 48 53	mp3an2i	$⊢ ((φ \land (x \in (1 \dots \|R\| + 1) \land y \in (1 \dots \|R\| + 1))) \land (F (x) = F (y) \land x < y)) \to x AP (1 + 1) (y - x) = \{x\} \cup ((x + y - x) AP (1) (y - x))$
55	51 54	eqtrid	$⊢ ((φ \land (x \in (1 \dots \|R\| + 1) \land y \in (1 \dots \|R\| + 1))) \land (F (x) = F (y) \land x < y)) \to x AP (2) (y - x) = \{x\} \cup ((x + y - x) AP (1) (y - x))$
56		simprl	$⊢ ((φ \land (x \in (1 \dots \|R\| + 1) \land y \in (1 \dots \|R\| + 1))) \land (F (x) = F (y) \land x < y)) \to F (x) = F (y)$
57	2	ad2antrr	$⊢ ((φ \land (x \in (1 \dots \|R\| + 1) \land y \in (1 \dots \|R\| + 1))) \land (F (x) = F (y) \land x < y)) \to F : (1 \dots \|R\| + 1) ⟶ R$
58	57	ffnd	$⊢ ((φ \land (x \in (1 \dots \|R\| + 1) \land y \in (1 \dots \|R\| + 1))) \land (F (x) = F (y) \land x < y)) \to F Fn (1 \dots \|R\| + 1)$
59		fniniseg	$⊢ F Fn (1 \dots \|R\| + 1) \to (x \in F^{-1} [\{F (y)\}] \leftrightarrow (x \in (1 \dots \|R\| + 1) \land F (x) = F (y)))$
60	58 59	syl	$⊢ ((φ \land (x \in (1 \dots \|R\| + 1) \land y \in (1 \dots \|R\| + 1))) \land (F (x) = F (y) \land x < y)) \to (x \in F^{-1} [\{F (y)\}] \leftrightarrow (x \in (1 \dots \|R\| + 1) \land F (x) = F (y)))$
61	40 56 60	mpbir2and	$⊢ ((φ \land (x \in (1 \dots \|R\| + 1) \land y \in (1 \dots \|R\| + 1))) \land (F (x) = F (y) \land x < y)) \to x \in F^{-1} [\{F (y)\}]$
62	61	snssd	$⊢ ((φ \land (x \in (1 \dots \|R\| + 1) \land y \in (1 \dots \|R\| + 1))) \land (F (x) = F (y) \land x < y)) \to \{x\} \subseteq F^{-1} [\{F (y)\}]$
63	41	nncnd	$⊢ ((φ \land (x \in (1 \dots \|R\| + 1) \land y \in (1 \dots \|R\| + 1))) \land (F (x) = F (y) \land x < y)) \to x \in ℂ$
64	45	nncnd	$⊢ ((φ \land (x \in (1 \dots \|R\| + 1) \land y \in (1 \dots \|R\| + 1))) \land (F (x) = F (y) \land x < y)) \to y \in ℂ$
65	63 64	pncan3d	$⊢ ((φ \land (x \in (1 \dots \|R\| + 1) \land y \in (1 \dots \|R\| + 1))) \land (F (x) = F (y) \land x < y)) \to x + y - x = y$
66	65	oveq1d	$⊢ ((φ \land (x \in (1 \dots \|R\| + 1) \land y \in (1 \dots \|R\| + 1))) \land (F (x) = F (y) \land x < y)) \to (x + y - x) AP (1) (y - x) = y AP (1) (y - x)$
67		vdwap1	$⊢ (y \in ℕ \land y - x \in ℕ) \to y AP (1) (y - x) = \{y\}$
68	45 48 67	syl2anc	$⊢ ((φ \land (x \in (1 \dots \|R\| + 1) \land y \in (1 \dots \|R\| + 1))) \land (F (x) = F (y) \land x < y)) \to y AP (1) (y - x) = \{y\}$
69	66 68	eqtrd	$⊢ ((φ \land (x \in (1 \dots \|R\| + 1) \land y \in (1 \dots \|R\| + 1))) \land (F (x) = F (y) \land x < y)) \to (x + y - x) AP (1) (y - x) = \{y\}$
70		eqidd	$⊢ ((φ \land (x \in (1 \dots \|R\| + 1) \land y \in (1 \dots \|R\| + 1))) \land (F (x) = F (y) \land x < y)) \to F (y) = F (y)$
71		fniniseg	$⊢ F Fn (1 \dots \|R\| + 1) \to (y \in F^{-1} [\{F (y)\}] \leftrightarrow (y \in (1 \dots \|R\| + 1) \land F (y) = F (y)))$
72	58 71	syl	$⊢ ((φ \land (x \in (1 \dots \|R\| + 1) \land y \in (1 \dots \|R\| + 1))) \land (F (x) = F (y) \land x < y)) \to (y \in F^{-1} [\{F (y)\}] \leftrightarrow (y \in (1 \dots \|R\| + 1) \land F (y) = F (y)))$
73	43 70 72	mpbir2and	$⊢ ((φ \land (x \in (1 \dots \|R\| + 1) \land y \in (1 \dots \|R\| + 1))) \land (F (x) = F (y) \land x < y)) \to y \in F^{-1} [\{F (y)\}]$
74	73	snssd	$⊢ ((φ \land (x \in (1 \dots \|R\| + 1) \land y \in (1 \dots \|R\| + 1))) \land (F (x) = F (y) \land x < y)) \to \{y\} \subseteq F^{-1} [\{F (y)\}]$
75	69 74	eqsstrd	$⊢ ((φ \land (x \in (1 \dots \|R\| + 1) \land y \in (1 \dots \|R\| + 1))) \land (F (x) = F (y) \land x < y)) \to (x + y - x) AP (1) (y - x) \subseteq F^{-1} [\{F (y)\}]$
76	62 75	unssd	$⊢ ((φ \land (x \in (1 \dots \|R\| + 1) \land y \in (1 \dots \|R\| + 1))) \land (F (x) = F (y) \land x < y)) \to \{x\} \cup ((x + y - x) AP (1) (y - x)) \subseteq F^{-1} [\{F (y)\}]$
77	55 76	eqsstrd	$⊢ ((φ \land (x \in (1 \dots \|R\| + 1) \land y \in (1 \dots \|R\| + 1))) \land (F (x) = F (y) \land x < y)) \to x AP (2) (y - x) \subseteq F^{-1} [\{F (y)\}]$
78		oveq1	$⊢ a = x \to a AP (2) d = x AP (2) d$
79	78	sseq1d	$⊢ a = x \to (a AP (2) d \subseteq F^{-1} [\{F (y)\}] \leftrightarrow x AP (2) d \subseteq F^{-1} [\{F (y)\}])$
80		oveq2	$⊢ d = y - x \to x AP (2) d = x AP (2) (y - x)$
81	80	sseq1d	$⊢ d = y - x \to (x AP (2) d \subseteq F^{-1} [\{F (y)\}] \leftrightarrow x AP (2) (y - x) \subseteq F^{-1} [\{F (y)\}])$
82	79 81	rspc2ev	$⊢ (x \in ℕ \land y - x \in ℕ \land x AP (2) (y - x) \subseteq F^{-1} [\{F (y)\}]) \to \exists a \in ℕ \exists d \in ℕ a AP (2) d \subseteq F^{-1} [\{F (y)\}]$
83	41 48 77 82	syl3anc	$⊢ ((φ \land (x \in (1 \dots \|R\| + 1) \land y \in (1 \dots \|R\| + 1))) \land (F (x) = F (y) \land x < y)) \to \exists a \in ℕ \exists d \in ℕ a AP (2) d \subseteq F^{-1} [\{F (y)\}]$
84		fvex	$⊢ F (y) \in V$
85		sneq	$⊢ c = F (y) \to \{c\} = \{F (y)\}$
86	85	imaeq2d	$⊢ c = F (y) \to F^{-1} [\{c\}] = F^{-1} [\{F (y)\}]$
87	86	sseq2d	$⊢ c = F (y) \to (a AP (2) d \subseteq F^{-1} [\{c\}] \leftrightarrow a AP (2) d \subseteq F^{-1} [\{F (y)\}])$
88	87	2rexbidv	$⊢ c = F (y) \to (\exists a \in ℕ \exists d \in ℕ a AP (2) d \subseteq F^{-1} [\{c\}] \leftrightarrow \exists a \in ℕ \exists d \in ℕ a AP (2) d \subseteq F^{-1} [\{F (y)\}])$
89	84 88	spcev	$⊢ \exists a \in ℕ \exists d \in ℕ a AP (2) d \subseteq F^{-1} [\{F (y)\}] \to \exists c \exists a \in ℕ \exists d \in ℕ a AP (2) d \subseteq F^{-1} [\{c\}]$
90	83 89	syl	$⊢ ((φ \land (x \in (1 \dots \|R\| + 1) \land y \in (1 \dots \|R\| + 1))) \land (F (x) = F (y) \land x < y)) \to \exists c \exists a \in ℕ \exists d \in ℕ a AP (2) d \subseteq F^{-1} [\{c\}]$
91		ovex	$⊢ (1 \dots \|R\| + 1) \in V$
92		2nn0	$⊢ 2 \in ℕ_{0}$
93	92	a1i	$⊢ ((φ \land (x \in (1 \dots \|R\| + 1) \land y \in (1 \dots \|R\| + 1))) \land (F (x) = F (y) \land x < y)) \to 2 \in ℕ_{0}$
94	91 93 57	vdwmc	$⊢ ((φ \land (x \in (1 \dots \|R\| + 1) \land y \in (1 \dots \|R\| + 1))) \land (F (x) = F (y) \land x < y)) \to (2 MonoAP F \leftrightarrow \exists c \exists a \in ℕ \exists d \in ℕ a AP (2) d \subseteq F^{-1} [\{c\}])$
95	90 94	mpbird	$⊢ ((φ \land (x \in (1 \dots \|R\| + 1) \land y \in (1 \dots \|R\| + 1))) \land (F (x) = F (y) \land x < y)) \to 2 MonoAP F$
96	39 95	sylanl2	$⊢ ((φ \land (x \in (1 \dots \|R\| + 1) \land y \in (1 \dots \|R\| + 1) \land x \leq y)) \land (F (x) = F (y) \land x < y)) \to 2 MonoAP F$
97	96	expr	$⊢ ((φ \land (x \in (1 \dots \|R\| + 1) \land y \in (1 \dots \|R\| + 1) \land x \leq y)) \land F (x) = F (y)) \to (x < y \to 2 MonoAP F)$
98	38 97	mtod	$⊢ ((φ \land (x \in (1 \dots \|R\| + 1) \land y \in (1 \dots \|R\| + 1) \land x \leq y)) \land F (x) = F (y)) \to \neg x < y$
99		simplr1	$⊢ ((φ \land (x \in (1 \dots \|R\| + 1) \land y \in (1 \dots \|R\| + 1) \land x \leq y)) \land F (x) = F (y)) \to x \in (1 \dots \|R\| + 1)$
100	99 33	syl	$⊢ ((φ \land (x \in (1 \dots \|R\| + 1) \land y \in (1 \dots \|R\| + 1) \land x \leq y)) \land F (x) = F (y)) \to x \in ℝ$
101		simplr2	$⊢ ((φ \land (x \in (1 \dots \|R\| + 1) \land y \in (1 \dots \|R\| + 1) \land x \leq y)) \land F (x) = F (y)) \to y \in (1 \dots \|R\| + 1)$
102	34 101	sselid	$⊢ ((φ \land (x \in (1 \dots \|R\| + 1) \land y \in (1 \dots \|R\| + 1) \land x \leq y)) \land F (x) = F (y)) \to y \in ℝ$
103	100 102	eqleltd	$⊢ ((φ \land (x \in (1 \dots \|R\| + 1) \land y \in (1 \dots \|R\| + 1) \land x \leq y)) \land F (x) = F (y)) \to (x = y \leftrightarrow (x \leq y \land \neg x < y))$
104	37 98 103	mpbir2and	$⊢ ((φ \land (x \in (1 \dots \|R\| + 1) \land y \in (1 \dots \|R\| + 1) \land x \leq y)) \land F (x) = F (y)) \to x = y$
105	104	ex	$⊢ (φ \land (x \in (1 \dots \|R\| + 1) \land y \in (1 \dots \|R\| + 1) \land x \leq y)) \to (F (x) = F (y) \to x = y)$
106	22 31 35 36 105	wlogle	$⊢ (φ \land (x \in (1 \dots \|R\| + 1) \land y \in (1 \dots \|R\| + 1))) \to (F (x) = F (y) \to x = y)$
107	106	ralrimivva	$⊢ φ \to \forall x \in (1 \dots \|R\| + 1) \forall y \in (1 \dots \|R\| + 1) (F (x) = F (y) \to x = y)$
108		dff13	$⊢ F : (1 \dots \|R\| + 1) \underset{1-1}{⟶} R \leftrightarrow (F : (1 \dots \|R\| + 1) ⟶ R \land \forall x \in (1 \dots \|R\| + 1) \forall y \in (1 \dots \|R\| + 1) (F (x) = F (y) \to x = y))$
109	2 107 108	sylanbrc	$⊢ φ \to F : (1 \dots \|R\| + 1) \underset{1-1}{⟶} R$
110		f1domg	$⊢ R \in Fin \to (F : (1 \dots \|R\| + 1) \underset{1-1}{⟶} R \to (1 \dots \|R\| + 1) ≼ R)$
111	1 109 110	sylc	$⊢ φ \to (1 \dots \|R\| + 1) ≼ R$
112		domnsym	$⊢ (1 \dots \|R\| + 1) ≼ R \to \neg R ≺ (1 \dots \|R\| + 1)$
113	111 112	syl	$⊢ φ \to \neg R ≺ (1 \dots \|R\| + 1)$
114	17 113	pm2.65i	$⊢ \neg φ$

Metamath Proof Explorer

Theorem vdwlem12

Proof