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 ∈ B x < y → ∃ z ∈ ℝ ∀ x ∈ A ∀ y ∈ B x ≤ z ∧ z ≤ y

Proof

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