Metamath Proof Explorer

Theorem nosepdm

Description: The first place two surreals differ is an element of the larger of their domains. (Contributed by Scott Fenton, 24-Nov-2021)

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

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 nosepdmlem 
 |-  ( ( A e. No /\ B e. No /\ A  |^| { x e. On | ( A ` x ) =/= ( B ` x ) } e. ( dom A u. dom B ) )
5 4 3expa 
 |-  ( ( ( A e. No /\ B e. No ) /\ A  |^| { x e. On | ( A ` x ) =/= ( B ` x ) } e. ( dom A u. dom B ) )
6 simplr 
 |-  ( ( ( A e. No /\ B e. No ) /\ B  B e. No )
7 simpll 
 |-  ( ( ( A e. No /\ B e. No ) /\ B  A e. No )
8 simpr 
 |-  ( ( ( A e. No /\ B e. No ) /\ B  B
9 nosepdmlem 
 |-  ( ( B e. No /\ A e. No /\ B  |^| { x e. On | ( B ` x ) =/= ( A ` x ) } e. ( dom B u. dom A ) )
10 6 7 8 9 syl3anc 
 |-  ( ( ( A e. No /\ B e. No ) /\ B  |^| { x e. On | ( B ` x ) =/= ( A ` x ) } e. ( dom B u. dom A ) )
11 necom 
 |-  ( ( A ` x ) =/= ( B ` x ) <-> ( B ` x ) =/= ( A ` x ) )
12 11 rabbii 
 |-  { x e. On | ( A ` x ) =/= ( B ` x ) } = { x e. On | ( B ` x ) =/= ( A ` x ) }
13 12 inteqi 
 |-  |^| { x e. On | ( A ` x ) =/= ( B ` x ) } = |^| { x e. On | ( B ` x ) =/= ( A ` x ) }
14 uncom 
 |-  ( dom A u. dom B ) = ( dom B u. dom A )
15 10 13 14 3eltr4g 
 |-  ( ( ( A e. No /\ B e. No ) /\ B  |^| { x e. On | ( A ` x ) =/= ( B ` x ) } e. ( dom A u. dom B ) )
16 5 15 jaodan 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( A  |^| { x e. On | ( A ` x ) =/= ( B ` x ) } e. ( dom A u. dom B ) )
17 16 ex 
 |-  ( ( A e. No /\ B e. No ) -> ( ( A  |^| { x e. On | ( A ` x ) =/= ( B ` x ) } e. ( dom A u. dom B ) ) )
18 3 17 sylbid 
 |-  ( ( A e. No /\ B e. No ) -> ( A =/= B -> |^| { x e. On | ( A ` x ) =/= ( B ` x ) } e. ( dom A u. dom B ) ) )
19 18 3impia 
 |-  ( ( A e. No /\ B e. No /\ A =/= B ) -> |^| { x e. On | ( A ` x ) =/= ( B ` x ) } e. ( dom A u. dom B ) )