Metamath Proof Explorer

Theorem left0s

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

Ref Expression
Assertion left0s 
|- ( _L ` 0s ) = (/)

Proof

Step Hyp Ref Expression
1 leftssold 
 |-  ( _L ` 0s ) C_ ( _Old ` ( bday ` 0s ) )
2 bday0s 
 |-  ( bday ` 0s ) = (/)
3 2 fveq2i 
 |-  ( _Old ` ( bday ` 0s ) ) = ( _Old ` (/) )
4 old0 
 |-  ( _Old ` (/) ) = (/)
5 3 4 eqtri 
 |-  ( _Old ` ( bday ` 0s ) ) = (/)
6 sseq0 
 |-  ( ( ( _L ` 0s ) C_ ( _Old ` ( bday ` 0s ) ) /\ ( _Old ` ( bday ` 0s ) ) = (/) ) -> ( _L ` 0s ) = (/) )
7 1 5 6 mp2an 
 |-  ( _L ` 0s ) = (/)