Theorem lesloe

Description: Surreal less-than or equal in terms of less-than. (Contributed by Scott Fenton, 8-Dec-2021)

	Ref	Expression
Assertion	lesloe	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐴 ≤s 𝐵 ↔ ( 𝐴 <s 𝐵 ∨ 𝐴 = 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		lenlts	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐴 ≤s 𝐵 ↔ ¬ 𝐵 <s 𝐴 ) )
2		orcom	⊢ ( ( 𝐴 <s 𝐵 ∨ 𝐴 = 𝐵 ) ↔ ( 𝐴 = 𝐵 ∨ 𝐴 <s 𝐵 ) )
3		eqcom	⊢ ( 𝐴 = 𝐵 ↔ 𝐵 = 𝐴 )
4	3	orbi1i	⊢ ( ( 𝐴 = 𝐵 ∨ 𝐴 <s 𝐵 ) ↔ ( 𝐵 = 𝐴 ∨ 𝐴 <s 𝐵 ) )
5	2 4	bitri	⊢ ( ( 𝐴 <s 𝐵 ∨ 𝐴 = 𝐵 ) ↔ ( 𝐵 = 𝐴 ∨ 𝐴 <s 𝐵 ) )
6		ltsso	⊢ <s Or No
7		sotric	⊢ ( ( <s Or No ∧ ( 𝐵 ∈ No ∧ 𝐴 ∈ No ) ) → ( 𝐵 <s 𝐴 ↔ ¬ ( 𝐵 = 𝐴 ∨ 𝐴 <s 𝐵 ) ) )
8	6 7	mpan	⊢ ( ( 𝐵 ∈ No ∧ 𝐴 ∈ No ) → ( 𝐵 <s 𝐴 ↔ ¬ ( 𝐵 = 𝐴 ∨ 𝐴 <s 𝐵 ) ) )
9	8	ancoms	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐵 <s 𝐴 ↔ ¬ ( 𝐵 = 𝐴 ∨ 𝐴 <s 𝐵 ) ) )
10	9	con2bid	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( ( 𝐵 = 𝐴 ∨ 𝐴 <s 𝐵 ) ↔ ¬ 𝐵 <s 𝐴 ) )
11	5 10	bitrid	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( ( 𝐴 <s 𝐵 ∨ 𝐴 = 𝐵 ) ↔ ¬ 𝐵 <s 𝐴 ) )
12	1 11	bitr4d	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐴 ≤s 𝐵 ↔ ( 𝐴 <s 𝐵 ∨ 𝐴 = 𝐵 ) ) )