Step | Hyp | Ref
| Expression |
1 | | simpr1 1067 |
. . . 4
⊢ (((𝐴 ∩ 𝐵) = ∅ ∧ (𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 ≤ 𝑦)) → 𝐴 ⊆ ℝ) |
2 | | simpr2 1068 |
. . . 4
⊢ (((𝐴 ∩ 𝐵) = ∅ ∧ (𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 ≤ 𝑦)) → 𝐵 ⊆ ℝ) |
3 | | simp1 1061 |
. . . . . . . . . 10
⊢ (((𝐴 ∩ 𝐵) = ∅ ∧ 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ) → (𝐴 ∩ 𝐵) = ∅) |
4 | | simpl 473 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝑥 ∈ 𝐴) |
5 | | disjel 4023 |
. . . . . . . . . 10
⊢ (((𝐴 ∩ 𝐵) = ∅ ∧ 𝑥 ∈ 𝐴) → ¬ 𝑥 ∈ 𝐵) |
6 | 3, 4, 5 | syl2an 494 |
. . . . . . . . 9
⊢ ((((𝐴 ∩ 𝐵) = ∅ ∧ 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → ¬ 𝑥 ∈ 𝐵) |
7 | | eleq1 2689 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑥 → (𝑦 ∈ 𝐵 ↔ 𝑥 ∈ 𝐵)) |
8 | 7 | biimpcd 239 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ 𝐵 → (𝑦 = 𝑥 → 𝑥 ∈ 𝐵)) |
9 | 8 | necon3bd 2808 |
. . . . . . . . . 10
⊢ (𝑦 ∈ 𝐵 → (¬ 𝑥 ∈ 𝐵 → 𝑦 ≠ 𝑥)) |
10 | 9 | ad2antll 765 |
. . . . . . . . 9
⊢ ((((𝐴 ∩ 𝐵) = ∅ ∧ 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (¬ 𝑥 ∈ 𝐵 → 𝑦 ≠ 𝑥)) |
11 | 6, 10 | mpd 15 |
. . . . . . . 8
⊢ ((((𝐴 ∩ 𝐵) = ∅ ∧ 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝑦 ≠ 𝑥) |
12 | | simp2 1062 |
. . . . . . . . . . 11
⊢ (((𝐴 ∩ 𝐵) = ∅ ∧ 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ) → 𝐴 ⊆ ℝ) |
13 | | ssel2 3598 |
. . . . . . . . . . 11
⊢ ((𝐴 ⊆ ℝ ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ℝ) |
14 | 12, 4, 13 | syl2an 494 |
. . . . . . . . . 10
⊢ ((((𝐴 ∩ 𝐵) = ∅ ∧ 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝑥 ∈ ℝ) |
15 | | simp3 1063 |
. . . . . . . . . . 11
⊢ (((𝐴 ∩ 𝐵) = ∅ ∧ 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ) → 𝐵 ⊆ ℝ) |
16 | | simpr 477 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ 𝐵) |
17 | | ssel2 3598 |
. . . . . . . . . . 11
⊢ ((𝐵 ⊆ ℝ ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ ℝ) |
18 | 15, 16, 17 | syl2an 494 |
. . . . . . . . . 10
⊢ ((((𝐴 ∩ 𝐵) = ∅ ∧ 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝑦 ∈ ℝ) |
19 | 14, 18 | ltlend 10182 |
. . . . . . . . 9
⊢ ((((𝐴 ∩ 𝐵) = ∅ ∧ 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝑥 < 𝑦 ↔ (𝑥 ≤ 𝑦 ∧ 𝑦 ≠ 𝑥))) |
20 | 19 | biimprd 238 |
. . . . . . . 8
⊢ ((((𝐴 ∩ 𝐵) = ∅ ∧ 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≠ 𝑥) → 𝑥 < 𝑦)) |
21 | 11, 20 | mpan2d 710 |
. . . . . . 7
⊢ ((((𝐴 ∩ 𝐵) = ∅ ∧ 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝑥 ≤ 𝑦 → 𝑥 < 𝑦)) |
22 | 21 | ralimdvva 2964 |
. . . . . 6
⊢ (((𝐴 ∩ 𝐵) = ∅ ∧ 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 ≤ 𝑦 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 < 𝑦)) |
23 | 22 | 3exp 1264 |
. . . . 5
⊢ ((𝐴 ∩ 𝐵) = ∅ → (𝐴 ⊆ ℝ → (𝐵 ⊆ ℝ → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 ≤ 𝑦 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 < 𝑦)))) |
24 | 23 | 3imp2 1282 |
. . . 4
⊢ (((𝐴 ∩ 𝐵) = ∅ ∧ (𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 ≤ 𝑦)) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 < 𝑦) |
25 | | dedekind 10200 |
. . . 4
⊢ ((𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧
∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 < 𝑦) → ∃𝑧 ∈ ℝ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)) |
26 | 1, 2, 24, 25 | syl3anc 1326 |
. . 3
⊢ (((𝐴 ∩ 𝐵) = ∅ ∧ (𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 ≤ 𝑦)) → ∃𝑧 ∈ ℝ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)) |
27 | 26 | ex 450 |
. 2
⊢ ((𝐴 ∩ 𝐵) = ∅ → ((𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 ≤ 𝑦) → ∃𝑧 ∈ ℝ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦))) |
28 | | n0 3931 |
. . 3
⊢ ((𝐴 ∩ 𝐵) ≠ ∅ ↔ ∃𝑤 𝑤 ∈ (𝐴 ∩ 𝐵)) |
29 | | simp1 1061 |
. . . . . . 7
⊢ ((𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧
∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 ≤ 𝑦) → 𝐴 ⊆ ℝ) |
30 | | inss1 3833 |
. . . . . . . 8
⊢ (𝐴 ∩ 𝐵) ⊆ 𝐴 |
31 | 30 | sseli 3599 |
. . . . . . 7
⊢ (𝑤 ∈ (𝐴 ∩ 𝐵) → 𝑤 ∈ 𝐴) |
32 | | ssel2 3598 |
. . . . . . 7
⊢ ((𝐴 ⊆ ℝ ∧ 𝑤 ∈ 𝐴) → 𝑤 ∈ ℝ) |
33 | 29, 31, 32 | syl2an 494 |
. . . . . 6
⊢ (((𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧
∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 ≤ 𝑦) ∧ 𝑤 ∈ (𝐴 ∩ 𝐵)) → 𝑤 ∈ ℝ) |
34 | | nfv 1843 |
. . . . . . . . 9
⊢
Ⅎ𝑥 𝐴 ⊆
ℝ |
35 | | nfv 1843 |
. . . . . . . . 9
⊢
Ⅎ𝑥 𝐵 ⊆
ℝ |
36 | | nfra1 2941 |
. . . . . . . . 9
⊢
Ⅎ𝑥∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 ≤ 𝑦 |
37 | 34, 35, 36 | nf3an 1831 |
. . . . . . . 8
⊢
Ⅎ𝑥(𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧
∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 ≤ 𝑦) |
38 | | nfv 1843 |
. . . . . . . 8
⊢
Ⅎ𝑥 𝑤 ∈ (𝐴 ∩ 𝐵) |
39 | 37, 38 | nfan 1828 |
. . . . . . 7
⊢
Ⅎ𝑥((𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧
∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 ≤ 𝑦) ∧ 𝑤 ∈ (𝐴 ∩ 𝐵)) |
40 | | nfv 1843 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦 𝐴 ⊆
ℝ |
41 | | nfv 1843 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦 𝐵 ⊆
ℝ |
42 | | nfra2 2946 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 ≤ 𝑦 |
43 | 40, 41, 42 | nf3an 1831 |
. . . . . . . . . 10
⊢
Ⅎ𝑦(𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧
∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 ≤ 𝑦) |
44 | | nfv 1843 |
. . . . . . . . . 10
⊢
Ⅎ𝑦(𝑤 ∈ (𝐴 ∩ 𝐵) ∧ 𝑥 ∈ 𝐴) |
45 | 43, 44 | nfan 1828 |
. . . . . . . . 9
⊢
Ⅎ𝑦((𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧
∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 ≤ 𝑦) ∧ (𝑤 ∈ (𝐴 ∩ 𝐵) ∧ 𝑥 ∈ 𝐴)) |
46 | | rsp 2929 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐵 𝑥 ≤ 𝑦 → (𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐵 𝑥 ≤ 𝑦)) |
47 | | inss2 3834 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∩ 𝐵) ⊆ 𝐵 |
48 | 47 | sseli 3599 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 ∈ (𝐴 ∩ 𝐵) → 𝑤 ∈ 𝐵) |
49 | | breq2 4657 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 𝑤 → (𝑥 ≤ 𝑦 ↔ 𝑥 ≤ 𝑤)) |
50 | 49 | rspccv 3306 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑦 ∈
𝐵 𝑥 ≤ 𝑦 → (𝑤 ∈ 𝐵 → 𝑥 ≤ 𝑤)) |
51 | 48, 50 | syl5 34 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑦 ∈
𝐵 𝑥 ≤ 𝑦 → (𝑤 ∈ (𝐴 ∩ 𝐵) → 𝑥 ≤ 𝑤)) |
52 | 46, 51 | syl6 35 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐵 𝑥 ≤ 𝑦 → (𝑥 ∈ 𝐴 → (𝑤 ∈ (𝐴 ∩ 𝐵) → 𝑥 ≤ 𝑤))) |
53 | 52 | com23 86 |
. . . . . . . . . . . . . 14
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐵 𝑥 ≤ 𝑦 → (𝑤 ∈ (𝐴 ∩ 𝐵) → (𝑥 ∈ 𝐴 → 𝑥 ≤ 𝑤))) |
54 | 53 | imp32 449 |
. . . . . . . . . . . . 13
⊢
((∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐵 𝑥 ≤ 𝑦 ∧ (𝑤 ∈ (𝐴 ∩ 𝐵) ∧ 𝑥 ∈ 𝐴)) → 𝑥 ≤ 𝑤) |
55 | 54 | 3ad2antl3 1225 |
. . . . . . . . . . . 12
⊢ (((𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧
∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 ≤ 𝑦) ∧ (𝑤 ∈ (𝐴 ∩ 𝐵) ∧ 𝑥 ∈ 𝐴)) → 𝑥 ≤ 𝑤) |
56 | 55 | adantr 481 |
. . . . . . . . . . 11
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧
∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 ≤ 𝑦) ∧ (𝑤 ∈ (𝐴 ∩ 𝐵) ∧ 𝑥 ∈ 𝐴)) ∧ 𝑦 ∈ 𝐵) → 𝑥 ≤ 𝑤) |
57 | | simp3 1063 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧
∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 ≤ 𝑦) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 ≤ 𝑦) |
58 | 31 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝑤 ∈ (𝐴 ∩ 𝐵) ∧ 𝑥 ∈ 𝐴) → 𝑤 ∈ 𝐴) |
59 | | breq1 4656 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑤 → (𝑥 ≤ 𝑦 ↔ 𝑤 ≤ 𝑦)) |
60 | 59 | ralbidv 2986 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑤 → (∀𝑦 ∈ 𝐵 𝑥 ≤ 𝑦 ↔ ∀𝑦 ∈ 𝐵 𝑤 ≤ 𝑦)) |
61 | 60 | rspccva 3308 |
. . . . . . . . . . . . 13
⊢
((∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐵 𝑥 ≤ 𝑦 ∧ 𝑤 ∈ 𝐴) → ∀𝑦 ∈ 𝐵 𝑤 ≤ 𝑦) |
62 | 57, 58, 61 | syl2an 494 |
. . . . . . . . . . . 12
⊢ (((𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧
∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 ≤ 𝑦) ∧ (𝑤 ∈ (𝐴 ∩ 𝐵) ∧ 𝑥 ∈ 𝐴)) → ∀𝑦 ∈ 𝐵 𝑤 ≤ 𝑦) |
63 | 62 | r19.21bi 2932 |
. . . . . . . . . . 11
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧
∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 ≤ 𝑦) ∧ (𝑤 ∈ (𝐴 ∩ 𝐵) ∧ 𝑥 ∈ 𝐴)) ∧ 𝑦 ∈ 𝐵) → 𝑤 ≤ 𝑦) |
64 | 56, 63 | jca 554 |
. . . . . . . . . 10
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧
∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 ≤ 𝑦) ∧ (𝑤 ∈ (𝐴 ∩ 𝐵) ∧ 𝑥 ∈ 𝐴)) ∧ 𝑦 ∈ 𝐵) → (𝑥 ≤ 𝑤 ∧ 𝑤 ≤ 𝑦)) |
65 | 64 | ex 450 |
. . . . . . . . 9
⊢ (((𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧
∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 ≤ 𝑦) ∧ (𝑤 ∈ (𝐴 ∩ 𝐵) ∧ 𝑥 ∈ 𝐴)) → (𝑦 ∈ 𝐵 → (𝑥 ≤ 𝑤 ∧ 𝑤 ≤ 𝑦))) |
66 | 45, 65 | ralrimi 2957 |
. . . . . . . 8
⊢ (((𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧
∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 ≤ 𝑦) ∧ (𝑤 ∈ (𝐴 ∩ 𝐵) ∧ 𝑥 ∈ 𝐴)) → ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑤 ∧ 𝑤 ≤ 𝑦)) |
67 | 66 | expr 643 |
. . . . . . 7
⊢ (((𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧
∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 ≤ 𝑦) ∧ 𝑤 ∈ (𝐴 ∩ 𝐵)) → (𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑤 ∧ 𝑤 ≤ 𝑦))) |
68 | 39, 67 | ralrimi 2957 |
. . . . . 6
⊢ (((𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧
∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 ≤ 𝑦) ∧ 𝑤 ∈ (𝐴 ∩ 𝐵)) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑤 ∧ 𝑤 ≤ 𝑦)) |
69 | | breq2 4657 |
. . . . . . . . 9
⊢ (𝑧 = 𝑤 → (𝑥 ≤ 𝑧 ↔ 𝑥 ≤ 𝑤)) |
70 | | breq1 4656 |
. . . . . . . . 9
⊢ (𝑧 = 𝑤 → (𝑧 ≤ 𝑦 ↔ 𝑤 ≤ 𝑦)) |
71 | 69, 70 | anbi12d 747 |
. . . . . . . 8
⊢ (𝑧 = 𝑤 → ((𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦) ↔ (𝑥 ≤ 𝑤 ∧ 𝑤 ≤ 𝑦))) |
72 | 71 | 2ralbidv 2989 |
. . . . . . 7
⊢ (𝑧 = 𝑤 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑤 ∧ 𝑤 ≤ 𝑦))) |
73 | 72 | rspcev 3309 |
. . . . . 6
⊢ ((𝑤 ∈ ℝ ∧
∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑤 ∧ 𝑤 ≤ 𝑦)) → ∃𝑧 ∈ ℝ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)) |
74 | 33, 68, 73 | syl2anc 693 |
. . . . 5
⊢ (((𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧
∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 ≤ 𝑦) ∧ 𝑤 ∈ (𝐴 ∩ 𝐵)) → ∃𝑧 ∈ ℝ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)) |
75 | 74 | expcom 451 |
. . . 4
⊢ (𝑤 ∈ (𝐴 ∩ 𝐵) → ((𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 ≤ 𝑦) → ∃𝑧 ∈ ℝ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦))) |
76 | 75 | exlimiv 1858 |
. . 3
⊢
(∃𝑤 𝑤 ∈ (𝐴 ∩ 𝐵) → ((𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 ≤ 𝑦) → ∃𝑧 ∈ ℝ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦))) |
77 | 28, 76 | sylbi 207 |
. 2
⊢ ((𝐴 ∩ 𝐵) ≠ ∅ → ((𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 ≤ 𝑦) → ∃𝑧 ∈ ℝ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦))) |
78 | 27, 77 | pm2.61ine 2877 |
1
⊢ ((𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧
∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 ≤ 𝑦) → ∃𝑧 ∈ ℝ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)) |