Theorem sltsright

Description: A surreal is less than its right options. Theorem 0(i) of Conway p. 16. (Contributed by Scott Fenton, 7-Aug-2024)

	Ref	Expression
Assertion	sltsright	⊢ ( 𝐴 ∈ No → { 𝐴 } <<s ( R ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		snex	⊢ { 𝐴 } ∈ V
2	1	a1i	⊢ ( 𝐴 ∈ No → { 𝐴 } ∈ V )
3		fvexd	⊢ ( 𝐴 ∈ No → ( R ‘ 𝐴 ) ∈ V )
4		snssi	⊢ ( 𝐴 ∈ No → { 𝐴 } ⊆ No )
5		rightf	⊢ R : No ⟶ 𝒫 No
6	5	ffvelcdmi	⊢ ( 𝐴 ∈ No → ( R ‘ 𝐴 ) ∈ 𝒫 No )
7	6	elpwid	⊢ ( 𝐴 ∈ No → ( R ‘ 𝐴 ) ⊆ No )
8		velsn	⊢ ( 𝑥 ∈ { 𝐴 } ↔ 𝑥 = 𝐴 )
9		rightval	⊢ ( R ‘ 𝐴 ) = { 𝑦 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∣ 𝐴 <s 𝑦 }
10	9	a1i	⊢ ( 𝐴 ∈ No → ( R ‘ 𝐴 ) = { 𝑦 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∣ 𝐴 <s 𝑦 } )
11	10	eleq2d	⊢ ( 𝐴 ∈ No → ( 𝑦 ∈ ( R ‘ 𝐴 ) ↔ 𝑦 ∈ { 𝑦 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∣ 𝐴 <s 𝑦 } ) )
12		rabid	⊢ ( 𝑦 ∈ { 𝑦 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∣ 𝐴 <s 𝑦 } ↔ ( 𝑦 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∧ 𝐴 <s 𝑦 ) )
13	11 12	bitrdi	⊢ ( 𝐴 ∈ No → ( 𝑦 ∈ ( R ‘ 𝐴 ) ↔ ( 𝑦 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∧ 𝐴 <s 𝑦 ) ) )
14	13	simplbda	⊢ ( ( 𝐴 ∈ No ∧ 𝑦 ∈ ( R ‘ 𝐴 ) ) → 𝐴 <s 𝑦 )
15		breq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 <s 𝑦 ↔ 𝐴 <s 𝑦 ) )
16	14 15	imbitrrid	⊢ ( 𝑥 = 𝐴 → ( ( 𝐴 ∈ No ∧ 𝑦 ∈ ( R ‘ 𝐴 ) ) → 𝑥 <s 𝑦 ) )
17	16	expd	⊢ ( 𝑥 = 𝐴 → ( 𝐴 ∈ No → ( 𝑦 ∈ ( R ‘ 𝐴 ) → 𝑥 <s 𝑦 ) ) )
18	8 17	sylbi	⊢ ( 𝑥 ∈ { 𝐴 } → ( 𝐴 ∈ No → ( 𝑦 ∈ ( R ‘ 𝐴 ) → 𝑥 <s 𝑦 ) ) )
19	18	3imp21	⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ { 𝐴 } ∧ 𝑦 ∈ ( R ‘ 𝐴 ) ) → 𝑥 <s 𝑦 )
20	2 3 4 7 19	sltsd	⊢ ( 𝐴 ∈ No → { 𝐴 } <<s ( R ‘ 𝐴 ) )