Metamath Proof Explorer

Theorem nodenselem5

Description: Lemma for nodense . If the birthdays of two distinct surreals are equal, then the ordinal from nodenselem4 is an element of that birthday. (Contributed by Scott Fenton, 16-Jun-2011)

Ref Expression
Assertion nodenselem5 
|- ( ( ( A e. No /\ B e. No ) /\ ( ( bday ` A ) = ( bday ` B ) /\ A  |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. ( bday ` A ) )

Proof

Step Hyp Ref Expression
1 simpll 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( ( bday ` A ) = ( bday ` B ) /\ A  A e. No )
2 simplr 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( ( bday ` A ) = ( bday ` B ) /\ A  B e. No )
3 sltso 
 |-
4 sonr 
 |-  ( (  -. A
5 3 4 mpan 
 |-  ( A e. No -> -. A
6 breq2 
 |-  ( A = B -> ( A  A
7 6 notbid 
 |-  ( A = B -> ( -. A  -. A
8 5 7 syl5ibcom 
 |-  ( A e. No -> ( A = B -> -. A
9 8 necon2ad 
 |-  ( A e. No -> ( A  A =/= B ) )
10 9 adantr 
 |-  ( ( A e. No /\ B e. No ) -> ( A  A =/= B ) )
11 10 imp 
 |-  ( ( ( A e. No /\ B e. No ) /\ A  A =/= B )
12 11 adantrl 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( ( bday ` A ) = ( bday ` B ) /\ A  A =/= B )
13 nosepdm 
 |-  ( ( A e. No /\ B e. No /\ A =/= B ) -> |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. ( dom A u. dom B ) )
14 1 2 12 13 syl3anc 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( ( bday ` A ) = ( bday ` B ) /\ A  |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. ( dom A u. dom B ) )
15 simprl 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( ( bday ` A ) = ( bday ` B ) /\ A  ( bday ` A ) = ( bday ` B ) )
16 15 uneq2d 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( ( bday ` A ) = ( bday ` B ) /\ A  ( ( bday ` A ) u. ( bday ` A ) ) = ( ( bday ` A ) u. ( bday ` B ) ) )
17 unidm 
 |-  ( ( bday ` A ) u. ( bday ` A ) ) = ( bday ` A )
18 16 17 eqtr3di 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( ( bday ` A ) = ( bday ` B ) /\ A  ( ( bday ` A ) u. ( bday ` B ) ) = ( bday ` A ) )
19 bdayval 
 |-  ( A e. No -> ( bday ` A ) = dom A )
20 1 19 syl 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( ( bday ` A ) = ( bday ` B ) /\ A  ( bday ` A ) = dom A )
21 bdayval 
 |-  ( B e. No -> ( bday ` B ) = dom B )
22 2 21 syl 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( ( bday ` A ) = ( bday ` B ) /\ A  ( bday ` B ) = dom B )
23 20 22 uneq12d 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( ( bday ` A ) = ( bday ` B ) /\ A  ( ( bday ` A ) u. ( bday ` B ) ) = ( dom A u. dom B ) )
24 18 23 20 3eqtr3d 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( ( bday ` A ) = ( bday ` B ) /\ A  ( dom A u. dom B ) = dom A )
25 14 24 eleqtrd 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( ( bday ` A ) = ( bday ` B ) /\ A  |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. dom A )
26 25 20 eleqtrrd 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( ( bday ` A ) = ( bday ` B ) /\ A  |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. ( bday ` A ) )