Theorem slenlt

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

	Ref	Expression
Assertion	slenlt	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐴 ≤s 𝐵 ↔ ¬ 𝐵 <s 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		df-sle	⊢ ≤s = ( ( No × No ) ∖ ◡ <s )
2	1	breqi	⊢ ( 𝐴 ≤s 𝐵 ↔ 𝐴 ( ( No × No ) ∖ ◡ <s ) 𝐵 )
3		brdif	⊢ ( 𝐴 ( ( No × No ) ∖ ◡ <s ) 𝐵 ↔ ( 𝐴 ( No × No ) 𝐵 ∧ ¬ 𝐴 ◡ <s 𝐵 ) )
4		brxp	⊢ ( 𝐴 ( No × No ) 𝐵 ↔ ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) )
5	4	anbi1i	⊢ ( ( 𝐴 ( No × No ) 𝐵 ∧ ¬ 𝐴 ◡ <s 𝐵 ) ↔ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ¬ 𝐴 ◡ <s 𝐵 ) )
6	2 3 5	3bitri	⊢ ( 𝐴 ≤s 𝐵 ↔ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ¬ 𝐴 ◡ <s 𝐵 ) )
7		ibar	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( ¬ 𝐴 ◡ <s 𝐵 ↔ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ¬ 𝐴 ◡ <s 𝐵 ) ) )
8		brcnvg	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐴 ◡ <s 𝐵 ↔ 𝐵 <s 𝐴 ) )
9	8	notbid	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( ¬ 𝐴 ◡ <s 𝐵 ↔ ¬ 𝐵 <s 𝐴 ) )
10	7 9	bitr3d	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ¬ 𝐴 ◡ <s 𝐵 ) ↔ ¬ 𝐵 <s 𝐴 ) )
11	6 10	syl5bb	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐴 ≤s 𝐵 ↔ ¬ 𝐵 <s 𝐴 ) )