Theorem ssltright

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	ssltright	⊢ ( 𝐴 ∈ No → { 𝐴 } <<s ( R ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		snssi	⊢ ( 𝐴 ∈ No → { 𝐴 } ⊆ No )
2		rightf	⊢ R : No ⟶ 𝒫 No
3	2	ffvelrni	⊢ ( 𝐴 ∈ No → ( R ‘ 𝐴 ) ∈ 𝒫 No )
4	3	elpwid	⊢ ( 𝐴 ∈ No → ( R ‘ 𝐴 ) ⊆ No )
5		rightval	⊢ ( 𝐴 ∈ No → ( R ‘ 𝐴 ) = { 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∣ 𝐴 <s 𝑥 } )
6	5	eleq2d	⊢ ( 𝐴 ∈ No → ( 𝑦 ∈ ( R ‘ 𝐴 ) ↔ 𝑦 ∈ { 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∣ 𝐴 <s 𝑥 } ) )
7		breq2	⊢ ( 𝑥 = 𝑦 → ( 𝐴 <s 𝑥 ↔ 𝐴 <s 𝑦 ) )
8	7	elrab	⊢ ( 𝑦 ∈ { 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∣ 𝐴 <s 𝑥 } ↔ ( 𝑦 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∧ 𝐴 <s 𝑦 ) )
9	8	simprbi	⊢ ( 𝑦 ∈ { 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∣ 𝐴 <s 𝑥 } → 𝐴 <s 𝑦 )
10	6 9	syl6bi	⊢ ( 𝐴 ∈ No → ( 𝑦 ∈ ( R ‘ 𝐴 ) → 𝐴 <s 𝑦 ) )
11	10	ralrimiv	⊢ ( 𝐴 ∈ No → ∀ 𝑦 ∈ ( R ‘ 𝐴 ) 𝐴 <s 𝑦 )
12		breq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 <s 𝑦 ↔ 𝐴 <s 𝑦 ) )
13	12	ralbidv	⊢ ( 𝑥 = 𝐴 → ( ∀ 𝑦 ∈ ( R ‘ 𝐴 ) 𝑥 <s 𝑦 ↔ ∀ 𝑦 ∈ ( R ‘ 𝐴 ) 𝐴 <s 𝑦 ) )
14	13	ralsng	⊢ ( 𝐴 ∈ No → ( ∀ 𝑥 ∈ { 𝐴 } ∀ 𝑦 ∈ ( R ‘ 𝐴 ) 𝑥 <s 𝑦 ↔ ∀ 𝑦 ∈ ( R ‘ 𝐴 ) 𝐴 <s 𝑦 ) )
15	11 14	mpbird	⊢ ( 𝐴 ∈ No → ∀ 𝑥 ∈ { 𝐴 } ∀ 𝑦 ∈ ( R ‘ 𝐴 ) 𝑥 <s 𝑦 )
16		snex	⊢ { 𝐴 } ∈ V
17		fvex	⊢ ( R ‘ 𝐴 ) ∈ V
18	16 17	pm3.2i	⊢ ( { 𝐴 } ∈ V ∧ ( R ‘ 𝐴 ) ∈ V )
19		brsslt	⊢ ( { 𝐴 } <<s ( R ‘ 𝐴 ) ↔ ( ( { 𝐴 } ∈ V ∧ ( R ‘ 𝐴 ) ∈ V ) ∧ ( { 𝐴 } ⊆ No ∧ ( R ‘ 𝐴 ) ⊆ No ∧ ∀ 𝑥 ∈ { 𝐴 } ∀ 𝑦 ∈ ( R ‘ 𝐴 ) 𝑥 <s 𝑦 ) ) )
20	18 19	mpbiran	⊢ ( { 𝐴 } <<s ( R ‘ 𝐴 ) ↔ ( { 𝐴 } ⊆ No ∧ ( R ‘ 𝐴 ) ⊆ No ∧ ∀ 𝑥 ∈ { 𝐴 } ∀ 𝑦 ∈ ( R ‘ 𝐴 ) 𝑥 <s 𝑦 ) )
21	1 4 15 20	syl3anbrc	⊢ ( 𝐴 ∈ No → { 𝐴 } <<s ( R ‘ 𝐴 ) )