Theorem left1s

Description: The left set of 1s is the singleton of 0s . (Contributed by Scott Fenton, 4-Feb-2025)

	Ref	Expression
Assertion	left1s	⊢ ( L ‘ 1s ) = { 0s }

Proof

Step	Hyp	Ref	Expression
1		leftval	⊢ ( L ‘ 1s ) = { 𝑥 ∈ ( O ‘ ( bday ‘ 1s ) ) ∣ 𝑥 <s 1s }
2		bday1s	⊢ ( bday ‘ 1s ) = 1o
3	2	fveq2i	⊢ ( O ‘ ( bday ‘ 1s ) ) = ( O ‘ 1o )
4		old1	⊢ ( O ‘ 1o ) = { 0s }
5	3 4	eqtri	⊢ ( O ‘ ( bday ‘ 1s ) ) = { 0s }
6	5	rabeqi	⊢ { 𝑥 ∈ ( O ‘ ( bday ‘ 1s ) ) ∣ 𝑥 <s 1s } = { 𝑥 ∈ { 0s } ∣ 𝑥 <s 1s }
7		breq1	⊢ ( 𝑥 = 0s → ( 𝑥 <s 1s ↔ 0s <s 1s ) )
8	7	rabsnif	⊢ { 𝑥 ∈ { 0s } ∣ 𝑥 <s 1s } = if ( 0s <s 1s , { 0s } , ∅ )
9	6 8	eqtri	⊢ { 𝑥 ∈ ( O ‘ ( bday ‘ 1s ) ) ∣ 𝑥 <s 1s } = if ( 0s <s 1s , { 0s } , ∅ )
10		0slt1s	⊢ 0s <s 1s
11	10	iftruei	⊢ if ( 0s <s 1s , { 0s } , ∅ ) = { 0s }
12	1 9 11	3eqtri	⊢ ( L ‘ 1s ) = { 0s }