Theorem left1s

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

	Ref	Expression
Assertion	left1s	|- ( _Left ` 1s ) = { 0s }

Proof

Step	Hyp	Ref	Expression
1		leftval	|- ( _Left ` 1s ) = { x e. ( _Old ` ( bday ` 1s ) ) | x
2		bday1s	|- ( bday ` 1s ) = 1o
3	2	fveq2i	|- ( _Old ` ( bday ` 1s ) ) = ( _Old ` 1o )
4		old1	|- ( _Old ` 1o ) = { 0s }
5	3 4	eqtri	|- ( _Old ` ( bday ` 1s ) ) = { 0s }
6	5	rabeqi	|- { x e. ( _Old ` ( bday ` 1s ) ) | x
7		breq1	|- ( x = 0s -> ( x 0s
8	7	rabsnif	|- { x e. { 0s } | x
9	6 8	eqtri	|- { x e. ( _Old ` ( bday ` 1s ) ) | x
10		0slt1s	|- 0s
11	10	iftruei	|- if ( 0s
12	1 9 11	3eqtri	|- ( _Left ` 1s ) = { 0s }