Step |
Hyp |
Ref |
Expression |
1 |
|
peano2re |
⊢ ( 𝑤 ∈ ℝ → ( 𝑤 + 1 ) ∈ ℝ ) |
2 |
1
|
adantl |
⊢ ( ( ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ∧ 𝑤 ∈ ℝ ) → ( 𝑤 + 1 ) ∈ ℝ ) |
3 |
|
simpl |
⊢ ( ( ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ∧ 𝑤 ∈ ℝ ) → ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) |
4 |
|
breq1 |
⊢ ( 𝑥 = ( 𝑤 + 1 ) → ( 𝑥 ≤ 𝑦 ↔ ( 𝑤 + 1 ) ≤ 𝑦 ) ) |
5 |
4
|
rexbidv |
⊢ ( 𝑥 = ( 𝑤 + 1 ) → ( ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ↔ ∃ 𝑦 ∈ 𝐴 ( 𝑤 + 1 ) ≤ 𝑦 ) ) |
6 |
5
|
rspcva |
⊢ ( ( ( 𝑤 + 1 ) ∈ ℝ ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) → ∃ 𝑦 ∈ 𝐴 ( 𝑤 + 1 ) ≤ 𝑦 ) |
7 |
2 3 6
|
syl2anc |
⊢ ( ( ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ∧ 𝑤 ∈ ℝ ) → ∃ 𝑦 ∈ 𝐴 ( 𝑤 + 1 ) ≤ 𝑦 ) |
8 |
7
|
adantll |
⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) ∧ 𝑤 ∈ ℝ ) → ∃ 𝑦 ∈ 𝐴 ( 𝑤 + 1 ) ≤ 𝑦 ) |
9 |
|
nfv |
⊢ Ⅎ 𝑦 𝐴 ⊆ ℝ* |
10 |
|
nfcv |
⊢ Ⅎ 𝑦 ℝ |
11 |
|
nfre1 |
⊢ Ⅎ 𝑦 ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 |
12 |
10 11
|
nfralw |
⊢ Ⅎ 𝑦 ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 |
13 |
9 12
|
nfan |
⊢ Ⅎ 𝑦 ( 𝐴 ⊆ ℝ* ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) |
14 |
|
nfv |
⊢ Ⅎ 𝑦 𝑤 ∈ ℝ |
15 |
13 14
|
nfan |
⊢ Ⅎ 𝑦 ( ( 𝐴 ⊆ ℝ* ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) ∧ 𝑤 ∈ ℝ ) |
16 |
|
simp1r |
⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ 𝑤 ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ∧ ( 𝑤 + 1 ) ≤ 𝑦 ) → 𝑤 ∈ ℝ ) |
17 |
|
rexr |
⊢ ( 𝑤 ∈ ℝ → 𝑤 ∈ ℝ* ) |
18 |
16 17
|
syl |
⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ 𝑤 ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ∧ ( 𝑤 + 1 ) ≤ 𝑦 ) → 𝑤 ∈ ℝ* ) |
19 |
1
|
rexrd |
⊢ ( 𝑤 ∈ ℝ → ( 𝑤 + 1 ) ∈ ℝ* ) |
20 |
16 19
|
syl |
⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ 𝑤 ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ∧ ( 𝑤 + 1 ) ≤ 𝑦 ) → ( 𝑤 + 1 ) ∈ ℝ* ) |
21 |
|
simp1l |
⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ 𝑤 ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ∧ ( 𝑤 + 1 ) ≤ 𝑦 ) → 𝐴 ⊆ ℝ* ) |
22 |
|
simp2 |
⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ 𝑤 ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ∧ ( 𝑤 + 1 ) ≤ 𝑦 ) → 𝑦 ∈ 𝐴 ) |
23 |
|
ssel2 |
⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ ℝ* ) |
24 |
21 22 23
|
syl2anc |
⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ 𝑤 ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ∧ ( 𝑤 + 1 ) ≤ 𝑦 ) → 𝑦 ∈ ℝ* ) |
25 |
16
|
ltp1d |
⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ 𝑤 ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ∧ ( 𝑤 + 1 ) ≤ 𝑦 ) → 𝑤 < ( 𝑤 + 1 ) ) |
26 |
|
simp3 |
⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ 𝑤 ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ∧ ( 𝑤 + 1 ) ≤ 𝑦 ) → ( 𝑤 + 1 ) ≤ 𝑦 ) |
27 |
18 20 24 25 26
|
xrltletrd |
⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ 𝑤 ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ∧ ( 𝑤 + 1 ) ≤ 𝑦 ) → 𝑤 < 𝑦 ) |
28 |
27
|
3exp |
⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝑤 ∈ ℝ ) → ( 𝑦 ∈ 𝐴 → ( ( 𝑤 + 1 ) ≤ 𝑦 → 𝑤 < 𝑦 ) ) ) |
29 |
28
|
adantlr |
⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) ∧ 𝑤 ∈ ℝ ) → ( 𝑦 ∈ 𝐴 → ( ( 𝑤 + 1 ) ≤ 𝑦 → 𝑤 < 𝑦 ) ) ) |
30 |
15 29
|
reximdai |
⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) ∧ 𝑤 ∈ ℝ ) → ( ∃ 𝑦 ∈ 𝐴 ( 𝑤 + 1 ) ≤ 𝑦 → ∃ 𝑦 ∈ 𝐴 𝑤 < 𝑦 ) ) |
31 |
8 30
|
mpd |
⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) ∧ 𝑤 ∈ ℝ ) → ∃ 𝑦 ∈ 𝐴 𝑤 < 𝑦 ) |
32 |
31
|
ralrimiva |
⊢ ( ( 𝐴 ⊆ ℝ* ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) → ∀ 𝑤 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑤 < 𝑦 ) |
33 |
32
|
ex |
⊢ ( 𝐴 ⊆ ℝ* → ( ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 → ∀ 𝑤 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑤 < 𝑦 ) ) |
34 |
|
breq1 |
⊢ ( 𝑤 = 𝑥 → ( 𝑤 < 𝑦 ↔ 𝑥 < 𝑦 ) ) |
35 |
34
|
rexbidv |
⊢ ( 𝑤 = 𝑥 → ( ∃ 𝑦 ∈ 𝐴 𝑤 < 𝑦 ↔ ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) ) |
36 |
35
|
cbvralvw |
⊢ ( ∀ 𝑤 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑤 < 𝑦 ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) |
37 |
36
|
biimpi |
⊢ ( ∀ 𝑤 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑤 < 𝑦 → ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) |
38 |
|
nfv |
⊢ Ⅎ 𝑥 𝐴 ⊆ ℝ* |
39 |
|
nfra1 |
⊢ Ⅎ 𝑥 ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 |
40 |
38 39
|
nfan |
⊢ Ⅎ 𝑥 ( 𝐴 ⊆ ℝ* ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) |
41 |
|
simpll |
⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) ∧ 𝑥 ∈ ℝ ) → 𝐴 ⊆ ℝ* ) |
42 |
|
simpr |
⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) ∧ 𝑥 ∈ ℝ ) → 𝑥 ∈ ℝ ) |
43 |
|
rspa |
⊢ ( ( ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ∧ 𝑥 ∈ ℝ ) → ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) |
44 |
43
|
adantll |
⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) ∧ 𝑥 ∈ ℝ ) → ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) |
45 |
|
rexr |
⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℝ* ) |
46 |
45
|
ad3antlr |
⊢ ( ( ( ( 𝐴 ⊆ ℝ* ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 < 𝑦 ) → 𝑥 ∈ ℝ* ) |
47 |
23
|
adantr |
⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 < 𝑦 ) → 𝑦 ∈ ℝ* ) |
48 |
47
|
adantllr |
⊢ ( ( ( ( 𝐴 ⊆ ℝ* ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 < 𝑦 ) → 𝑦 ∈ ℝ* ) |
49 |
|
simpr |
⊢ ( ( ( ( 𝐴 ⊆ ℝ* ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 < 𝑦 ) → 𝑥 < 𝑦 ) |
50 |
46 48 49
|
xrltled |
⊢ ( ( ( ( 𝐴 ⊆ ℝ* ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 < 𝑦 ) → 𝑥 ≤ 𝑦 ) |
51 |
50
|
ex |
⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 < 𝑦 → 𝑥 ≤ 𝑦 ) ) |
52 |
51
|
reximdva |
⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝑥 ∈ ℝ ) → ( ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 → ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) ) |
53 |
52
|
adantlr |
⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) ∧ 𝑥 ∈ ℝ ) → ( ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 → ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) ) |
54 |
44 53
|
mpd |
⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) ∧ 𝑥 ∈ ℝ ) → ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) |
55 |
|
simpr |
⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ 𝑥 ∈ ℝ ) ∧ ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) → ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) |
56 |
41 42 54 55
|
syl21anc |
⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) ∧ 𝑥 ∈ ℝ ) → ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) |
57 |
56
|
ex |
⊢ ( ( 𝐴 ⊆ ℝ* ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) → ( 𝑥 ∈ ℝ → ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) ) |
58 |
40 57
|
ralrimi |
⊢ ( ( 𝐴 ⊆ ℝ* ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) → ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) |
59 |
37 58
|
sylan2 |
⊢ ( ( 𝐴 ⊆ ℝ* ∧ ∀ 𝑤 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑤 < 𝑦 ) → ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) |
60 |
59
|
ex |
⊢ ( 𝐴 ⊆ ℝ* → ( ∀ 𝑤 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑤 < 𝑦 → ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) ) |
61 |
33 60
|
impbid |
⊢ ( 𝐴 ⊆ ℝ* → ( ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ↔ ∀ 𝑤 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑤 < 𝑦 ) ) |
62 |
|
supxrunb2 |
⊢ ( 𝐴 ⊆ ℝ* → ( ∀ 𝑤 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑤 < 𝑦 ↔ sup ( 𝐴 , ℝ* , < ) = +∞ ) ) |
63 |
61 62
|
bitrd |
⊢ ( 𝐴 ⊆ ℝ* → ( ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ↔ sup ( 𝐴 , ℝ* , < ) = +∞ ) ) |