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	No typesetting found for |- ( ph -> 0s
Assertion	0elleft	Could not format assertion : No typesetting found for |- ( ph -> 0s e. ( _Left ` A ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		0elleft.1	$$⊢\phi \to A\in \mathrm{No}$$
2		0elleft.2	Could not format ( ph -> 0s 0s
3	2	sgt0ne0d	Could not format ( ph -> A =/= 0s ) : No typesetting found for |- ( ph -> A =/= 0s ) with typecode |-
4	1 3	0elold	Could not format ( ph -> 0s e. ( _Old ` ( bday ` A ) ) ) : No typesetting found for |- ( ph -> 0s e. ( _Old ` ( bday ` A ) ) ) with typecode |-
5		breq1	Could not format ( x = 0s -> ( x 0s ( x 0s
6		leftval	Could not format ( _Left ` A ) = { x e. ( _Old ` ( bday ` A ) ) | x
7	5 6	elrab2	Could not format ( 0s e. ( _Left ` A ) <-> ( 0s e. ( _Old ` ( bday ` A ) ) /\ 0s ( 0s e. ( _Old ` ( bday ` A ) ) /\ 0s
8	4 2 7	sylanbrc	Could not format ( ph -> 0s e. ( _Left ` A ) ) : No typesetting found for |- ( ph -> 0s e. ( _Left ` A ) ) with typecode |-