Theorem elreno

Description: Membership in the set of surreal reals. (Contributed by Scott Fenton, 15-Apr-2025)

	Ref	Expression
Assertion	elreno	$$⊢A\in {ℝ}_s\leftrightarrow \left(A\in \mathrm{No}\wedge \left(\exists n\in {\mathbb{N}}_s\left({+}_s\left(n\right){<}_{s}A\wedge A{<}_{s}n\right)\wedge A=\left\{x|\exists n\in {\mathbb{N}}_{s}x=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}{|}_s\left\{x|\exists n\in {\mathbb{N}}_{s}x=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		breq2	$$⊢y=A\to \left({+}_s\left(n\right){<}_{s}y\leftrightarrow {+}_s\left(n\right){<}_{s}A\right)$$
2		breq1	$$⊢y=A\to \left(y{<}_{s}n\leftrightarrow A{<}_{s}n\right)$$
3	1 2	anbi12d	$$⊢y=A\to \left(\left({+}_s\left(n\right){<}_{s}y\wedge y{<}_{s}n\right)\leftrightarrow \left({+}_s\left(n\right){<}_{s}A\wedge A{<}_{s}n\right)\right)$$
4	3	rexbidv	$$⊢y=A\to \left(\exists n\in {\mathbb{N}}_s\left({+}_s\left(n\right){<}_{s}y\wedge y{<}_{s}n\right)\leftrightarrow \exists n\in {\mathbb{N}}_s\left({+}_s\left(n\right){<}_{s}A\wedge A{<}_{s}n\right)\right)$$
5		id	$$⊢y=A\to y=A$$
6		oveq1	$$⊢y=A\to y{-}_s\left(1_s{/}_{\mathrm{su}}n\right)=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)$$
7	6	eqeq2d	$$⊢y=A\to \left(x=y{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\leftrightarrow x=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right)$$
8	7	rexbidv	$$⊢y=A\to \left(\exists n\in {\mathbb{N}}_{s}x=y{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\leftrightarrow \exists n\in {\mathbb{N}}_{s}x=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right)$$
9	8	abbidv	$$⊢y=A\to \left\{x|\exists n\in {\mathbb{N}}_{s}x=y{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}=\left\{x|\exists n\in {\mathbb{N}}_{s}x=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}$$
10		oveq1	$$⊢y=A\to y{+}_s\left(1_s{/}_{\mathrm{su}}n\right)=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)$$
11	10	eqeq2d	$$⊢y=A\to \left(x=y{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\leftrightarrow x=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right)$$
12	11	rexbidv	$$⊢y=A\to \left(\exists n\in {\mathbb{N}}_{s}x=y{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\leftrightarrow \exists n\in {\mathbb{N}}_{s}x=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right)$$
13	12	abbidv	$$⊢y=A\to \left\{x|\exists n\in {\mathbb{N}}_{s}x=y{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}=\left\{x|\exists n\in {\mathbb{N}}_{s}x=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}$$
14	9 13	oveq12d	$$⊢y=A\to \left\{x|\exists n\in {\mathbb{N}}_{s}x=y{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}{|}_s\left\{x|\exists n\in {\mathbb{N}}_{s}x=y{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}=\left\{x|\exists n\in {\mathbb{N}}_{s}x=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}{|}_s\left\{x|\exists n\in {\mathbb{N}}_{s}x=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}$$
15	5 14	eqeq12d	$$⊢y=A\to \left(y=\left\{x|\exists n\in {\mathbb{N}}_{s}x=y{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}{|}_s\left\{x|\exists n\in {\mathbb{N}}_{s}x=y{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}\leftrightarrow A=\left\{x|\exists n\in {\mathbb{N}}_{s}x=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}{|}_s\left\{x|\exists n\in {\mathbb{N}}_{s}x=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}\right)$$
16	4 15	anbi12d	$$⊢y=A\to \left(\left(\exists n\in {\mathbb{N}}_s\left({+}_s\left(n\right){<}_{s}y\wedge y{<}_{s}n\right)\wedge y=\left\{x|\exists n\in {\mathbb{N}}_{s}x=y{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}{|}_s\left\{x|\exists n\in {\mathbb{N}}_{s}x=y{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}\right)\leftrightarrow \left(\exists n\in {\mathbb{N}}_s\left({+}_s\left(n\right){<}_{s}A\wedge A{<}_{s}n\right)\wedge A=\left\{x|\exists n\in {\mathbb{N}}_{s}x=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}{|}_s\left\{x|\exists n\in {\mathbb{N}}_{s}x=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}\right)\right)$$
17		df-reno	$$⊢{ℝ}_s=\left\{y\in \mathrm{No}|\left(\exists n\in {\mathbb{N}}_s\left({+}_s\left(n\right){<}_{s}y\wedge y{<}_{s}n\right)\wedge y=\left\{x|\exists n\in {\mathbb{N}}_{s}x=y{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}{|}_s\left\{x|\exists n\in {\mathbb{N}}_{s}x=y{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}\right)\right\}$$
18	16 17	elrab2	$$⊢A\in {ℝ}_s\leftrightarrow \left(A\in \mathrm{No}\wedge \left(\exists n\in {\mathbb{N}}_s\left({+}_s\left(n\right){<}_{s}A\wedge A{<}_{s}n\right)\wedge A=\left\{x|\exists n\in {\mathbb{N}}_{s}x=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}{|}_s\left\{x|\exists n\in {\mathbb{N}}_{s}x=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}\right)\right)$$