Theorem left0s

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

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

Proof

Step	Hyp	Ref	Expression
1		leftssold	Could not format ( _L ` 0s ) C_ ( _Old ` ( bday ` 0s ) ) : No typesetting found for |- ( _L ` 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	$$⊢\mathrm{Old}\left(\varnothing \right)=\varnothing$$
5	3 4	eqtri	Could not format ( _Old ` ( bday ` 0s ) ) = (/) : No typesetting found for |- ( _Old ` ( bday ` 0s ) ) = (/) with typecode |-
6		sseq0	Could not format ( ( ( _L ` 0s ) C_ ( _Old ` ( bday ` 0s ) ) /\ ( _Old ` ( bday ` 0s ) ) = (/) ) -> ( _L ` 0s ) = (/) ) : No typesetting found for |- ( ( ( _L ` 0s ) C_ ( _Old ` ( bday ` 0s ) ) /\ ( _Old ` ( bday ` 0s ) ) = (/) ) -> ( _L ` 0s ) = (/) ) with typecode |-
7	1 5 6	mp2an	Could not format ( _L ` 0s ) = (/) : No typesetting found for |- ( _L ` 0s ) = (/) with typecode |-