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 ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 ≤ 𝑦 ) → ∃ 𝑧 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦 ) )

Proof

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