Metamath Proof Explorer

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

Proof

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