Metamath Proof Explorer

Theorem right0s

Description: The right set of 0s is empty. (Contributed by Scott Fenton, 20-Aug-2024)

Ref Expression
Assertion right0s 
|- ( _R ` 0s ) = (/)

Proof

Step Hyp Ref Expression
1 0sno 
 |-  0s e. No
2 rightssold 
 |-  ( 0s e. No -> ( _R ` 0s ) C_ ( _Old ` ( bday ` 0s ) ) )
3 1 2 ax-mp 
 |-  ( _R ` 0s ) C_ ( _Old ` ( bday ` 0s ) )
4 bday0s 
 |-  ( bday ` 0s ) = (/)
5 4 fveq2i 
 |-  ( _Old ` ( bday ` 0s ) ) = ( _Old ` (/) )
6 old0 
 |-  ( _Old ` (/) ) = (/)
7 5 6 eqtri 
 |-  ( _Old ` ( bday ` 0s ) ) = (/)
8 sseq0 
 |-  ( ( ( _R ` 0s ) C_ ( _Old ` ( bday ` 0s ) ) /\ ( _Old ` ( bday ` 0s ) ) = (/) ) -> ( _R ` 0s ) = (/) )
9 3 7 8 mp2an 
 |-  ( _R ` 0s ) = (/)