Theorem right1s

Description: The right set of 1s is empty . (Contributed by Scott Fenton, 4-Feb-2025)

	Ref	Expression
Assertion	right1s	⊢ ( R ‘ 1s ) = ∅

Proof

Step	Hyp	Ref	Expression
1		rightval	⊢ ( R ‘ 1s ) = { 𝑥 ∈ ( O ‘ ( bday ‘ 1s ) ) ∣ 1s <s 𝑥 }
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 ) ) ∣ 1s <s 𝑥 } = { 𝑥 ∈ { 0s } ∣ 1s <s 𝑥 }
7		breq2	⊢ ( 𝑥 = 0s → ( 1s <s 𝑥 ↔ 1s <s 0s ) )
8	7	rabsnif	⊢ { 𝑥 ∈ { 0s } ∣ 1s <s 𝑥 } = if ( 1s <s 0s , { 0s } , ∅ )
9	6 8	eqtri	⊢ { 𝑥 ∈ ( O ‘ ( bday ‘ 1s ) ) ∣ 1s <s 𝑥 } = if ( 1s <s 0s , { 0s } , ∅ )
10		0slt1s	⊢ 0s <s 1s
11		0sno	⊢ 0s ∈ No
12		1sno	⊢ 1s ∈ No
13		sltasym	⊢ ( ( 0s ∈ No ∧ 1s ∈ No ) → ( 0s <s 1s → ¬ 1s <s 0s ) )
14	11 12 13	mp2an	⊢ ( 0s <s 1s → ¬ 1s <s 0s )
15	10 14	ax-mp	⊢ ¬ 1s <s 0s
16	15	iffalsei	⊢ if ( 1s <s 0s , { 0s } , ∅ ) = ∅
17	1 9 16	3eqtri	⊢ ( R ‘ 1s ) = ∅