Theorem right1s

Description: The right set of 1s is empty . (Contributed by Scott Fenton, 4-Feb-2025)

	Ref	Expression
Assertion	right1s	$$⊢R\left(1_s\right)=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		rightval	$$⊢R\left(1_s\right)=\left\{x\in \mathrm{Old}\left(\mathrm{bday}\left(1_s\right)\right)|1_s{<}_{s}x\right\}$$
2		bday1	$$⊢\mathrm{bday}\left(1_s\right)=1_{𝑜}$$
3	2	fveq2i	$$⊢\mathrm{Old}\left(\mathrm{bday}\left(1_s\right)\right)=\mathrm{Old}\left(1_{𝑜}\right)$$
4		old1	$$⊢\mathrm{Old}\left(1_{𝑜}\right)=\left\{0_s\right\}$$
5	3 4	eqtri	$$⊢\mathrm{Old}\left(\mathrm{bday}\left(1_s\right)\right)=\left\{0_s\right\}$$
6	5	rabeqi	$$⊢\left\{x\in \mathrm{Old}\left(\mathrm{bday}\left(1_s\right)\right)|1_s{<}_{s}x\right\}=\left\{x\in \left\{0_s\right\}|1_s{<}_{s}x\right\}$$
7		breq2	$$⊢x=0_s\to \left(1_s{<}_{s}x\leftrightarrow 1_s{<}_s{0}_s\right)$$
8	7	rabsnif	$$⊢\left\{x\in \left\{0_s\right\}|1_s{<}_{s}x\right\}=if\left(1_s{<}_s{0}_s,\left\{0_s\right\},\varnothing \right)$$
9	6 8	eqtri	$$⊢\left\{x\in \mathrm{Old}\left(\mathrm{bday}\left(1_s\right)\right)|1_s{<}_{s}x\right\}=if\left(1_s{<}_s{0}_s,\left\{0_s\right\},\varnothing \right)$$
10		0lt1s	$$⊢0_s{<}_s{1}_s$$
11		0no	$$⊢0_s\in \mathrm{No}$$
12		1no	$$⊢1_s\in \mathrm{No}$$
13		ltsasym	$$⊢\left(0_s\in \mathrm{No}\wedge 1_s\in \mathrm{No}\right)\to \left(0_s{<}_s{1}_s\to \neg 1_s{<}_s{0}_s\right)$$
14	11 12 13	mp2an	$$⊢0_s{<}_s{1}_s\to \neg 1_s{<}_s{0}_s$$
15	10 14	ax-mp	$$⊢\neg 1_s{<}_s{0}_s$$
16	15	iffalsei	$$⊢if\left(1_s{<}_s{0}_s,\left\{0_s\right\},\varnothing \right)=\varnothing$$
17	1 9 16	3eqtri	$$⊢R\left(1_s\right)=\varnothing$$