| Step | Hyp | Ref
| Expression |
| 1 | | breq2 5147 |
. . . . 5
⊢ (𝑦 = 𝐴 → (( -us ‘𝑛) <s 𝑦 ↔ ( -us ‘𝑛) <s 𝐴)) |
| 2 | | breq1 5146 |
. . . . 5
⊢ (𝑦 = 𝐴 → (𝑦 <s 𝑛 ↔ 𝐴 <s 𝑛)) |
| 3 | 1, 2 | anbi12d 632 |
. . . 4
⊢ (𝑦 = 𝐴 → ((( -us ‘𝑛) <s 𝑦 ∧ 𝑦 <s 𝑛) ↔ (( -us ‘𝑛) <s 𝐴 ∧ 𝐴 <s 𝑛))) |
| 4 | 3 | rexbidv 3179 |
. . 3
⊢ (𝑦 = 𝐴 → (∃𝑛 ∈ ℕs (( -us
‘𝑛) <s 𝑦 ∧ 𝑦 <s 𝑛) ↔ ∃𝑛 ∈ ℕs (( -us
‘𝑛) <s 𝐴 ∧ 𝐴 <s 𝑛))) |
| 5 | | id 22 |
. . . 4
⊢ (𝑦 = 𝐴 → 𝑦 = 𝐴) |
| 6 | | oveq1 7438 |
. . . . . . . 8
⊢ (𝑦 = 𝐴 → (𝑦 -s ( 1s
/su 𝑛)) =
(𝐴 -s (
1s /su 𝑛))) |
| 7 | 6 | eqeq2d 2748 |
. . . . . . 7
⊢ (𝑦 = 𝐴 → (𝑥 = (𝑦 -s ( 1s
/su 𝑛))
↔ 𝑥 = (𝐴 -s ( 1s
/su 𝑛)))) |
| 8 | 7 | rexbidv 3179 |
. . . . . 6
⊢ (𝑦 = 𝐴 → (∃𝑛 ∈ ℕs 𝑥 = (𝑦 -s ( 1s
/su 𝑛))
↔ ∃𝑛 ∈
ℕs 𝑥 =
(𝐴 -s (
1s /su 𝑛)))) |
| 9 | 8 | abbidv 2808 |
. . . . 5
⊢ (𝑦 = 𝐴 → {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝑦 -s ( 1s
/su 𝑛))} =
{𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 -s ( 1s
/su 𝑛))}) |
| 10 | | oveq1 7438 |
. . . . . . . 8
⊢ (𝑦 = 𝐴 → (𝑦 +s ( 1s
/su 𝑛)) =
(𝐴 +s (
1s /su 𝑛))) |
| 11 | 10 | eqeq2d 2748 |
. . . . . . 7
⊢ (𝑦 = 𝐴 → (𝑥 = (𝑦 +s ( 1s
/su 𝑛))
↔ 𝑥 = (𝐴 +s ( 1s
/su 𝑛)))) |
| 12 | 11 | rexbidv 3179 |
. . . . . 6
⊢ (𝑦 = 𝐴 → (∃𝑛 ∈ ℕs 𝑥 = (𝑦 +s ( 1s
/su 𝑛))
↔ ∃𝑛 ∈
ℕs 𝑥 =
(𝐴 +s (
1s /su 𝑛)))) |
| 13 | 12 | abbidv 2808 |
. . . . 5
⊢ (𝑦 = 𝐴 → {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝑦 +s ( 1s
/su 𝑛))} =
{𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 +s ( 1s
/su 𝑛))}) |
| 14 | 9, 13 | oveq12d 7449 |
. . . 4
⊢ (𝑦 = 𝐴 → ({𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝑦 -s ( 1s
/su 𝑛))} |s
{𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝑦 +s ( 1s
/su 𝑛))}) =
({𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 -s ( 1s
/su 𝑛))} |s
{𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 +s ( 1s
/su 𝑛))})) |
| 15 | 5, 14 | eqeq12d 2753 |
. . 3
⊢ (𝑦 = 𝐴 → (𝑦 = ({𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝑦 -s ( 1s
/su 𝑛))} |s
{𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝑦 +s ( 1s
/su 𝑛))})
↔ 𝐴 = ({𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 -s ( 1s
/su 𝑛))} |s
{𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 +s ( 1s
/su 𝑛))}))) |
| 16 | 4, 15 | anbi12d 632 |
. 2
⊢ (𝑦 = 𝐴 → ((∃𝑛 ∈ ℕs (( -us
‘𝑛) <s 𝑦 ∧ 𝑦 <s 𝑛) ∧ 𝑦 = ({𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝑦 -s ( 1s
/su 𝑛))} |s
{𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝑦 +s ( 1s
/su 𝑛))}))
↔ (∃𝑛 ∈
ℕs (( -us ‘𝑛) <s 𝐴 ∧ 𝐴 <s 𝑛) ∧ 𝐴 = ({𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 -s ( 1s
/su 𝑛))} |s
{𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 +s ( 1s
/su 𝑛))})))) |
| 17 | | df-reno 28426 |
. 2
⊢
ℝs = {𝑦 ∈ No
∣ (∃𝑛 ∈
ℕs (( -us ‘𝑛) <s 𝑦 ∧ 𝑦 <s 𝑛) ∧ 𝑦 = ({𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝑦 -s ( 1s
/su 𝑛))} |s
{𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝑦 +s ( 1s
/su 𝑛))}))} |
| 18 | 16, 17 | elrab2 3695 |
1
⊢ (𝐴 ∈ ℝs
↔ (𝐴 ∈ No ∧ (∃𝑛 ∈ ℕs (( -us
‘𝑛) <s 𝐴 ∧ 𝐴 <s 𝑛) ∧ 𝐴 = ({𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 -s ( 1s
/su 𝑛))} |s
{𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 +s ( 1s
/su 𝑛))})))) |