Theorem sletri3

Description: Trichotomy law for surreal less-than or equal. (Contributed by Scott Fenton, 8-Dec-2021)

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

Proof

Step	Hyp	Ref	Expression
1		slttrieq2	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐴 = 𝐵 ↔ ( ¬ 𝐴 <s 𝐵 ∧ ¬ 𝐵 <s 𝐴 ) ) )
2		slenlt	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐴 ≤s 𝐵 ↔ ¬ 𝐵 <s 𝐴 ) )
3		slenlt	⊢ ( ( 𝐵 ∈ No ∧ 𝐴 ∈ No ) → ( 𝐵 ≤s 𝐴 ↔ ¬ 𝐴 <s 𝐵 ) )
4	3	ancoms	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐵 ≤s 𝐴 ↔ ¬ 𝐴 <s 𝐵 ) )
5	2 4	anbi12d	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( ( 𝐴 ≤s 𝐵 ∧ 𝐵 ≤s 𝐴 ) ↔ ( ¬ 𝐵 <s 𝐴 ∧ ¬ 𝐴 <s 𝐵 ) ) )
6		ancom	⊢ ( ( ¬ 𝐵 <s 𝐴 ∧ ¬ 𝐴 <s 𝐵 ) ↔ ( ¬ 𝐴 <s 𝐵 ∧ ¬ 𝐵 <s 𝐴 ) )
7	5 6	bitrdi	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( ( 𝐴 ≤s 𝐵 ∧ 𝐵 ≤s 𝐴 ) ↔ ( ¬ 𝐴 <s 𝐵 ∧ ¬ 𝐵 <s 𝐴 ) ) )
8	1 7	bitr4d	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐴 = 𝐵 ↔ ( 𝐴 ≤s 𝐵 ∧ 𝐵 ≤s 𝐴 ) ) )