Theorem left1s

Description: The left set of 1s is the singleton of 0s . (Contributed by Scott Fenton, 4-Feb-2025)

	Ref	Expression
Assertion	left1s	$$⊢L\left(1_s\right)=\left\{0_s\right\}$$

Proof

Step	Hyp	Ref	Expression
1		leftval	$$⊢L\left(1_s\right)=\left\{x\in \mathrm{Old}\left(\mathrm{bday}\left(1_s\right)\right)|x{<}_s{1}_s\right\}$$
2		bday1s	$$⊢\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)|x{<}_s{1}_s\right\}=\left\{x\in \left\{0_s\right\}|x{<}_s{1}_s\right\}$$
7		breq1	$$⊢x=0_s\to \left(x{<}_s{1}_s\leftrightarrow 0_s{<}_s{1}_s\right)$$
8	7	rabsnif	$$⊢\left\{x\in \left\{0_s\right\}|x{<}_s{1}_s\right\}=if\left(0_s{<}_s{1}_s,\left\{0_s\right\},\varnothing \right)$$
9	6 8	eqtri	$$⊢\left\{x\in \mathrm{Old}\left(\mathrm{bday}\left(1_s\right)\right)|x{<}_s{1}_s\right\}=if\left(0_s{<}_s{1}_s,\left\{0_s\right\},\varnothing \right)$$
10		0slt1s	$$⊢0_s{<}_s{1}_s$$
11	10	iftruei	$$⊢if\left(0_s{<}_s{1}_s,\left\{0_s\right\},\varnothing \right)=\left\{0_s\right\}$$
12	1 9 11	3eqtri	$$⊢L\left(1_s\right)=\left\{0_s\right\}$$