Theorem lestric

Description: Surreal trichotomy law. (Contributed by Scott Fenton, 14-Feb-2025)

	Ref	Expression
Assertion	lestric	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐴 ≤s 𝐵 ∨ 𝐵 ≤s 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		ltsasym	⊢ ( ( 𝐵 ∈ No ∧ 𝐴 ∈ No ) → ( 𝐵 <s 𝐴 → ¬ 𝐴 <s 𝐵 ) )
2		ltnles	⊢ ( ( 𝐵 ∈ No ∧ 𝐴 ∈ No ) → ( 𝐵 <s 𝐴 ↔ ¬ 𝐴 ≤s 𝐵 ) )
3	2	bicomd	⊢ ( ( 𝐵 ∈ No ∧ 𝐴 ∈ No ) → ( ¬ 𝐴 ≤s 𝐵 ↔ 𝐵 <s 𝐴 ) )
4		lenlts	⊢ ( ( 𝐵 ∈ No ∧ 𝐴 ∈ No ) → ( 𝐵 ≤s 𝐴 ↔ ¬ 𝐴 <s 𝐵 ) )
5	1 3 4	3imtr4d	⊢ ( ( 𝐵 ∈ No ∧ 𝐴 ∈ No ) → ( ¬ 𝐴 ≤s 𝐵 → 𝐵 ≤s 𝐴 ) )
6	5	orrd	⊢ ( ( 𝐵 ∈ No ∧ 𝐴 ∈ No ) → ( 𝐴 ≤s 𝐵 ∨ 𝐵 ≤s 𝐴 ) )
7	6	ancoms	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐴 ≤s 𝐵 ∨ 𝐵 ≤s 𝐴 ) )