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	|- ( ph -> A e. No )
	0elleft.2	|- ( ph -> 0s
Assertion	0elleft	|- ( ph -> 0s e. ( _Left ` A ) )

Proof

Step	Hyp	Ref	Expression
1		0elleft.1	|- ( ph -> A e. No )
2		0elleft.2	|- ( ph -> 0s
3	2	sgt0ne0d	|- ( ph -> A =/= 0s )
4	1 3	0elold	|- ( ph -> 0s e. ( _Old ` ( bday ` A ) ) )
5		breq1	|- ( x = 0s -> ( x 0s
6		leftval	|- ( _Left ` A ) = { x e. ( _Old ` ( bday ` A ) ) | x
7	5 6	elrab2	|- ( 0s e. ( _Left ` A ) <-> ( 0s e. ( _Old ` ( bday ` A ) ) /\ 0s
8	4 2 7	sylanbrc	|- ( ph -> 0s e. ( _Left ` A ) )