Metamath Proof Explorer

Theorem sltne

Description: Surreal less-than implies not equal. (Contributed by Scott Fenton, 12-Mar-2025)

Ref Expression
Assertion sltne 
|- ( ( A e. No /\ A  B =/= A )

Proof

Step Hyp Ref Expression
1 sltirr 
 |-  ( A e. No -> -. A
2 breq2 
 |-  ( B = A -> ( A  A
3 2 notbid 
 |-  ( B = A -> ( -. A  -. A
4 1 3 syl5ibrcom 
 |-  ( A e. No -> ( B = A -> -. A
5 4 necon2ad 
 |-  ( A e. No -> ( A  B =/= A ) )
6 5 imp 
 |-  ( ( A e. No /\ A  B =/= A )