Description: The left set of 0s is empty. (Contributed by Scott Fenton, 20-Aug-2024)
Ref | Expression | ||
---|---|---|---|
Assertion | left0s | ⊢ ( L ‘ 0s ) = ∅ |
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 ) = ∅ |