Metamath Proof Explorer


Theorem right0s

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

Ref Expression
Assertion right0s Could not format assertion : No typesetting found for |- ( _R ` 0s ) = (/) with typecode |-

Proof

Step Hyp Ref Expression
1 rightssold Could not format ( _R ` 0s ) C_ ( _Old ` ( bday ` 0s ) ) : No typesetting found for |- ( _R ` 0s ) C_ ( _Old ` ( bday ` 0s ) ) with typecode |-
2 bday0s Could not format ( bday ` 0s ) = (/) : No typesetting found for |- ( bday ` 0s ) = (/) with typecode |-
3 2 fveq2i Could not format ( _Old ` ( bday ` 0s ) ) = ( _Old ` (/) ) : No typesetting found for |- ( _Old ` ( bday ` 0s ) ) = ( _Old ` (/) ) with typecode |-
4 old0 Old =
5 3 4 eqtri Could not format ( _Old ` ( bday ` 0s ) ) = (/) : No typesetting found for |- ( _Old ` ( bday ` 0s ) ) = (/) with typecode |-
6 sseq0 Could not format ( ( ( _R ` 0s ) C_ ( _Old ` ( bday ` 0s ) ) /\ ( _Old ` ( bday ` 0s ) ) = (/) ) -> ( _R ` 0s ) = (/) ) : No typesetting found for |- ( ( ( _R ` 0s ) C_ ( _Old ` ( bday ` 0s ) ) /\ ( _Old ` ( bday ` 0s ) ) = (/) ) -> ( _R ` 0s ) = (/) ) with typecode |-
7 1 5 6 mp2an Could not format ( _R ` 0s ) = (/) : No typesetting found for |- ( _R ` 0s ) = (/) with typecode |-