Step |
Hyp |
Ref |
Expression |
1 |
|
nfv |
⊢ Ⅎ 𝑤 𝐴 ⊆ ℝ* |
2 |
|
nfra1 |
⊢ Ⅎ 𝑤 ∀ 𝑤 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑦 < 𝑤 |
3 |
1 2
|
nfan |
⊢ Ⅎ 𝑤 ( 𝐴 ⊆ ℝ* ∧ ∀ 𝑤 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑦 < 𝑤 ) |
4 |
|
simpll |
⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ ∀ 𝑤 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑦 < 𝑤 ) ∧ 𝑤 ∈ ℝ ) → 𝐴 ⊆ ℝ* ) |
5 |
|
simpr |
⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ ∀ 𝑤 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑦 < 𝑤 ) ∧ 𝑤 ∈ ℝ ) → 𝑤 ∈ ℝ ) |
6 |
|
rspa |
⊢ ( ( ∀ 𝑤 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑦 < 𝑤 ∧ 𝑤 ∈ ℝ ) → ∃ 𝑦 ∈ 𝐴 𝑦 < 𝑤 ) |
7 |
6
|
adantll |
⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ ∀ 𝑤 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑦 < 𝑤 ) ∧ 𝑤 ∈ ℝ ) → ∃ 𝑦 ∈ 𝐴 𝑦 < 𝑤 ) |
8 |
|
ssel2 |
⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ ℝ* ) |
9 |
8
|
ad4ant13 |
⊢ ( ( ( ( 𝐴 ⊆ ℝ* ∧ 𝑤 ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑦 < 𝑤 ) → 𝑦 ∈ ℝ* ) |
10 |
|
simpllr |
⊢ ( ( ( ( 𝐴 ⊆ ℝ* ∧ 𝑤 ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑦 < 𝑤 ) → 𝑤 ∈ ℝ ) |
11 |
10
|
rexrd |
⊢ ( ( ( ( 𝐴 ⊆ ℝ* ∧ 𝑤 ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑦 < 𝑤 ) → 𝑤 ∈ ℝ* ) |
12 |
|
simpr |
⊢ ( ( ( ( 𝐴 ⊆ ℝ* ∧ 𝑤 ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑦 < 𝑤 ) → 𝑦 < 𝑤 ) |
13 |
9 11 12
|
xrltled |
⊢ ( ( ( ( 𝐴 ⊆ ℝ* ∧ 𝑤 ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑦 < 𝑤 ) → 𝑦 ≤ 𝑤 ) |
14 |
13
|
ex |
⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ 𝑤 ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑦 < 𝑤 → 𝑦 ≤ 𝑤 ) ) |
15 |
14
|
reximdva |
⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝑤 ∈ ℝ ) → ( ∃ 𝑦 ∈ 𝐴 𝑦 < 𝑤 → ∃ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑤 ) ) |
16 |
15
|
imp |
⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ 𝑤 ∈ ℝ ) ∧ ∃ 𝑦 ∈ 𝐴 𝑦 < 𝑤 ) → ∃ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑤 ) |
17 |
4 5 7 16
|
syl21anc |
⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ ∀ 𝑤 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑦 < 𝑤 ) ∧ 𝑤 ∈ ℝ ) → ∃ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑤 ) |
18 |
3 17
|
ralrimia |
⊢ ( ( 𝐴 ⊆ ℝ* ∧ ∀ 𝑤 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑦 < 𝑤 ) → ∀ 𝑤 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑤 ) |
19 |
|
breq2 |
⊢ ( 𝑤 = 𝑥 → ( 𝑦 ≤ 𝑤 ↔ 𝑦 ≤ 𝑥 ) ) |
20 |
19
|
rexbidv |
⊢ ( 𝑤 = 𝑥 → ( ∃ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑤 ↔ ∃ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) ) |
21 |
20
|
cbvralvw |
⊢ ( ∀ 𝑤 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑤 ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) |
22 |
18 21
|
sylib |
⊢ ( ( 𝐴 ⊆ ℝ* ∧ ∀ 𝑤 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑦 < 𝑤 ) → ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) |
23 |
22
|
ex |
⊢ ( 𝐴 ⊆ ℝ* → ( ∀ 𝑤 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑦 < 𝑤 → ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) ) |
24 |
|
simpll |
⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) ∧ 𝑤 ∈ ℝ ) → 𝐴 ⊆ ℝ* ) |
25 |
|
simpr |
⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) ∧ 𝑤 ∈ ℝ ) → 𝑤 ∈ ℝ ) |
26 |
|
peano2rem |
⊢ ( 𝑤 ∈ ℝ → ( 𝑤 − 1 ) ∈ ℝ ) |
27 |
26
|
adantl |
⊢ ( ( ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ∧ 𝑤 ∈ ℝ ) → ( 𝑤 − 1 ) ∈ ℝ ) |
28 |
|
simpl |
⊢ ( ( ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ∧ 𝑤 ∈ ℝ ) → ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) |
29 |
|
breq2 |
⊢ ( 𝑥 = ( 𝑤 − 1 ) → ( 𝑦 ≤ 𝑥 ↔ 𝑦 ≤ ( 𝑤 − 1 ) ) ) |
30 |
29
|
rexbidv |
⊢ ( 𝑥 = ( 𝑤 − 1 ) → ( ∃ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ↔ ∃ 𝑦 ∈ 𝐴 𝑦 ≤ ( 𝑤 − 1 ) ) ) |
31 |
30
|
rspcva |
⊢ ( ( ( 𝑤 − 1 ) ∈ ℝ ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) → ∃ 𝑦 ∈ 𝐴 𝑦 ≤ ( 𝑤 − 1 ) ) |
32 |
27 28 31
|
syl2anc |
⊢ ( ( ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ∧ 𝑤 ∈ ℝ ) → ∃ 𝑦 ∈ 𝐴 𝑦 ≤ ( 𝑤 − 1 ) ) |
33 |
32
|
adantll |
⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) ∧ 𝑤 ∈ ℝ ) → ∃ 𝑦 ∈ 𝐴 𝑦 ≤ ( 𝑤 − 1 ) ) |
34 |
8
|
ad4ant13 |
⊢ ( ( ( ( 𝐴 ⊆ ℝ* ∧ 𝑤 ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑦 ≤ ( 𝑤 − 1 ) ) → 𝑦 ∈ ℝ* ) |
35 |
|
simpllr |
⊢ ( ( ( ( 𝐴 ⊆ ℝ* ∧ 𝑤 ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑦 ≤ ( 𝑤 − 1 ) ) → 𝑤 ∈ ℝ ) |
36 |
26
|
rexrd |
⊢ ( 𝑤 ∈ ℝ → ( 𝑤 − 1 ) ∈ ℝ* ) |
37 |
35 36
|
syl |
⊢ ( ( ( ( 𝐴 ⊆ ℝ* ∧ 𝑤 ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑦 ≤ ( 𝑤 − 1 ) ) → ( 𝑤 − 1 ) ∈ ℝ* ) |
38 |
35
|
rexrd |
⊢ ( ( ( ( 𝐴 ⊆ ℝ* ∧ 𝑤 ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑦 ≤ ( 𝑤 − 1 ) ) → 𝑤 ∈ ℝ* ) |
39 |
|
simpr |
⊢ ( ( ( ( 𝐴 ⊆ ℝ* ∧ 𝑤 ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑦 ≤ ( 𝑤 − 1 ) ) → 𝑦 ≤ ( 𝑤 − 1 ) ) |
40 |
35
|
ltm1d |
⊢ ( ( ( ( 𝐴 ⊆ ℝ* ∧ 𝑤 ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑦 ≤ ( 𝑤 − 1 ) ) → ( 𝑤 − 1 ) < 𝑤 ) |
41 |
34 37 38 39 40
|
xrlelttrd |
⊢ ( ( ( ( 𝐴 ⊆ ℝ* ∧ 𝑤 ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑦 ≤ ( 𝑤 − 1 ) ) → 𝑦 < 𝑤 ) |
42 |
41
|
ex |
⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ 𝑤 ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑦 ≤ ( 𝑤 − 1 ) → 𝑦 < 𝑤 ) ) |
43 |
42
|
reximdva |
⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝑤 ∈ ℝ ) → ( ∃ 𝑦 ∈ 𝐴 𝑦 ≤ ( 𝑤 − 1 ) → ∃ 𝑦 ∈ 𝐴 𝑦 < 𝑤 ) ) |
44 |
43
|
imp |
⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ 𝑤 ∈ ℝ ) ∧ ∃ 𝑦 ∈ 𝐴 𝑦 ≤ ( 𝑤 − 1 ) ) → ∃ 𝑦 ∈ 𝐴 𝑦 < 𝑤 ) |
45 |
24 25 33 44
|
syl21anc |
⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) ∧ 𝑤 ∈ ℝ ) → ∃ 𝑦 ∈ 𝐴 𝑦 < 𝑤 ) |
46 |
45
|
ralrimiva |
⊢ ( ( 𝐴 ⊆ ℝ* ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) → ∀ 𝑤 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑦 < 𝑤 ) |
47 |
46
|
ex |
⊢ ( 𝐴 ⊆ ℝ* → ( ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 → ∀ 𝑤 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑦 < 𝑤 ) ) |
48 |
23 47
|
impbid |
⊢ ( 𝐴 ⊆ ℝ* → ( ∀ 𝑤 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑦 < 𝑤 ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) ) |