Metamath Proof Explorer

Theorem dedekind

Description: The Dedekind cut theorem. This theorem, which may be used to replace ax-pre-sup with appropriate adjustments, states that, if A completely preceeds B , then there is some number separating the two of them. (Contributed by Scott Fenton, 13-Jun-2013)

Ref Expression
Assertion dedekind ⊢A⊆ℝ∧B⊆ℝ∧∀x∈A∀y∈Bx<y→∃z∈ℝ∀x∈A∀y∈Bx≤z∧z≤y

Proof

Step Hyp Ref Expression
1 nfv ⊢ℲxA≠∅∧B≠∅
2 nfv ⊢ℲxA⊆ℝ∧B⊆ℝ
3 nfra1 ⊢Ⅎx∀x∈A∀y∈Bx<y
4 1 2 3 nf3an ⊢ℲxA≠∅∧B≠∅∧A⊆ℝ∧B⊆ℝ∧∀x∈A∀y∈Bx<y
5 nfv ⊢Ⅎxz∈ℝ
6 nfra1 ⊢Ⅎx∀x∈A¬z<x
7 nfra1 ⊢Ⅎx∀x∈ℝx<z→∃w∈Ax<w
8 6 7 nfan ⊢Ⅎx∀x∈A¬z<x∧∀x∈ℝx<z→∃w∈Ax<w
9 5 8 nfan ⊢Ⅎxz∈ℝ∧∀x∈A¬z<x∧∀x∈ℝx<z→∃w∈Ax<w
10 4 9 nfan ⊢ℲxA≠∅∧B≠∅∧A⊆ℝ∧B⊆ℝ∧∀x∈A∀y∈Bx<y∧z∈ℝ∧∀x∈A¬z<x∧∀x∈ℝx<z→∃w∈Ax<w
11 nfv ⊢ℲyA≠∅∧B≠∅
12 nfv ⊢ℲyA⊆ℝ∧B⊆ℝ
13 nfra2w ⊢Ⅎy∀x∈A∀y∈Bx<y
14 11 12 13 nf3an ⊢ℲyA≠∅∧B≠∅∧A⊆ℝ∧B⊆ℝ∧∀x∈A∀y∈Bx<y
15 nfv ⊢Ⅎyz∈ℝ∧∀x∈A¬z<x∧∀x∈ℝx<z→∃w∈Ax<w
16 14 15 nfan ⊢ℲyA≠∅∧B≠∅∧A⊆ℝ∧B⊆ℝ∧∀x∈A∀y∈Bx<y∧z∈ℝ∧∀x∈A¬z<x∧∀x∈ℝx<z→∃w∈Ax<w
17 nfv ⊢Ⅎyx∈A
18 simpl2l ⊢A≠∅∧B≠∅∧A⊆ℝ∧B⊆ℝ∧∀x∈A∀y∈Bx<y∧z∈ℝ∧∀x∈A¬z<x∧∀x∈ℝx<z→∃w∈Ax<w→A⊆ℝ
19 18 sselda ⊢A≠∅∧B≠∅∧A⊆ℝ∧B⊆ℝ∧∀x∈A∀y∈Bx<y∧z∈ℝ∧∀x∈A¬z<x∧∀x∈ℝx<z→∃w∈Ax<w∧x∈A→x∈ℝ
20 simplrl ⊢A≠∅∧B≠∅∧A⊆ℝ∧B⊆ℝ∧∀x∈A∀y∈Bx<y∧z∈ℝ∧∀x∈A¬z<x∧∀x∈ℝx<z→∃w∈Ax<w∧x∈A→z∈ℝ
21 simprrl ⊢A≠∅∧B≠∅∧A⊆ℝ∧B⊆ℝ∧∀x∈A∀y∈Bx<y∧z∈ℝ∧∀x∈A¬z<x∧∀x∈ℝx<z→∃w∈Ax<w→∀x∈A¬z<x
22 21 r19.21bi ⊢A≠∅∧B≠∅∧A⊆ℝ∧B⊆ℝ∧∀x∈A∀y∈Bx<y∧z∈ℝ∧∀x∈A¬z<x∧∀x∈ℝx<z→∃w∈Ax<w∧x∈A→¬z<x
23 19 20 22 nltled ⊢A≠∅∧B≠∅∧A⊆ℝ∧B⊆ℝ∧∀x∈A∀y∈Bx<y∧z∈ℝ∧∀x∈A¬z<x∧∀x∈ℝx<z→∃w∈Ax<w∧x∈A→x≤z
24 23 ex ⊢A≠∅∧B≠∅∧A⊆ℝ∧B⊆ℝ∧∀x∈A∀y∈Bx<y∧z∈ℝ∧∀x∈A¬z<x∧∀x∈ℝx<z→∃w∈Ax<w→x∈A→x≤z
25 simprll ⊢A≠∅∧B≠∅∧A⊆ℝ∧B⊆ℝ∧∀x∈A∀y∈Bx<y∧z∈ℝ∧∀x∈A¬z<x∧∀x∈ℝx<z→∃w∈Ax<w∧y∈B→z∈ℝ
26 simp2r ⊢A≠∅∧B≠∅∧A⊆ℝ∧B⊆ℝ∧∀x∈A∀y∈Bx<y→B⊆ℝ
27 simpr ⊢z∈ℝ∧∀x∈A¬z<x∧∀x∈ℝx<z→∃w∈Ax<w∧y∈B→y∈B
28 ssel2 ⊢B⊆ℝ∧y∈B→y∈ℝ
29 26 27 28 syl2an ⊢A≠∅∧B≠∅∧A⊆ℝ∧B⊆ℝ∧∀x∈A∀y∈Bx<y∧z∈ℝ∧∀x∈A¬z<x∧∀x∈ℝx<z→∃w∈Ax<w∧y∈B→y∈ℝ
30 simpl3 ⊢A≠∅∧B≠∅∧A⊆ℝ∧B⊆ℝ∧∀x∈A∀y∈Bx<y∧z∈ℝ∧∀x∈A¬z<x∧∀x∈ℝx<z→∃w∈Ax<w∧y∈B→∀x∈A∀y∈Bx<y
31 simp2 ⊢A≠∅∧B≠∅∧A⊆ℝ∧B⊆ℝ∧∀x∈A∀y∈Bx<y→A⊆ℝ∧B⊆ℝ
32 rsp ⊢∀y∈Bx<y→y∈B→x<y
33 32 com12 ⊢y∈B→∀y∈Bx<y→x<y
34 33 adantl ⊢A⊆ℝ∧B⊆ℝ∧x∈A∧y∈B→∀y∈Bx<y→x<y
35 ssel2 ⊢A⊆ℝ∧x∈A→x∈ℝ
36 35 adantlr ⊢A⊆ℝ∧B⊆ℝ∧x∈A→x∈ℝ
37 simplr ⊢A⊆ℝ∧B⊆ℝ∧x∈A→B⊆ℝ
38 37 sselda ⊢A⊆ℝ∧B⊆ℝ∧x∈A∧y∈B→y∈ℝ
39 ltnsym ⊢x∈ℝ∧y∈ℝ→x<y→¬y<x
40 36 38 39 syl2an2r ⊢A⊆ℝ∧B⊆ℝ∧x∈A∧y∈B→x<y→¬y<x
41 34 40 syld ⊢A⊆ℝ∧B⊆ℝ∧x∈A∧y∈B→∀y∈Bx<y→¬y<x
42 41 an32s ⊢A⊆ℝ∧B⊆ℝ∧y∈B∧x∈A→∀y∈Bx<y→¬y<x
43 42 ralimdva ⊢A⊆ℝ∧B⊆ℝ∧y∈B→∀x∈A∀y∈Bx<y→∀x∈A¬y<x
44 31 27 43 syl2an ⊢A≠∅∧B≠∅∧A⊆ℝ∧B⊆ℝ∧∀x∈A∀y∈Bx<y∧z∈ℝ∧∀x∈A¬z<x∧∀x∈ℝx<z→∃w∈Ax<w∧y∈B→∀x∈A∀y∈Bx<y→∀x∈A¬y<x
45 30 44 mpd ⊢A≠∅∧B≠∅∧A⊆ℝ∧B⊆ℝ∧∀x∈A∀y∈Bx<y∧z∈ℝ∧∀x∈A¬z<x∧∀x∈ℝx<z→∃w∈Ax<w∧y∈B→∀x∈A¬y<x
46 breq2 ⊢x=w→y<x↔y<w
47 46 notbid ⊢x=w→¬y<x↔¬y<w
48 47 cbvralvw ⊢∀x∈A¬y<x↔∀w∈A¬y<w
49 45 48 sylib ⊢A≠∅∧B≠∅∧A⊆ℝ∧B⊆ℝ∧∀x∈A∀y∈Bx<y∧z∈ℝ∧∀x∈A¬z<x∧∀x∈ℝx<z→∃w∈Ax<w∧y∈B→∀w∈A¬y<w
50 ralnex ⊢∀w∈A¬y<w↔¬∃w∈Ay<w
51 49 50 sylib ⊢A≠∅∧B≠∅∧A⊆ℝ∧B⊆ℝ∧∀x∈A∀y∈Bx<y∧z∈ℝ∧∀x∈A¬z<x∧∀x∈ℝx<z→∃w∈Ax<w∧y∈B→¬∃w∈Ay<w
52 breq1 ⊢x=y→x<z↔y<z
53 breq1 ⊢x=y→x<w↔y<w
54 53 rexbidv ⊢x=y→∃w∈Ax<w↔∃w∈Ay<w
55 52 54 imbi12d ⊢x=y→x<z→∃w∈Ax<w↔y<z→∃w∈Ay<w
56 simplrr ⊢z∈ℝ∧∀x∈A¬z<x∧∀x∈ℝx<z→∃w∈Ax<w∧y∈B→∀x∈ℝx<z→∃w∈Ax<w
57 56 adantl ⊢A≠∅∧B≠∅∧A⊆ℝ∧B⊆ℝ∧∀x∈A∀y∈Bx<y∧z∈ℝ∧∀x∈A¬z<x∧∀x∈ℝx<z→∃w∈Ax<w∧y∈B→∀x∈ℝx<z→∃w∈Ax<w
58 55 57 29 rspcdva ⊢A≠∅∧B≠∅∧A⊆ℝ∧B⊆ℝ∧∀x∈A∀y∈Bx<y∧z∈ℝ∧∀x∈A¬z<x∧∀x∈ℝx<z→∃w∈Ax<w∧y∈B→y<z→∃w∈Ay<w
59 51 58 mtod ⊢A≠∅∧B≠∅∧A⊆ℝ∧B⊆ℝ∧∀x∈A∀y∈Bx<y∧z∈ℝ∧∀x∈A¬z<x∧∀x∈ℝx<z→∃w∈Ax<w∧y∈B→¬y<z
60 25 29 59 nltled ⊢A≠∅∧B≠∅∧A⊆ℝ∧B⊆ℝ∧∀x∈A∀y∈Bx<y∧z∈ℝ∧∀x∈A¬z<x∧∀x∈ℝx<z→∃w∈Ax<w∧y∈B→z≤y
61 60 expr ⊢A≠∅∧B≠∅∧A⊆ℝ∧B⊆ℝ∧∀x∈A∀y∈Bx<y∧z∈ℝ∧∀x∈A¬z<x∧∀x∈ℝx<z→∃w∈Ax<w→y∈B→z≤y
62 24 61 anim12d ⊢A≠∅∧B≠∅∧A⊆ℝ∧B⊆ℝ∧∀x∈A∀y∈Bx<y∧z∈ℝ∧∀x∈A¬z<x∧∀x∈ℝx<z→∃w∈Ax<w→x∈A∧y∈B→x≤z∧z≤y
63 62 expd ⊢A≠∅∧B≠∅∧A⊆ℝ∧B⊆ℝ∧∀x∈A∀y∈Bx<y∧z∈ℝ∧∀x∈A¬z<x∧∀x∈ℝx<z→∃w∈Ax<w→x∈A→y∈B→x≤z∧z≤y
64 16 17 63 ralrimd ⊢A≠∅∧B≠∅∧A⊆ℝ∧B⊆ℝ∧∀x∈A∀y∈Bx<y∧z∈ℝ∧∀x∈A¬z<x∧∀x∈ℝx<z→∃w∈Ax<w→x∈A→∀y∈Bx≤z∧z≤y
65 10 64 ralrimi ⊢A≠∅∧B≠∅∧A⊆ℝ∧B⊆ℝ∧∀x∈A∀y∈Bx<y∧z∈ℝ∧∀x∈A¬z<x∧∀x∈ℝx<z→∃w∈Ax<w→∀x∈A∀y∈Bx≤z∧z≤y
66 simp2l ⊢A≠∅∧B≠∅∧A⊆ℝ∧B⊆ℝ∧∀x∈A∀y∈Bx<y→A⊆ℝ
67 simp1l ⊢A≠∅∧B≠∅∧A⊆ℝ∧B⊆ℝ∧∀x∈A∀y∈Bx<y→A≠∅
68 simp1r ⊢A≠∅∧B≠∅∧A⊆ℝ∧B⊆ℝ∧∀x∈A∀y∈Bx<y→B≠∅
69 n0 ⊢B≠∅↔∃zz∈B
70 68 69 sylib ⊢A≠∅∧B≠∅∧A⊆ℝ∧B⊆ℝ∧∀x∈A∀y∈Bx<y→∃zz∈B
71 26 sseld ⊢A≠∅∧B≠∅∧A⊆ℝ∧B⊆ℝ∧∀x∈A∀y∈Bx<y→z∈B→z∈ℝ
72 ralcom ⊢∀x∈A∀y∈Bx<y↔∀y∈B∀x∈Ax<y
73 breq2 ⊢y=z→x<y↔x<z
74 73 ralbidv ⊢y=z→∀x∈Ax<y↔∀x∈Ax<z
75 74 rspccv ⊢∀y∈B∀x∈Ax<y→z∈B→∀x∈Ax<z
76 72 75 sylbi ⊢∀x∈A∀y∈Bx<y→z∈B→∀x∈Ax<z
77 76 3ad2ant3 ⊢A≠∅∧B≠∅∧A⊆ℝ∧B⊆ℝ∧∀x∈A∀y∈Bx<y→z∈B→∀x∈Ax<z
78 71 77 jcad ⊢A≠∅∧B≠∅∧A⊆ℝ∧B⊆ℝ∧∀x∈A∀y∈Bx<y→z∈B→z∈ℝ∧∀x∈Ax<z
79 78 eximdv ⊢A≠∅∧B≠∅∧A⊆ℝ∧B⊆ℝ∧∀x∈A∀y∈Bx<y→∃zz∈B→∃zz∈ℝ∧∀x∈Ax<z
80 70 79 mpd ⊢A≠∅∧B≠∅∧A⊆ℝ∧B⊆ℝ∧∀x∈A∀y∈Bx<y→∃zz∈ℝ∧∀x∈Ax<z
81 df-rex ⊢∃z∈ℝ∀x∈Ax<z↔∃zz∈ℝ∧∀x∈Ax<z
82 80 81 sylibr ⊢A≠∅∧B≠∅∧A⊆ℝ∧B⊆ℝ∧∀x∈A∀y∈Bx<y→∃z∈ℝ∀x∈Ax<z
83 axsup ⊢A⊆ℝ∧A≠∅∧∃z∈ℝ∀x∈Ax<z→∃z∈ℝ∀x∈A¬z<x∧∀x∈ℝx<z→∃w∈Ax<w
84 66 67 82 83 syl3anc ⊢A≠∅∧B≠∅∧A⊆ℝ∧B⊆ℝ∧∀x∈A∀y∈Bx<y→∃z∈ℝ∀x∈A¬z<x∧∀x∈ℝx<z→∃w∈Ax<w
85 65 84 reximddv ⊢A≠∅∧B≠∅∧A⊆ℝ∧B⊆ℝ∧∀x∈A∀y∈Bx<y→∃z∈ℝ∀x∈A∀y∈Bx≤z∧z≤y
86 85 3expib ⊢A≠∅∧B≠∅→A⊆ℝ∧B⊆ℝ∧∀x∈A∀y∈Bx<y→∃z∈ℝ∀x∈A∀y∈Bx≤z∧z≤y
87 1re ⊢1∈ℝ
88 rzal ⊢A=∅→∀x∈A∀y∈Bx≤1∧1≤y
89 breq2 ⊢z=1→x≤z↔x≤1
90 breq1 ⊢z=1→z≤y↔1≤y
91 89 90 anbi12d ⊢z=1→x≤z∧z≤y↔x≤1∧1≤y
92 91 2ralbidv ⊢z=1→∀x∈A∀y∈Bx≤z∧z≤y↔∀x∈A∀y∈Bx≤1∧1≤y
93 92 rspcev ⊢1∈ℝ∧∀x∈A∀y∈Bx≤1∧1≤y→∃z∈ℝ∀x∈A∀y∈Bx≤z∧z≤y
94 87 88 93 sylancr ⊢A=∅→∃z∈ℝ∀x∈A∀y∈Bx≤z∧z≤y
95 94 a1d ⊢A=∅→A⊆ℝ∧B⊆ℝ∧∀x∈A∀y∈Bx<y→∃z∈ℝ∀x∈A∀y∈Bx≤z∧z≤y
96 rzal ⊢B=∅→∀y∈Bx≤1∧1≤y
97 96 ralrimivw ⊢B=∅→∀x∈A∀y∈Bx≤1∧1≤y
98 87 97 93 sylancr ⊢B=∅→∃z∈ℝ∀x∈A∀y∈Bx≤z∧z≤y
99 98 a1d ⊢B=∅→A⊆ℝ∧B⊆ℝ∧∀x∈A∀y∈Bx<y→∃z∈ℝ∀x∈A∀y∈Bx≤z∧z≤y
100 86 95 99 pm2.61iine ⊢A⊆ℝ∧B⊆ℝ∧∀x∈A∀y∈Bx<y→∃z∈ℝ∀x∈A∀y∈Bx≤z∧z≤y
101 100 3impa ⊢A⊆ℝ∧B⊆ℝ∧∀x∈A∀y∈Bx<y→∃z∈ℝ∀x∈A∀y∈Bx≤z∧z≤y