Theorem lltropt

Description: The left options of a surreal are strictly less than the right options of the same surreal. (Contributed by Scott Fenton, 6-Aug-2024) (Revised by Scott Fenton, 21-Feb-2025)

	Ref	Expression
Assertion	lltropt	⊢ ( L ‘ 𝐴 ) <<s ( R ‘ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		ssltleft	⊢ ( 𝐴 ∈ No → ( L ‘ 𝐴 ) <<s { 𝐴 } )
2		ssltright	⊢ ( 𝐴 ∈ No → { 𝐴 } <<s ( R ‘ 𝐴 ) )
3		snnzg	⊢ ( 𝐴 ∈ No → { 𝐴 } ≠ ∅ )
4		sslttr	⊢ ( ( ( L ‘ 𝐴 ) <<s { 𝐴 } ∧ { 𝐴 } <<s ( R ‘ 𝐴 ) ∧ { 𝐴 } ≠ ∅ ) → ( L ‘ 𝐴 ) <<s ( R ‘ 𝐴 ) )
5	1 2 3 4	syl3anc	⊢ ( 𝐴 ∈ No → ( L ‘ 𝐴 ) <<s ( R ‘ 𝐴 ) )
6		0elpw	⊢ ∅ ∈ 𝒫 No
7		nulssgt	⊢ ( ∅ ∈ 𝒫 No → ∅ <<s ∅ )
8	6 7	mp1i	⊢ ( ¬ 𝐴 ∈ No → ∅ <<s ∅ )
9		leftf	⊢ L : No ⟶ 𝒫 No
10	9	fdmi	⊢ dom L = No
11	10	eleq2i	⊢ ( 𝐴 ∈ dom L ↔ 𝐴 ∈ No )
12		ndmfv	⊢ ( ¬ 𝐴 ∈ dom L → ( L ‘ 𝐴 ) = ∅ )
13	11 12	sylnbir	⊢ ( ¬ 𝐴 ∈ No → ( L ‘ 𝐴 ) = ∅ )
14		rightf	⊢ R : No ⟶ 𝒫 No
15	14	fdmi	⊢ dom R = No
16	15	eleq2i	⊢ ( 𝐴 ∈ dom R ↔ 𝐴 ∈ No )
17		ndmfv	⊢ ( ¬ 𝐴 ∈ dom R → ( R ‘ 𝐴 ) = ∅ )
18	16 17	sylnbir	⊢ ( ¬ 𝐴 ∈ No → ( R ‘ 𝐴 ) = ∅ )
19	8 13 18	3brtr4d	⊢ ( ¬ 𝐴 ∈ No → ( L ‘ 𝐴 ) <<s ( R ‘ 𝐴 ) )
20	5 19	pm2.61i	⊢ ( L ‘ 𝐴 ) <<s ( R ‘ 𝐴 )