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 ) ⊆ ( O ‘ ( bday ‘ 0s ) )
2 bday0s ( bday ‘ 0s ) = ∅
3 2 fveq2i ( O ‘ ( bday ‘ 0s ) ) = ( O ‘ ∅ )
4 old0 ( O ‘ ∅ ) = ∅
5 3 4 eqtri ( O ‘ ( bday ‘ 0s ) ) = ∅
6 sseq0 ( ( ( L ‘ 0s ) ⊆ ( O ‘ ( bday ‘ 0s ) ) ∧ ( O ‘ ( bday ‘ 0s ) ) = ∅ ) → ( L ‘ 0s ) = ∅ )
7 1 5 6 mp2an ( L ‘ 0s ) = ∅