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		0sno	Could not format 0s e. No : No typesetting found for |- 0s e. No with typecode |-
2		leftssold	Could not format ( 0s e. No -> ( _L ` 0s ) C_ ( _Old ` ( bday ` 0s ) ) ) : No typesetting found for |- ( 0s e. No -> ( _L ` 0s ) C_ ( _Old ` ( bday ` 0s ) ) ) with typecode |-
3	1 2	ax-mp	Could not format ( _L ` 0s ) C_ ( _Old ` ( bday ` 0s ) ) : No typesetting found for |- ( _L ` 0s ) C_ ( _Old ` ( bday ` 0s ) ) with typecode |-
4		bday0s	Could not format ( bday ` 0s ) = (/) : No typesetting found for |- ( bday ` 0s ) = (/) with typecode |-
5	4	fveq2i	Could not format ( _Old ` ( bday ` 0s ) ) = ( _Old ` (/) ) : No typesetting found for |- ( _Old ` ( bday ` 0s ) ) = ( _Old ` (/) ) with typecode |-
6		old0	$$⊢\mathrm{Old}\left(\varnothing \right)=\varnothing$$
7	5 6	eqtri	Could not format ( _Old ` ( bday ` 0s ) ) = (/) : No typesetting found for |- ( _Old ` ( bday ` 0s ) ) = (/) with typecode |-
8		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 |-
9	3 7 8	mp2an	Could not format ( _L ` 0s ) = (/) : No typesetting found for |- ( _L ` 0s ) = (/) with typecode |-