Step |
Hyp |
Ref |
Expression |
1 |
|
nnssz |
⊢ ℕ ⊆ ℤ |
2 |
|
arch |
⊢ ( 𝐴 ∈ ℝ → ∃ 𝑧 ∈ ℕ 𝐴 < 𝑧 ) |
3 |
|
ssrexv |
⊢ ( ℕ ⊆ ℤ → ( ∃ 𝑧 ∈ ℕ 𝐴 < 𝑧 → ∃ 𝑧 ∈ ℤ 𝐴 < 𝑧 ) ) |
4 |
1 2 3
|
mpsyl |
⊢ ( 𝐴 ∈ ℝ → ∃ 𝑧 ∈ ℤ 𝐴 < 𝑧 ) |
5 |
|
zre |
⊢ ( 𝑧 ∈ ℤ → 𝑧 ∈ ℝ ) |
6 |
|
ltle |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ ) → ( 𝐴 < 𝑧 → 𝐴 ≤ 𝑧 ) ) |
7 |
5 6
|
sylan2 |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑧 ∈ ℤ ) → ( 𝐴 < 𝑧 → 𝐴 ≤ 𝑧 ) ) |
8 |
7
|
reximdva |
⊢ ( 𝐴 ∈ ℝ → ( ∃ 𝑧 ∈ ℤ 𝐴 < 𝑧 → ∃ 𝑧 ∈ ℤ 𝐴 ≤ 𝑧 ) ) |
9 |
4 8
|
mpd |
⊢ ( 𝐴 ∈ ℝ → ∃ 𝑧 ∈ ℤ 𝐴 ≤ 𝑧 ) |
10 |
|
rabn0 |
⊢ ( { 𝑧 ∈ ℤ ∣ 𝐴 ≤ 𝑧 } ≠ ∅ ↔ ∃ 𝑧 ∈ ℤ 𝐴 ≤ 𝑧 ) |
11 |
9 10
|
sylibr |
⊢ ( 𝐴 ∈ ℝ → { 𝑧 ∈ ℤ ∣ 𝐴 ≤ 𝑧 } ≠ ∅ ) |
12 |
|
breq2 |
⊢ ( 𝑧 = 𝑛 → ( 𝐴 ≤ 𝑧 ↔ 𝐴 ≤ 𝑛 ) ) |
13 |
12
|
cbvrabv |
⊢ { 𝑧 ∈ ℤ ∣ 𝐴 ≤ 𝑧 } = { 𝑛 ∈ ℤ ∣ 𝐴 ≤ 𝑛 } |
14 |
13
|
eqimssi |
⊢ { 𝑧 ∈ ℤ ∣ 𝐴 ≤ 𝑧 } ⊆ { 𝑛 ∈ ℤ ∣ 𝐴 ≤ 𝑛 } |
15 |
|
uzwo3 |
⊢ ( ( 𝐴 ∈ ℝ ∧ ( { 𝑧 ∈ ℤ ∣ 𝐴 ≤ 𝑧 } ⊆ { 𝑛 ∈ ℤ ∣ 𝐴 ≤ 𝑛 } ∧ { 𝑧 ∈ ℤ ∣ 𝐴 ≤ 𝑧 } ≠ ∅ ) ) → ∃! 𝑥 ∈ { 𝑧 ∈ ℤ ∣ 𝐴 ≤ 𝑧 } ∀ 𝑦 ∈ { 𝑧 ∈ ℤ ∣ 𝐴 ≤ 𝑧 } 𝑥 ≤ 𝑦 ) |
16 |
14 15
|
mpanr1 |
⊢ ( ( 𝐴 ∈ ℝ ∧ { 𝑧 ∈ ℤ ∣ 𝐴 ≤ 𝑧 } ≠ ∅ ) → ∃! 𝑥 ∈ { 𝑧 ∈ ℤ ∣ 𝐴 ≤ 𝑧 } ∀ 𝑦 ∈ { 𝑧 ∈ ℤ ∣ 𝐴 ≤ 𝑧 } 𝑥 ≤ 𝑦 ) |
17 |
11 16
|
mpdan |
⊢ ( 𝐴 ∈ ℝ → ∃! 𝑥 ∈ { 𝑧 ∈ ℤ ∣ 𝐴 ≤ 𝑧 } ∀ 𝑦 ∈ { 𝑧 ∈ ℤ ∣ 𝐴 ≤ 𝑧 } 𝑥 ≤ 𝑦 ) |
18 |
|
breq2 |
⊢ ( 𝑧 = 𝑥 → ( 𝐴 ≤ 𝑧 ↔ 𝐴 ≤ 𝑥 ) ) |
19 |
18
|
elrab |
⊢ ( 𝑥 ∈ { 𝑧 ∈ ℤ ∣ 𝐴 ≤ 𝑧 } ↔ ( 𝑥 ∈ ℤ ∧ 𝐴 ≤ 𝑥 ) ) |
20 |
|
breq2 |
⊢ ( 𝑧 = 𝑦 → ( 𝐴 ≤ 𝑧 ↔ 𝐴 ≤ 𝑦 ) ) |
21 |
20
|
ralrab |
⊢ ( ∀ 𝑦 ∈ { 𝑧 ∈ ℤ ∣ 𝐴 ≤ 𝑧 } 𝑥 ≤ 𝑦 ↔ ∀ 𝑦 ∈ ℤ ( 𝐴 ≤ 𝑦 → 𝑥 ≤ 𝑦 ) ) |
22 |
19 21
|
anbi12i |
⊢ ( ( 𝑥 ∈ { 𝑧 ∈ ℤ ∣ 𝐴 ≤ 𝑧 } ∧ ∀ 𝑦 ∈ { 𝑧 ∈ ℤ ∣ 𝐴 ≤ 𝑧 } 𝑥 ≤ 𝑦 ) ↔ ( ( 𝑥 ∈ ℤ ∧ 𝐴 ≤ 𝑥 ) ∧ ∀ 𝑦 ∈ ℤ ( 𝐴 ≤ 𝑦 → 𝑥 ≤ 𝑦 ) ) ) |
23 |
|
anass |
⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝐴 ≤ 𝑥 ) ∧ ∀ 𝑦 ∈ ℤ ( 𝐴 ≤ 𝑦 → 𝑥 ≤ 𝑦 ) ) ↔ ( 𝑥 ∈ ℤ ∧ ( 𝐴 ≤ 𝑥 ∧ ∀ 𝑦 ∈ ℤ ( 𝐴 ≤ 𝑦 → 𝑥 ≤ 𝑦 ) ) ) ) |
24 |
22 23
|
bitri |
⊢ ( ( 𝑥 ∈ { 𝑧 ∈ ℤ ∣ 𝐴 ≤ 𝑧 } ∧ ∀ 𝑦 ∈ { 𝑧 ∈ ℤ ∣ 𝐴 ≤ 𝑧 } 𝑥 ≤ 𝑦 ) ↔ ( 𝑥 ∈ ℤ ∧ ( 𝐴 ≤ 𝑥 ∧ ∀ 𝑦 ∈ ℤ ( 𝐴 ≤ 𝑦 → 𝑥 ≤ 𝑦 ) ) ) ) |
25 |
24
|
eubii |
⊢ ( ∃! 𝑥 ( 𝑥 ∈ { 𝑧 ∈ ℤ ∣ 𝐴 ≤ 𝑧 } ∧ ∀ 𝑦 ∈ { 𝑧 ∈ ℤ ∣ 𝐴 ≤ 𝑧 } 𝑥 ≤ 𝑦 ) ↔ ∃! 𝑥 ( 𝑥 ∈ ℤ ∧ ( 𝐴 ≤ 𝑥 ∧ ∀ 𝑦 ∈ ℤ ( 𝐴 ≤ 𝑦 → 𝑥 ≤ 𝑦 ) ) ) ) |
26 |
|
df-reu |
⊢ ( ∃! 𝑥 ∈ { 𝑧 ∈ ℤ ∣ 𝐴 ≤ 𝑧 } ∀ 𝑦 ∈ { 𝑧 ∈ ℤ ∣ 𝐴 ≤ 𝑧 } 𝑥 ≤ 𝑦 ↔ ∃! 𝑥 ( 𝑥 ∈ { 𝑧 ∈ ℤ ∣ 𝐴 ≤ 𝑧 } ∧ ∀ 𝑦 ∈ { 𝑧 ∈ ℤ ∣ 𝐴 ≤ 𝑧 } 𝑥 ≤ 𝑦 ) ) |
27 |
|
df-reu |
⊢ ( ∃! 𝑥 ∈ ℤ ( 𝐴 ≤ 𝑥 ∧ ∀ 𝑦 ∈ ℤ ( 𝐴 ≤ 𝑦 → 𝑥 ≤ 𝑦 ) ) ↔ ∃! 𝑥 ( 𝑥 ∈ ℤ ∧ ( 𝐴 ≤ 𝑥 ∧ ∀ 𝑦 ∈ ℤ ( 𝐴 ≤ 𝑦 → 𝑥 ≤ 𝑦 ) ) ) ) |
28 |
25 26 27
|
3bitr4i |
⊢ ( ∃! 𝑥 ∈ { 𝑧 ∈ ℤ ∣ 𝐴 ≤ 𝑧 } ∀ 𝑦 ∈ { 𝑧 ∈ ℤ ∣ 𝐴 ≤ 𝑧 } 𝑥 ≤ 𝑦 ↔ ∃! 𝑥 ∈ ℤ ( 𝐴 ≤ 𝑥 ∧ ∀ 𝑦 ∈ ℤ ( 𝐴 ≤ 𝑦 → 𝑥 ≤ 𝑦 ) ) ) |
29 |
17 28
|
sylib |
⊢ ( 𝐴 ∈ ℝ → ∃! 𝑥 ∈ ℤ ( 𝐴 ≤ 𝑥 ∧ ∀ 𝑦 ∈ ℤ ( 𝐴 ≤ 𝑦 → 𝑥 ≤ 𝑦 ) ) ) |