dedekindle

Description: The Dedekind cut theorem, with the hypothesis weakened to only require non-strict less than. (Contributed by Scott Fenton, 2-Jul-2013)

		Ref	Expression
	Assertion	dedekindle	$⊢ (A \subseteq ℝ \land B \subseteq ℝ \land \forall x \in A \forall y \in B x \leq y) \to \exists z \in ℝ \forall x \in A \forall y \in B (x \leq z \land z \leq y)$

Proof

Step	Hyp	Ref	Expression
1		simpr1	$⊢ (A \cap B = \emptyset \land (A \subseteq ℝ \land B \subseteq ℝ \land \forall x \in A \forall y \in B x \leq y)) \to A \subseteq ℝ$
2		simpr2	$⊢ (A \cap B = \emptyset \land (A \subseteq ℝ \land B \subseteq ℝ \land \forall x \in A \forall y \in B x \leq y)) \to B \subseteq ℝ$
3		simp1	$⊢ (A \cap B = \emptyset \land A \subseteq ℝ \land B \subseteq ℝ) \to A \cap B = \emptyset$
4		simpl	$⊢ (x \in A \land y \in B) \to x \in A$
5		disjel	$⊢ (A \cap B = \emptyset \land x \in A) \to \neg x \in B$
6	3 4 5	syl2an	$⊢ ((A \cap B = \emptyset \land A \subseteq ℝ \land B \subseteq ℝ) \land (x \in A \land y \in B)) \to \neg x \in B$
7		eleq1w	$⊢ y = x \to (y \in B \leftrightarrow x \in B)$
8	7	biimpcd	$⊢ y \in B \to (y = x \to x \in B)$
9	8	necon3bd	$⊢ y \in B \to (\neg x \in B \to y \neq x)$
10	9	ad2antll	$⊢ ((A \cap B = \emptyset \land A \subseteq ℝ \land B \subseteq ℝ) \land (x \in A \land y \in B)) \to (\neg x \in B \to y \neq x)$
11	6 10	mpd	$⊢ ((A \cap B = \emptyset \land A \subseteq ℝ \land B \subseteq ℝ) \land (x \in A \land y \in B)) \to y \neq x$
12		simp2	$⊢ (A \cap B = \emptyset \land A \subseteq ℝ \land B \subseteq ℝ) \to A \subseteq ℝ$
13		ssel2	$⊢ (A \subseteq ℝ \land x \in A) \to x \in ℝ$
14	12 4 13	syl2an	$⊢ ((A \cap B = \emptyset \land A \subseteq ℝ \land B \subseteq ℝ) \land (x \in A \land y \in B)) \to x \in ℝ$
15		simp3	$⊢ (A \cap B = \emptyset \land A \subseteq ℝ \land B \subseteq ℝ) \to B \subseteq ℝ$
16		simpr	$⊢ (x \in A \land y \in B) \to y \in B$
17		ssel2	$⊢ (B \subseteq ℝ \land y \in B) \to y \in ℝ$
18	15 16 17	syl2an	$⊢ ((A \cap B = \emptyset \land A \subseteq ℝ \land B \subseteq ℝ) \land (x \in A \land y \in B)) \to y \in ℝ$
19	14 18	ltlend	$⊢ ((A \cap B = \emptyset \land A \subseteq ℝ \land B \subseteq ℝ) \land (x \in A \land y \in B)) \to (x < y \leftrightarrow (x \leq y \land y \neq x))$
20	19	biimprd	$⊢ ((A \cap B = \emptyset \land A \subseteq ℝ \land B \subseteq ℝ) \land (x \in A \land y \in B)) \to ((x \leq y \land y \neq x) \to x < y)$
21	11 20	mpan2d	$⊢ ((A \cap B = \emptyset \land A \subseteq ℝ \land B \subseteq ℝ) \land (x \in A \land y \in B)) \to (x \leq y \to x < y)$
22	21	ralimdvva	$⊢ (A \cap B = \emptyset \land A \subseteq ℝ \land B \subseteq ℝ) \to (\forall x \in A \forall y \in B x \leq y \to \forall x \in A \forall y \in B x < y)$
23	22	3exp	$⊢ A \cap B = \emptyset \to (A \subseteq ℝ \to (B \subseteq ℝ \to (\forall x \in A \forall y \in B x \leq y \to \forall x \in A \forall y \in B x < y)))$
24	23	3imp2	$⊢ (A \cap B = \emptyset \land (A \subseteq ℝ \land B \subseteq ℝ \land \forall x \in A \forall y \in B x \leq y)) \to \forall x \in A \forall y \in B x < y$
25		dedekind	$⊢ (A \subseteq ℝ \land B \subseteq ℝ \land \forall x \in A \forall y \in B x < y) \to \exists z \in ℝ \forall x \in A \forall y \in B (x \leq z \land z \leq y)$
26	1 2 24 25	syl3anc	$⊢ (A \cap B = \emptyset \land (A \subseteq ℝ \land B \subseteq ℝ \land \forall x \in A \forall y \in B x \leq y)) \to \exists z \in ℝ \forall x \in A \forall y \in B (x \leq z \land z \leq y)$
27	26	ex	$⊢ A \cap B = \emptyset \to ((A \subseteq ℝ \land B \subseteq ℝ \land \forall x \in A \forall y \in B x \leq y) \to \exists z \in ℝ \forall x \in A \forall y \in B (x \leq z \land z \leq y))$
28		n0	$⊢ A \cap B \neq \emptyset \leftrightarrow \exists w w \in (A \cap B)$
29		simp1	$⊢ (A \subseteq ℝ \land B \subseteq ℝ \land \forall x \in A \forall y \in B x \leq y) \to A \subseteq ℝ$
30		elinel1	$⊢ w \in (A \cap B) \to w \in A$
31		ssel2	$⊢ (A \subseteq ℝ \land w \in A) \to w \in ℝ$
32	29 30 31	syl2an	$⊢ ((A \subseteq ℝ \land B \subseteq ℝ \land \forall x \in A \forall y \in B x \leq y) \land w \in (A \cap B)) \to w \in ℝ$
33		nfv	$⊢ Ⅎ x A \subseteq ℝ$
34		nfv	$⊢ Ⅎ x B \subseteq ℝ$
35		nfra1	$⊢ Ⅎ x \forall x \in A \forall y \in B x \leq y$
36	33 34 35	nf3an	$⊢ Ⅎ x (A \subseteq ℝ \land B \subseteq ℝ \land \forall x \in A \forall y \in B x \leq y)$
37		nfv	$⊢ Ⅎ x w \in (A \cap B)$
38	36 37	nfan	$⊢ Ⅎ x ((A \subseteq ℝ \land B \subseteq ℝ \land \forall x \in A \forall y \in B x \leq y) \land w \in (A \cap B))$
39		nfv	$⊢ Ⅎ y A \subseteq ℝ$
40		nfv	$⊢ Ⅎ y B \subseteq ℝ$
41		nfra2w	$⊢ Ⅎ y \forall x \in A \forall y \in B x \leq y$
42	39 40 41	nf3an	$⊢ Ⅎ y (A \subseteq ℝ \land B \subseteq ℝ \land \forall x \in A \forall y \in B x \leq y)$
43		nfv	$⊢ Ⅎ y (w \in (A \cap B) \land x \in A)$
44	42 43	nfan	$⊢ Ⅎ y ((A \subseteq ℝ \land B \subseteq ℝ \land \forall x \in A \forall y \in B x \leq y) \land (w \in (A \cap B) \land x \in A))$
45		rsp	$⊢ \forall x \in A \forall y \in B x \leq y \to (x \in A \to \forall y \in B x \leq y)$
46		elinel2	$⊢ w \in (A \cap B) \to w \in B$
47		breq2	$⊢ y = w \to (x \leq y \leftrightarrow x \leq w)$
48	47	rspccv	$⊢ \forall y \in B x \leq y \to (w \in B \to x \leq w)$
49	46 48	syl5	$⊢ \forall y \in B x \leq y \to (w \in (A \cap B) \to x \leq w)$
50	45 49	syl6	$⊢ \forall x \in A \forall y \in B x \leq y \to (x \in A \to (w \in (A \cap B) \to x \leq w))$
51	50	com23	$⊢ \forall x \in A \forall y \in B x \leq y \to (w \in (A \cap B) \to (x \in A \to x \leq w))$
52	51	imp32	$⊢ (\forall x \in A \forall y \in B x \leq y \land (w \in (A \cap B) \land x \in A)) \to x \leq w$
53	52	3ad2antl3	$⊢ ((A \subseteq ℝ \land B \subseteq ℝ \land \forall x \in A \forall y \in B x \leq y) \land (w \in (A \cap B) \land x \in A)) \to x \leq w$
54	53	adantr	$⊢ (((A \subseteq ℝ \land B \subseteq ℝ \land \forall x \in A \forall y \in B x \leq y) \land (w \in (A \cap B) \land x \in A)) \land y \in B) \to x \leq w$
55		simp3	$⊢ (A \subseteq ℝ \land B \subseteq ℝ \land \forall x \in A \forall y \in B x \leq y) \to \forall x \in A \forall y \in B x \leq y$
56	30	adantr	$⊢ (w \in (A \cap B) \land x \in A) \to w \in A$
57		breq1	$⊢ x = w \to (x \leq y \leftrightarrow w \leq y)$
58	57	ralbidv	$⊢ x = w \to (\forall y \in B x \leq y \leftrightarrow \forall y \in B w \leq y)$
59	58	rspccva	$⊢ (\forall x \in A \forall y \in B x \leq y \land w \in A) \to \forall y \in B w \leq y$
60	55 56 59	syl2an	$⊢ ((A \subseteq ℝ \land B \subseteq ℝ \land \forall x \in A \forall y \in B x \leq y) \land (w \in (A \cap B) \land x \in A)) \to \forall y \in B w \leq y$
61	60	r19.21bi	$⊢ (((A \subseteq ℝ \land B \subseteq ℝ \land \forall x \in A \forall y \in B x \leq y) \land (w \in (A \cap B) \land x \in A)) \land y \in B) \to w \leq y$
62	54 61	jca	$⊢ (((A \subseteq ℝ \land B \subseteq ℝ \land \forall x \in A \forall y \in B x \leq y) \land (w \in (A \cap B) \land x \in A)) \land y \in B) \to (x \leq w \land w \leq y)$
63	62	ex	$⊢ ((A \subseteq ℝ \land B \subseteq ℝ \land \forall x \in A \forall y \in B x \leq y) \land (w \in (A \cap B) \land x \in A)) \to (y \in B \to (x \leq w \land w \leq y))$
64	44 63	ralrimi	$⊢ ((A \subseteq ℝ \land B \subseteq ℝ \land \forall x \in A \forall y \in B x \leq y) \land (w \in (A \cap B) \land x \in A)) \to \forall y \in B (x \leq w \land w \leq y)$
65	64	expr	$⊢ ((A \subseteq ℝ \land B \subseteq ℝ \land \forall x \in A \forall y \in B x \leq y) \land w \in (A \cap B)) \to (x \in A \to \forall y \in B (x \leq w \land w \leq y))$
66	38 65	ralrimi	$⊢ ((A \subseteq ℝ \land B \subseteq ℝ \land \forall x \in A \forall y \in B x \leq y) \land w \in (A \cap B)) \to \forall x \in A \forall y \in B (x \leq w \land w \leq y)$
67		breq2	$⊢ z = w \to (x \leq z \leftrightarrow x \leq w)$
68		breq1	$⊢ z = w \to (z \leq y \leftrightarrow w \leq y)$
69	67 68	anbi12d	$⊢ z = w \to ((x \leq z \land z \leq y) \leftrightarrow (x \leq w \land w \leq y))$
70	69	2ralbidv	$⊢ z = w \to (\forall x \in A \forall y \in B (x \leq z \land z \leq y) \leftrightarrow \forall x \in A \forall y \in B (x \leq w \land w \leq y))$
71	70	rspcev	$⊢ (w \in ℝ \land \forall x \in A \forall y \in B (x \leq w \land w \leq y)) \to \exists z \in ℝ \forall x \in A \forall y \in B (x \leq z \land z \leq y)$
72	32 66 71	syl2anc	$⊢ ((A \subseteq ℝ \land B \subseteq ℝ \land \forall x \in A \forall y \in B x \leq y) \land w \in (A \cap B)) \to \exists z \in ℝ \forall x \in A \forall y \in B (x \leq z \land z \leq y)$
73	72	expcom	$⊢ w \in (A \cap B) \to ((A \subseteq ℝ \land B \subseteq ℝ \land \forall x \in A \forall y \in B x \leq y) \to \exists z \in ℝ \forall x \in A \forall y \in B (x \leq z \land z \leq y))$
74	73	exlimiv	$⊢ \exists w w \in (A \cap B) \to ((A \subseteq ℝ \land B \subseteq ℝ \land \forall x \in A \forall y \in B x \leq y) \to \exists z \in ℝ \forall x \in A \forall y \in B (x \leq z \land z \leq y))$
75	28 74	sylbi	$⊢ A \cap B \neq \emptyset \to ((A \subseteq ℝ \land B \subseteq ℝ \land \forall x \in A \forall y \in B x \leq y) \to \exists z \in ℝ \forall x \in A \forall y \in B (x \leq z \land z \leq y))$
76	27 75	pm2.61ine	$⊢ (A \subseteq ℝ \land B \subseteq ℝ \land \forall x \in A \forall y \in B x \leq y) \to \exists z \in ℝ \forall x \in A \forall y \in B (x \leq z \land z \leq y)$

Metamath Proof Explorer

Theorem dedekindle

Proof