Theorem left1s

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

	Ref	Expression
Assertion	left1s	Could not format assertion : No typesetting found for |- ( _Left ` 1s ) = { 0s } with typecode |-

Proof

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