Step | Hyp | Ref
| Expression |
1 | | sseq1 3147 |
. . . 4
⊢ (𝑤 = ∅ → (𝑤 ⊆ ℝ ↔ ∅
⊆ ℝ)) |
2 | | raleq 2649 |
. . . . 5
⊢ (𝑤 = ∅ → (∀𝑦 ∈ 𝑤 𝑦 ≤ 𝑥 ↔ ∀𝑦 ∈ ∅ 𝑦 ≤ 𝑥)) |
3 | 2 | rexbidv 2455 |
. . . 4
⊢ (𝑤 = ∅ → (∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑤 𝑦 ≤ 𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ∅ 𝑦 ≤ 𝑥)) |
4 | 1, 3 | imbi12d 233 |
. . 3
⊢ (𝑤 = ∅ → ((𝑤 ⊆ ℝ →
∃𝑥 ∈ ℝ
∀𝑦 ∈ 𝑤 𝑦 ≤ 𝑥) ↔ (∅ ⊆ ℝ →
∃𝑥 ∈ ℝ
∀𝑦 ∈ ∅
𝑦 ≤ 𝑥))) |
5 | | sseq1 3147 |
. . . 4
⊢ (𝑤 = 𝑢 → (𝑤 ⊆ ℝ ↔ 𝑢 ⊆ ℝ)) |
6 | | raleq 2649 |
. . . . 5
⊢ (𝑤 = 𝑢 → (∀𝑦 ∈ 𝑤 𝑦 ≤ 𝑥 ↔ ∀𝑦 ∈ 𝑢 𝑦 ≤ 𝑥)) |
7 | 6 | rexbidv 2455 |
. . . 4
⊢ (𝑤 = 𝑢 → (∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑤 𝑦 ≤ 𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑢 𝑦 ≤ 𝑥)) |
8 | 5, 7 | imbi12d 233 |
. . 3
⊢ (𝑤 = 𝑢 → ((𝑤 ⊆ ℝ → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑤 𝑦 ≤ 𝑥) ↔ (𝑢 ⊆ ℝ → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑢 𝑦 ≤ 𝑥))) |
9 | | sseq1 3147 |
. . . 4
⊢ (𝑤 = (𝑢 ∪ {𝑣}) → (𝑤 ⊆ ℝ ↔ (𝑢 ∪ {𝑣}) ⊆ ℝ)) |
10 | | raleq 2649 |
. . . . 5
⊢ (𝑤 = (𝑢 ∪ {𝑣}) → (∀𝑦 ∈ 𝑤 𝑦 ≤ 𝑥 ↔ ∀𝑦 ∈ (𝑢 ∪ {𝑣})𝑦 ≤ 𝑥)) |
11 | 10 | rexbidv 2455 |
. . . 4
⊢ (𝑤 = (𝑢 ∪ {𝑣}) → (∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑤 𝑦 ≤ 𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑦 ∈ (𝑢 ∪ {𝑣})𝑦 ≤ 𝑥)) |
12 | 9, 11 | imbi12d 233 |
. . 3
⊢ (𝑤 = (𝑢 ∪ {𝑣}) → ((𝑤 ⊆ ℝ → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑤 𝑦 ≤ 𝑥) ↔ ((𝑢 ∪ {𝑣}) ⊆ ℝ → ∃𝑥 ∈ ℝ ∀𝑦 ∈ (𝑢 ∪ {𝑣})𝑦 ≤ 𝑥))) |
13 | | sseq1 3147 |
. . . 4
⊢ (𝑤 = 𝐴 → (𝑤 ⊆ ℝ ↔ 𝐴 ⊆ ℝ)) |
14 | | raleq 2649 |
. . . . 5
⊢ (𝑤 = 𝐴 → (∀𝑦 ∈ 𝑤 𝑦 ≤ 𝑥 ↔ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)) |
15 | 14 | rexbidv 2455 |
. . . 4
⊢ (𝑤 = 𝐴 → (∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑤 𝑦 ≤ 𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)) |
16 | 13, 15 | imbi12d 233 |
. . 3
⊢ (𝑤 = 𝐴 → ((𝑤 ⊆ ℝ → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑤 𝑦 ≤ 𝑥) ↔ (𝐴 ⊆ ℝ → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥))) |
17 | | 0re 7857 |
. . . . 5
⊢ 0 ∈
ℝ |
18 | | ral0 3491 |
. . . . 5
⊢
∀𝑦 ∈
∅ 𝑦 ≤
0 |
19 | | breq2 3965 |
. . . . . . 7
⊢ (𝑥 = 0 → (𝑦 ≤ 𝑥 ↔ 𝑦 ≤ 0)) |
20 | 19 | ralbidv 2454 |
. . . . . 6
⊢ (𝑥 = 0 → (∀𝑦 ∈ ∅ 𝑦 ≤ 𝑥 ↔ ∀𝑦 ∈ ∅ 𝑦 ≤ 0)) |
21 | 20 | rspcev 2813 |
. . . . 5
⊢ ((0
∈ ℝ ∧ ∀𝑦 ∈ ∅ 𝑦 ≤ 0) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ∅ 𝑦 ≤ 𝑥) |
22 | 17, 18, 21 | mp2an 423 |
. . . 4
⊢
∃𝑥 ∈
ℝ ∀𝑦 ∈
∅ 𝑦 ≤ 𝑥 |
23 | 22 | a1i 9 |
. . 3
⊢ (∅
⊆ ℝ → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ∅ 𝑦 ≤ 𝑥) |
24 | | unss 3277 |
. . . . . . . . . 10
⊢ ((𝑢 ⊆ ℝ ∧ {𝑣} ⊆ ℝ) ↔ (𝑢 ∪ {𝑣}) ⊆ ℝ) |
25 | 24 | biimpri 132 |
. . . . . . . . 9
⊢ ((𝑢 ∪ {𝑣}) ⊆ ℝ → (𝑢 ⊆ ℝ ∧ {𝑣} ⊆ ℝ)) |
26 | 25 | simpld 111 |
. . . . . . . 8
⊢ ((𝑢 ∪ {𝑣}) ⊆ ℝ → 𝑢 ⊆ ℝ) |
27 | 26 | adantl 275 |
. . . . . . 7
⊢ (((𝑢 ∈ Fin ∧ (𝑢 ⊆ ℝ →
∃𝑥 ∈ ℝ
∀𝑦 ∈ 𝑢 𝑦 ≤ 𝑥)) ∧ (𝑢 ∪ {𝑣}) ⊆ ℝ) → 𝑢 ⊆ ℝ) |
28 | | simplr 520 |
. . . . . . 7
⊢ (((𝑢 ∈ Fin ∧ (𝑢 ⊆ ℝ →
∃𝑥 ∈ ℝ
∀𝑦 ∈ 𝑢 𝑦 ≤ 𝑥)) ∧ (𝑢 ∪ {𝑣}) ⊆ ℝ) → (𝑢 ⊆ ℝ →
∃𝑥 ∈ ℝ
∀𝑦 ∈ 𝑢 𝑦 ≤ 𝑥)) |
29 | 27, 28 | mpd 13 |
. . . . . 6
⊢ (((𝑢 ∈ Fin ∧ (𝑢 ⊆ ℝ →
∃𝑥 ∈ ℝ
∀𝑦 ∈ 𝑢 𝑦 ≤ 𝑥)) ∧ (𝑢 ∪ {𝑣}) ⊆ ℝ) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑢 𝑦 ≤ 𝑥) |
30 | | breq2 3965 |
. . . . . . . 8
⊢ (𝑥 = 𝑠 → (𝑦 ≤ 𝑥 ↔ 𝑦 ≤ 𝑠)) |
31 | 30 | ralbidv 2454 |
. . . . . . 7
⊢ (𝑥 = 𝑠 → (∀𝑦 ∈ 𝑢 𝑦 ≤ 𝑥 ↔ ∀𝑦 ∈ 𝑢 𝑦 ≤ 𝑠)) |
32 | 31 | cbvrexv 2678 |
. . . . . 6
⊢
(∃𝑥 ∈
ℝ ∀𝑦 ∈
𝑢 𝑦 ≤ 𝑥 ↔ ∃𝑠 ∈ ℝ ∀𝑦 ∈ 𝑢 𝑦 ≤ 𝑠) |
33 | 29, 32 | sylib 121 |
. . . . 5
⊢ (((𝑢 ∈ Fin ∧ (𝑢 ⊆ ℝ →
∃𝑥 ∈ ℝ
∀𝑦 ∈ 𝑢 𝑦 ≤ 𝑥)) ∧ (𝑢 ∪ {𝑣}) ⊆ ℝ) → ∃𝑠 ∈ ℝ ∀𝑦 ∈ 𝑢 𝑦 ≤ 𝑠) |
34 | | simprl 521 |
. . . . . . 7
⊢ ((((𝑢 ∈ Fin ∧ (𝑢 ⊆ ℝ →
∃𝑥 ∈ ℝ
∀𝑦 ∈ 𝑢 𝑦 ≤ 𝑥)) ∧ (𝑢 ∪ {𝑣}) ⊆ ℝ) ∧ (𝑠 ∈ ℝ ∧ ∀𝑦 ∈ 𝑢 𝑦 ≤ 𝑠)) → 𝑠 ∈ ℝ) |
35 | 25 | simprd 113 |
. . . . . . . . 9
⊢ ((𝑢 ∪ {𝑣}) ⊆ ℝ → {𝑣} ⊆ ℝ) |
36 | | vex 2712 |
. . . . . . . . . 10
⊢ 𝑣 ∈ V |
37 | 36 | snss 3681 |
. . . . . . . . 9
⊢ (𝑣 ∈ ℝ ↔ {𝑣} ⊆
ℝ) |
38 | 35, 37 | sylibr 133 |
. . . . . . . 8
⊢ ((𝑢 ∪ {𝑣}) ⊆ ℝ → 𝑣 ∈ ℝ) |
39 | 38 | ad2antlr 481 |
. . . . . . 7
⊢ ((((𝑢 ∈ Fin ∧ (𝑢 ⊆ ℝ →
∃𝑥 ∈ ℝ
∀𝑦 ∈ 𝑢 𝑦 ≤ 𝑥)) ∧ (𝑢 ∪ {𝑣}) ⊆ ℝ) ∧ (𝑠 ∈ ℝ ∧ ∀𝑦 ∈ 𝑢 𝑦 ≤ 𝑠)) → 𝑣 ∈ ℝ) |
40 | | maxcl 11087 |
. . . . . . 7
⊢ ((𝑠 ∈ ℝ ∧ 𝑣 ∈ ℝ) →
sup({𝑠, 𝑣}, ℝ, < ) ∈
ℝ) |
41 | 34, 39, 40 | syl2anc 409 |
. . . . . 6
⊢ ((((𝑢 ∈ Fin ∧ (𝑢 ⊆ ℝ →
∃𝑥 ∈ ℝ
∀𝑦 ∈ 𝑢 𝑦 ≤ 𝑥)) ∧ (𝑢 ∪ {𝑣}) ⊆ ℝ) ∧ (𝑠 ∈ ℝ ∧ ∀𝑦 ∈ 𝑢 𝑦 ≤ 𝑠)) → sup({𝑠, 𝑣}, ℝ, < ) ∈
ℝ) |
42 | | nfv 1505 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦 𝑢 ∈ Fin |
43 | | nfv 1505 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦 𝑢 ⊆
ℝ |
44 | | nfcv 2296 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑦ℝ |
45 | | nfra1 2485 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑦∀𝑦 ∈ 𝑢 𝑦 ≤ 𝑥 |
46 | 44, 45 | nfrexxy 2493 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑢 𝑦 ≤ 𝑥 |
47 | 43, 46 | nfim 1549 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦(𝑢 ⊆ ℝ →
∃𝑥 ∈ ℝ
∀𝑦 ∈ 𝑢 𝑦 ≤ 𝑥) |
48 | 42, 47 | nfan 1542 |
. . . . . . . . . 10
⊢
Ⅎ𝑦(𝑢 ∈ Fin ∧ (𝑢 ⊆ ℝ →
∃𝑥 ∈ ℝ
∀𝑦 ∈ 𝑢 𝑦 ≤ 𝑥)) |
49 | | nfv 1505 |
. . . . . . . . . 10
⊢
Ⅎ𝑦(𝑢 ∪ {𝑣}) ⊆ ℝ |
50 | 48, 49 | nfan 1542 |
. . . . . . . . 9
⊢
Ⅎ𝑦((𝑢 ∈ Fin ∧ (𝑢 ⊆ ℝ →
∃𝑥 ∈ ℝ
∀𝑦 ∈ 𝑢 𝑦 ≤ 𝑥)) ∧ (𝑢 ∪ {𝑣}) ⊆ ℝ) |
51 | | nfv 1505 |
. . . . . . . . . 10
⊢
Ⅎ𝑦 𝑠 ∈ ℝ |
52 | | nfra1 2485 |
. . . . . . . . . 10
⊢
Ⅎ𝑦∀𝑦 ∈ 𝑢 𝑦 ≤ 𝑠 |
53 | 51, 52 | nfan 1542 |
. . . . . . . . 9
⊢
Ⅎ𝑦(𝑠 ∈ ℝ ∧
∀𝑦 ∈ 𝑢 𝑦 ≤ 𝑠) |
54 | 50, 53 | nfan 1542 |
. . . . . . . 8
⊢
Ⅎ𝑦(((𝑢 ∈ Fin ∧ (𝑢 ⊆ ℝ →
∃𝑥 ∈ ℝ
∀𝑦 ∈ 𝑢 𝑦 ≤ 𝑥)) ∧ (𝑢 ∪ {𝑣}) ⊆ ℝ) ∧ (𝑠 ∈ ℝ ∧ ∀𝑦 ∈ 𝑢 𝑦 ≤ 𝑠)) |
55 | | simprr 522 |
. . . . . . . . . . . 12
⊢ ((((𝑢 ∈ Fin ∧ (𝑢 ⊆ ℝ →
∃𝑥 ∈ ℝ
∀𝑦 ∈ 𝑢 𝑦 ≤ 𝑥)) ∧ (𝑢 ∪ {𝑣}) ⊆ ℝ) ∧ (𝑠 ∈ ℝ ∧ ∀𝑦 ∈ 𝑢 𝑦 ≤ 𝑠)) → ∀𝑦 ∈ 𝑢 𝑦 ≤ 𝑠) |
56 | | maxle1 11088 |
. . . . . . . . . . . . 13
⊢ ((𝑠 ∈ ℝ ∧ 𝑣 ∈ ℝ) → 𝑠 ≤ sup({𝑠, 𝑣}, ℝ, < )) |
57 | 34, 39, 56 | syl2anc 409 |
. . . . . . . . . . . 12
⊢ ((((𝑢 ∈ Fin ∧ (𝑢 ⊆ ℝ →
∃𝑥 ∈ ℝ
∀𝑦 ∈ 𝑢 𝑦 ≤ 𝑥)) ∧ (𝑢 ∪ {𝑣}) ⊆ ℝ) ∧ (𝑠 ∈ ℝ ∧ ∀𝑦 ∈ 𝑢 𝑦 ≤ 𝑠)) → 𝑠 ≤ sup({𝑠, 𝑣}, ℝ, < )) |
58 | | r19.27av 2589 |
. . . . . . . . . . . 12
⊢
((∀𝑦 ∈
𝑢 𝑦 ≤ 𝑠 ∧ 𝑠 ≤ sup({𝑠, 𝑣}, ℝ, < )) → ∀𝑦 ∈ 𝑢 (𝑦 ≤ 𝑠 ∧ 𝑠 ≤ sup({𝑠, 𝑣}, ℝ, < ))) |
59 | 55, 57, 58 | syl2anc 409 |
. . . . . . . . . . 11
⊢ ((((𝑢 ∈ Fin ∧ (𝑢 ⊆ ℝ →
∃𝑥 ∈ ℝ
∀𝑦 ∈ 𝑢 𝑦 ≤ 𝑥)) ∧ (𝑢 ∪ {𝑣}) ⊆ ℝ) ∧ (𝑠 ∈ ℝ ∧ ∀𝑦 ∈ 𝑢 𝑦 ≤ 𝑠)) → ∀𝑦 ∈ 𝑢 (𝑦 ≤ 𝑠 ∧ 𝑠 ≤ sup({𝑠, 𝑣}, ℝ, < ))) |
60 | 59 | r19.21bi 2542 |
. . . . . . . . . 10
⊢
(((((𝑢 ∈ Fin
∧ (𝑢 ⊆ ℝ
→ ∃𝑥 ∈
ℝ ∀𝑦 ∈
𝑢 𝑦 ≤ 𝑥)) ∧ (𝑢 ∪ {𝑣}) ⊆ ℝ) ∧ (𝑠 ∈ ℝ ∧ ∀𝑦 ∈ 𝑢 𝑦 ≤ 𝑠)) ∧ 𝑦 ∈ 𝑢) → (𝑦 ≤ 𝑠 ∧ 𝑠 ≤ sup({𝑠, 𝑣}, ℝ, < ))) |
61 | 27 | ad2antrr 480 |
. . . . . . . . . . . 12
⊢
(((((𝑢 ∈ Fin
∧ (𝑢 ⊆ ℝ
→ ∃𝑥 ∈
ℝ ∀𝑦 ∈
𝑢 𝑦 ≤ 𝑥)) ∧ (𝑢 ∪ {𝑣}) ⊆ ℝ) ∧ (𝑠 ∈ ℝ ∧ ∀𝑦 ∈ 𝑢 𝑦 ≤ 𝑠)) ∧ 𝑦 ∈ 𝑢) → 𝑢 ⊆ ℝ) |
62 | | simpr 109 |
. . . . . . . . . . . 12
⊢
(((((𝑢 ∈ Fin
∧ (𝑢 ⊆ ℝ
→ ∃𝑥 ∈
ℝ ∀𝑦 ∈
𝑢 𝑦 ≤ 𝑥)) ∧ (𝑢 ∪ {𝑣}) ⊆ ℝ) ∧ (𝑠 ∈ ℝ ∧ ∀𝑦 ∈ 𝑢 𝑦 ≤ 𝑠)) ∧ 𝑦 ∈ 𝑢) → 𝑦 ∈ 𝑢) |
63 | 61, 62 | sseldd 3125 |
. . . . . . . . . . 11
⊢
(((((𝑢 ∈ Fin
∧ (𝑢 ⊆ ℝ
→ ∃𝑥 ∈
ℝ ∀𝑦 ∈
𝑢 𝑦 ≤ 𝑥)) ∧ (𝑢 ∪ {𝑣}) ⊆ ℝ) ∧ (𝑠 ∈ ℝ ∧ ∀𝑦 ∈ 𝑢 𝑦 ≤ 𝑠)) ∧ 𝑦 ∈ 𝑢) → 𝑦 ∈ ℝ) |
64 | 34 | adantr 274 |
. . . . . . . . . . 11
⊢
(((((𝑢 ∈ Fin
∧ (𝑢 ⊆ ℝ
→ ∃𝑥 ∈
ℝ ∀𝑦 ∈
𝑢 𝑦 ≤ 𝑥)) ∧ (𝑢 ∪ {𝑣}) ⊆ ℝ) ∧ (𝑠 ∈ ℝ ∧ ∀𝑦 ∈ 𝑢 𝑦 ≤ 𝑠)) ∧ 𝑦 ∈ 𝑢) → 𝑠 ∈ ℝ) |
65 | 41 | adantr 274 |
. . . . . . . . . . 11
⊢
(((((𝑢 ∈ Fin
∧ (𝑢 ⊆ ℝ
→ ∃𝑥 ∈
ℝ ∀𝑦 ∈
𝑢 𝑦 ≤ 𝑥)) ∧ (𝑢 ∪ {𝑣}) ⊆ ℝ) ∧ (𝑠 ∈ ℝ ∧ ∀𝑦 ∈ 𝑢 𝑦 ≤ 𝑠)) ∧ 𝑦 ∈ 𝑢) → sup({𝑠, 𝑣}, ℝ, < ) ∈
ℝ) |
66 | | letr 7939 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℝ ∧ 𝑠 ∈ ℝ ∧ sup({𝑠, 𝑣}, ℝ, < ) ∈ ℝ) →
((𝑦 ≤ 𝑠 ∧ 𝑠 ≤ sup({𝑠, 𝑣}, ℝ, < )) → 𝑦 ≤ sup({𝑠, 𝑣}, ℝ, < ))) |
67 | 63, 64, 65, 66 | syl3anc 1217 |
. . . . . . . . . 10
⊢
(((((𝑢 ∈ Fin
∧ (𝑢 ⊆ ℝ
→ ∃𝑥 ∈
ℝ ∀𝑦 ∈
𝑢 𝑦 ≤ 𝑥)) ∧ (𝑢 ∪ {𝑣}) ⊆ ℝ) ∧ (𝑠 ∈ ℝ ∧ ∀𝑦 ∈ 𝑢 𝑦 ≤ 𝑠)) ∧ 𝑦 ∈ 𝑢) → ((𝑦 ≤ 𝑠 ∧ 𝑠 ≤ sup({𝑠, 𝑣}, ℝ, < )) → 𝑦 ≤ sup({𝑠, 𝑣}, ℝ, < ))) |
68 | 60, 67 | mpd 13 |
. . . . . . . . 9
⊢
(((((𝑢 ∈ Fin
∧ (𝑢 ⊆ ℝ
→ ∃𝑥 ∈
ℝ ∀𝑦 ∈
𝑢 𝑦 ≤ 𝑥)) ∧ (𝑢 ∪ {𝑣}) ⊆ ℝ) ∧ (𝑠 ∈ ℝ ∧ ∀𝑦 ∈ 𝑢 𝑦 ≤ 𝑠)) ∧ 𝑦 ∈ 𝑢) → 𝑦 ≤ sup({𝑠, 𝑣}, ℝ, < )) |
69 | 68 | ex 114 |
. . . . . . . 8
⊢ ((((𝑢 ∈ Fin ∧ (𝑢 ⊆ ℝ →
∃𝑥 ∈ ℝ
∀𝑦 ∈ 𝑢 𝑦 ≤ 𝑥)) ∧ (𝑢 ∪ {𝑣}) ⊆ ℝ) ∧ (𝑠 ∈ ℝ ∧ ∀𝑦 ∈ 𝑢 𝑦 ≤ 𝑠)) → (𝑦 ∈ 𝑢 → 𝑦 ≤ sup({𝑠, 𝑣}, ℝ, < ))) |
70 | 54, 69 | ralrimi 2525 |
. . . . . . 7
⊢ ((((𝑢 ∈ Fin ∧ (𝑢 ⊆ ℝ →
∃𝑥 ∈ ℝ
∀𝑦 ∈ 𝑢 𝑦 ≤ 𝑥)) ∧ (𝑢 ∪ {𝑣}) ⊆ ℝ) ∧ (𝑠 ∈ ℝ ∧ ∀𝑦 ∈ 𝑢 𝑦 ≤ 𝑠)) → ∀𝑦 ∈ 𝑢 𝑦 ≤ sup({𝑠, 𝑣}, ℝ, < )) |
71 | | maxle2 11089 |
. . . . . . . . 9
⊢ ((𝑠 ∈ ℝ ∧ 𝑣 ∈ ℝ) → 𝑣 ≤ sup({𝑠, 𝑣}, ℝ, < )) |
72 | 34, 39, 71 | syl2anc 409 |
. . . . . . . 8
⊢ ((((𝑢 ∈ Fin ∧ (𝑢 ⊆ ℝ →
∃𝑥 ∈ ℝ
∀𝑦 ∈ 𝑢 𝑦 ≤ 𝑥)) ∧ (𝑢 ∪ {𝑣}) ⊆ ℝ) ∧ (𝑠 ∈ ℝ ∧ ∀𝑦 ∈ 𝑢 𝑦 ≤ 𝑠)) → 𝑣 ≤ sup({𝑠, 𝑣}, ℝ, < )) |
73 | | breq1 3964 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑣 → (𝑦 ≤ sup({𝑠, 𝑣}, ℝ, < ) ↔ 𝑣 ≤ sup({𝑠, 𝑣}, ℝ, < ))) |
74 | 73 | ralsng 3595 |
. . . . . . . . 9
⊢ (𝑣 ∈ ℝ →
(∀𝑦 ∈ {𝑣}𝑦 ≤ sup({𝑠, 𝑣}, ℝ, < ) ↔ 𝑣 ≤ sup({𝑠, 𝑣}, ℝ, < ))) |
75 | 39, 74 | syl 14 |
. . . . . . . 8
⊢ ((((𝑢 ∈ Fin ∧ (𝑢 ⊆ ℝ →
∃𝑥 ∈ ℝ
∀𝑦 ∈ 𝑢 𝑦 ≤ 𝑥)) ∧ (𝑢 ∪ {𝑣}) ⊆ ℝ) ∧ (𝑠 ∈ ℝ ∧ ∀𝑦 ∈ 𝑢 𝑦 ≤ 𝑠)) → (∀𝑦 ∈ {𝑣}𝑦 ≤ sup({𝑠, 𝑣}, ℝ, < ) ↔ 𝑣 ≤ sup({𝑠, 𝑣}, ℝ, < ))) |
76 | 72, 75 | mpbird 166 |
. . . . . . 7
⊢ ((((𝑢 ∈ Fin ∧ (𝑢 ⊆ ℝ →
∃𝑥 ∈ ℝ
∀𝑦 ∈ 𝑢 𝑦 ≤ 𝑥)) ∧ (𝑢 ∪ {𝑣}) ⊆ ℝ) ∧ (𝑠 ∈ ℝ ∧ ∀𝑦 ∈ 𝑢 𝑦 ≤ 𝑠)) → ∀𝑦 ∈ {𝑣}𝑦 ≤ sup({𝑠, 𝑣}, ℝ, < )) |
77 | | ralun 3285 |
. . . . . . 7
⊢
((∀𝑦 ∈
𝑢 𝑦 ≤ sup({𝑠, 𝑣}, ℝ, < ) ∧ ∀𝑦 ∈ {𝑣}𝑦 ≤ sup({𝑠, 𝑣}, ℝ, < )) → ∀𝑦 ∈ (𝑢 ∪ {𝑣})𝑦 ≤ sup({𝑠, 𝑣}, ℝ, < )) |
78 | 70, 76, 77 | syl2anc 409 |
. . . . . 6
⊢ ((((𝑢 ∈ Fin ∧ (𝑢 ⊆ ℝ →
∃𝑥 ∈ ℝ
∀𝑦 ∈ 𝑢 𝑦 ≤ 𝑥)) ∧ (𝑢 ∪ {𝑣}) ⊆ ℝ) ∧ (𝑠 ∈ ℝ ∧ ∀𝑦 ∈ 𝑢 𝑦 ≤ 𝑠)) → ∀𝑦 ∈ (𝑢 ∪ {𝑣})𝑦 ≤ sup({𝑠, 𝑣}, ℝ, < )) |
79 | | breq2 3965 |
. . . . . . . 8
⊢ (𝑥 = sup({𝑠, 𝑣}, ℝ, < ) → (𝑦 ≤ 𝑥 ↔ 𝑦 ≤ sup({𝑠, 𝑣}, ℝ, < ))) |
80 | 79 | ralbidv 2454 |
. . . . . . 7
⊢ (𝑥 = sup({𝑠, 𝑣}, ℝ, < ) → (∀𝑦 ∈ (𝑢 ∪ {𝑣})𝑦 ≤ 𝑥 ↔ ∀𝑦 ∈ (𝑢 ∪ {𝑣})𝑦 ≤ sup({𝑠, 𝑣}, ℝ, < ))) |
81 | 80 | rspcev 2813 |
. . . . . 6
⊢
((sup({𝑠, 𝑣}, ℝ, < ) ∈
ℝ ∧ ∀𝑦
∈ (𝑢 ∪ {𝑣})𝑦 ≤ sup({𝑠, 𝑣}, ℝ, < )) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ (𝑢 ∪ {𝑣})𝑦 ≤ 𝑥) |
82 | 41, 78, 81 | syl2anc 409 |
. . . . 5
⊢ ((((𝑢 ∈ Fin ∧ (𝑢 ⊆ ℝ →
∃𝑥 ∈ ℝ
∀𝑦 ∈ 𝑢 𝑦 ≤ 𝑥)) ∧ (𝑢 ∪ {𝑣}) ⊆ ℝ) ∧ (𝑠 ∈ ℝ ∧ ∀𝑦 ∈ 𝑢 𝑦 ≤ 𝑠)) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ (𝑢 ∪ {𝑣})𝑦 ≤ 𝑥) |
83 | 33, 82 | rexlimddv 2576 |
. . . 4
⊢ (((𝑢 ∈ Fin ∧ (𝑢 ⊆ ℝ →
∃𝑥 ∈ ℝ
∀𝑦 ∈ 𝑢 𝑦 ≤ 𝑥)) ∧ (𝑢 ∪ {𝑣}) ⊆ ℝ) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ (𝑢 ∪ {𝑣})𝑦 ≤ 𝑥) |
84 | 83 | exp31 362 |
. . 3
⊢ (𝑢 ∈ Fin → ((𝑢 ⊆ ℝ →
∃𝑥 ∈ ℝ
∀𝑦 ∈ 𝑢 𝑦 ≤ 𝑥) → ((𝑢 ∪ {𝑣}) ⊆ ℝ → ∃𝑥 ∈ ℝ ∀𝑦 ∈ (𝑢 ∪ {𝑣})𝑦 ≤ 𝑥))) |
85 | 4, 8, 12, 16, 23, 84 | findcard2 6823 |
. 2
⊢ (𝐴 ∈ Fin → (𝐴 ⊆ ℝ →
∃𝑥 ∈ ℝ
∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)) |
86 | 85 | impcom 124 |
1
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ∈ Fin) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) |