Metamath Proof Explorer

Theorem nosepeq

Description: The values of two surreals at a point less than their separators are equal. (Contributed by Scott Fenton, 6-Dec-2021)

Ref Expression
Assertion nosepeq 
|- ( ( ( A e. No /\ B e. No /\ A =/= B ) /\ X e. |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) -> ( A ` X ) = ( B ` X ) )

Proof

Step Hyp Ref Expression
1 nosepon 
 |-  ( ( A e. No /\ B e. No /\ A =/= B ) -> |^| { x e. On | ( A ` x ) =/= ( B ` x ) } e. On )
2 onelon 
 |-  ( ( |^| { x e. On | ( A ` x ) =/= ( B ` x ) } e. On /\ X e. |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) -> X e. On )
3 1 2 sylan 
 |-  ( ( ( A e. No /\ B e. No /\ A =/= B ) /\ X e. |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) -> X e. On )
4 simpr 
 |-  ( ( ( A e. No /\ B e. No /\ A =/= B ) /\ X e. |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) -> X e. |^| { x e. On | ( A ` x ) =/= ( B ` x ) } )
5 fveq2 
 |-  ( x = X -> ( A ` x ) = ( A ` X ) )
6 fveq2 
 |-  ( x = X -> ( B ` x ) = ( B ` X ) )
7 5 6 neeq12d 
 |-  ( x = X -> ( ( A ` x ) =/= ( B ` x ) <-> ( A ` X ) =/= ( B ` X ) ) )
8 7 onnminsb 
 |-  ( X e. On -> ( X e. |^| { x e. On | ( A ` x ) =/= ( B ` x ) } -> -. ( A ` X ) =/= ( B ` X ) ) )
9 3 4 8 sylc 
 |-  ( ( ( A e. No /\ B e. No /\ A =/= B ) /\ X e. |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) -> -. ( A ` X ) =/= ( B ` X ) )
10 df-ne 
 |-  ( ( A ` X ) =/= ( B ` X ) <-> -. ( A ` X ) = ( B ` X ) )
11 10 con2bii 
 |-  ( ( A ` X ) = ( B ` X ) <-> -. ( A ` X ) =/= ( B ` X ) )
12 9 11 sylibr 
 |-  ( ( ( A e. No /\ B e. No /\ A =/= B ) /\ X e. |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) -> ( A ` X ) = ( B ` X ) )