Step |
Hyp |
Ref |
Expression |
0 |
|
cA |
⊢ 𝐴 |
1 |
|
cr |
⊢ ℝ |
2 |
0 1
|
wss |
⊢ 𝐴 ⊆ ℝ |
3 |
|
c0 |
⊢ ∅ |
4 |
0 3
|
wne |
⊢ 𝐴 ≠ ∅ |
5 |
|
vx |
⊢ 𝑥 |
6 |
|
vy |
⊢ 𝑦 |
7 |
6
|
cv |
⊢ 𝑦 |
8 |
|
cltrr |
⊢ <ℝ |
9 |
5
|
cv |
⊢ 𝑥 |
10 |
7 9 8
|
wbr |
⊢ 𝑦 <ℝ 𝑥 |
11 |
10 6 0
|
wral |
⊢ ∀ 𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥 |
12 |
11 5 1
|
wrex |
⊢ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥 |
13 |
2 4 12
|
w3a |
⊢ ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥 ) |
14 |
9 7 8
|
wbr |
⊢ 𝑥 <ℝ 𝑦 |
15 |
14
|
wn |
⊢ ¬ 𝑥 <ℝ 𝑦 |
16 |
15 6 0
|
wral |
⊢ ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <ℝ 𝑦 |
17 |
|
vz |
⊢ 𝑧 |
18 |
17
|
cv |
⊢ 𝑧 |
19 |
7 18 8
|
wbr |
⊢ 𝑦 <ℝ 𝑧 |
20 |
19 17 0
|
wrex |
⊢ ∃ 𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧 |
21 |
10 20
|
wi |
⊢ ( 𝑦 <ℝ 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧 ) |
22 |
21 6 1
|
wral |
⊢ ∀ 𝑦 ∈ ℝ ( 𝑦 <ℝ 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧 ) |
23 |
16 22
|
wa |
⊢ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <ℝ 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 <ℝ 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧 ) ) |
24 |
23 5 1
|
wrex |
⊢ ∃ 𝑥 ∈ ℝ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <ℝ 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 <ℝ 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧 ) ) |
25 |
13 24
|
wi |
⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥 ) → ∃ 𝑥 ∈ ℝ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <ℝ 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 <ℝ 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧 ) ) ) |