Theorem right1s

Description: The right set of 1s is empty . (Contributed by Scott Fenton, 4-Feb-2025)

	Ref	Expression
Assertion	right1s	|- ( _Right ` 1s ) = (/)

Proof

Step	Hyp	Ref	Expression
1		rightval	|- ( _Right ` 1s ) = { x e. ( _Old ` ( bday ` 1s ) ) | 1s
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 ) ) | 1s
7		breq2	|- ( x = 0s -> ( 1s 1s
8	7	rabsnif	|- { x e. { 0s } | 1s
9	6 8	eqtri	|- { x e. ( _Old ` ( bday ` 1s ) ) | 1s
10		0slt1s	|- 0s
11		0sno	|- 0s e. No
12		1sno	|- 1s e. No
13		sltasym	|- ( ( 0s e. No /\ 1s e. No ) -> ( 0s -. 1s
14	11 12 13	mp2an	|- ( 0s -. 1s
15	10 14	ax-mp	|- -. 1s
16	15	iffalsei	|- if ( 1s
17	1 9 16	3eqtri	|- ( _Right ` 1s ) = (/)