Metamath Proof Explorer

Theorem nosepne

Description: The value of two non-equal surreals at the first place they differ is different. (Contributed by Scott Fenton, 24-Nov-2021)

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

Proof

Step Hyp Ref Expression
1 sltso 
 |-
2 sotrine 
 |-  ( (  ( A =/= B <-> ( A
3 1 2 mpan 
 |-  ( ( A e. No /\ B e. No ) -> ( A =/= B <-> ( A
4 nosepnelem 
 |-  ( ( A e. No /\ B e. No /\ A  ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) =/= ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) )
5 4 3expia 
 |-  ( ( A e. No /\ B e. No ) -> ( A  ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) =/= ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) ) )
6 nosepnelem 
 |-  ( ( B e. No /\ A e. No /\ B  ( B ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) =/= ( A ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) )
7 necom 
 |-  ( ( A ` x ) =/= ( B ` x ) <-> ( B ` x ) =/= ( A ` x ) )
8 7 rabbii 
 |-  { x e. On | ( A ` x ) =/= ( B ` x ) } = { x e. On | ( B ` x ) =/= ( A ` x ) }
9 8 inteqi 
 |-  |^| { x e. On | ( A ` x ) =/= ( B ` x ) } = |^| { x e. On | ( B ` x ) =/= ( A ` x ) }
10 9 fveq2i 
 |-  ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = ( A ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } )
11 9 fveq2i 
 |-  ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = ( B ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } )
12 10 11 neeq12i 
 |-  ( ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) =/= ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) <-> ( A ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) =/= ( B ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) )
13 necom 
 |-  ( ( A ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) =/= ( B ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) <-> ( B ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) =/= ( A ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) )
14 12 13 bitri 
 |-  ( ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) =/= ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) <-> ( B ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) =/= ( A ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) )
15 6 14 sylibr 
 |-  ( ( B e. No /\ A e. No /\ B  ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) =/= ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) )
16 15 3expia 
 |-  ( ( B e. No /\ A e. No ) -> ( B  ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) =/= ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) ) )
17 16 ancoms 
 |-  ( ( A e. No /\ B e. No ) -> ( B  ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) =/= ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) ) )
18 5 17 jaod 
 |-  ( ( A e. No /\ B e. No ) -> ( ( A  ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) =/= ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) ) )
19 3 18 sylbid 
 |-  ( ( A e. No /\ B e. No ) -> ( A =/= B -> ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) =/= ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) ) )
20 19 3impia 
 |-  ( ( A e. No /\ B e. No /\ A =/= B ) -> ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) =/= ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) )