Theorem 0elleft

Description: Zero is in the left set of any positive number. (Contributed by Scott Fenton, 13-Mar-2025)

	Ref	Expression
Hypotheses	0elleft.1	$$⊢\phi \to A\in \mathrm{No}$$
	0elleft.2	$$⊢\phi \to 0_s{<}_{s}A$$
Assertion	0elleft	$$⊢\phi \to 0_s\in L\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		0elleft.1	$$⊢\phi \to A\in \mathrm{No}$$
2		0elleft.2	$$⊢\phi \to 0_s{<}_{s}A$$
3	2	sgt0ne0d	$$⊢\phi \to A\ne 0_s$$
4	1 3	0elold	$$⊢\phi \to 0_s\in \mathrm{Old}\left(\mathrm{bday}\left(A\right)\right)$$
5		breq1	$$⊢x=0_s\to \left(x{<}_{s}A\leftrightarrow 0_s{<}_{s}A\right)$$
6		leftval	$$⊢L\left(A\right)=\left\{x\in \mathrm{Old}\left(\mathrm{bday}\left(A\right)\right)|x{<}_{s}A\right\}$$
7	5 6	elrab2	$$⊢0_s\in L\left(A\right)\leftrightarrow \left(0_s\in \mathrm{Old}\left(\mathrm{bday}\left(A\right)\right)\wedge 0_s{<}_{s}A\right)$$
8	4 2 7	sylanbrc	$$⊢\phi \to 0_s\in L\left(A\right)$$