Description: The right set of 0s is empty. (Contributed by Scott Fenton, 20-Aug-2024)
Ref | Expression | ||
---|---|---|---|
Assertion | right0s | ⊢ ( R ‘ 0s ) = ∅ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rightssold | ⊢ ( R ‘ 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 | ⊢ ( ( ( R ‘ 0s ) ⊆ ( O ‘ ( bday ‘ 0s ) ) ∧ ( O ‘ ( bday ‘ 0s ) ) = ∅ ) → ( R ‘ 0s ) = ∅ ) | |
7 | 1 5 6 | mp2an | ⊢ ( R ‘ 0s ) = ∅ |