Metamath Proof Explorer

Theorem negsproplem4

Description: Lemma for surreal negation. Show the second half of the inductive hypothesis when A is simpler than B . (Contributed by Scott Fenton, 2-Feb-2025)

Ref Expression
Hypotheses negsproplem.1 
|- ( ph -> A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` A ) u. ( bday ` B ) ) -> ( ( -us ` x ) e. No /\ ( x  ( -us ` y )
negsproplem4.1 
|- ( ph -> A e. No )
negsproplem4.2 
|- ( ph -> B e. No )
negsproplem4.3 
|- ( ph -> A
negsproplem4.4 
|- ( ph -> ( bday ` A ) e. ( bday ` B ) )
Assertion negsproplem4 
|- ( ph -> ( -us ` B )

Proof

Step Hyp Ref Expression
1 negsproplem.1 
 |-  ( ph -> A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` A ) u. ( bday ` B ) ) -> ( ( -us ` x ) e. No /\ ( x  ( -us ` y )
2 negsproplem4.1 
 |-  ( ph -> A e. No )
3 negsproplem4.2 
 |-  ( ph -> B e. No )
4 negsproplem4.3 
 |-  ( ph -> A
5 negsproplem4.4 
 |-  ( ph -> ( bday ` A ) e. ( bday ` B ) )
6 uncom 
 |-  ( ( bday ` A ) u. ( bday ` B ) ) = ( ( bday ` B ) u. ( bday ` A ) )
7 6 eleq2i 
 |-  ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` A ) u. ( bday ` B ) ) <-> ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` B ) u. ( bday ` A ) ) )
8 7 imbi1i 
 |-  ( ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` A ) u. ( bday ` B ) ) -> ( ( -us ` x ) e. No /\ ( x  ( -us ` y )  ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` B ) u. ( bday ` A ) ) -> ( ( -us ` x ) e. No /\ ( x  ( -us ` y )
9 8 2ralbii 
 |-  ( A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` A ) u. ( bday ` B ) ) -> ( ( -us ` x ) e. No /\ ( x  ( -us ` y )  A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` B ) u. ( bday ` A ) ) -> ( ( -us ` x ) e. No /\ ( x  ( -us ` y )
10 1 9 sylib 
 |-  ( ph -> A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` B ) u. ( bday ` A ) ) -> ( ( -us ` x ) e. No /\ ( x  ( -us ` y )
11 10 3 negsproplem3 
 |-  ( ph -> ( ( -us ` B ) e. No /\ ( -us " ( _Right ` B ) ) <
12 11 simp3d 
 |-  ( ph -> { ( -us ` B ) } <
13 fvex 
 |-  ( -us ` B ) e. _V
14 13 snid 
 |-  ( -us ` B ) e. { ( -us ` B ) }
15 14 a1i 
 |-  ( ph -> ( -us ` B ) e. { ( -us ` B ) } )
16 negsfn 
 |-  -us Fn No
17 leftssno 
 |-  ( _Left ` B ) C_ No
18 bdayelon 
 |-  ( bday ` B ) e. On
19 oldbday 
 |-  ( ( ( bday ` B ) e. On /\ A e. No ) -> ( A e. ( _Old ` ( bday ` B ) ) <-> ( bday ` A ) e. ( bday ` B ) ) )
20 18 2 19 sylancr 
 |-  ( ph -> ( A e. ( _Old ` ( bday ` B ) ) <-> ( bday ` A ) e. ( bday ` B ) ) )
21 5 20 mpbird 
 |-  ( ph -> A e. ( _Old ` ( bday ` B ) ) )
22 breq1 
 |-  ( a = A -> ( a  A
23 leftval 
 |-  ( _Left ` B ) = { a e. ( _Old ` ( bday ` B ) ) | a
24 22 23 elrab2 
 |-  ( A e. ( _Left ` B ) <-> ( A e. ( _Old ` ( bday ` B ) ) /\ A
25 21 4 24 sylanbrc 
 |-  ( ph -> A e. ( _Left ` B ) )
26 fnfvima 
 |-  ( ( -us Fn No /\ ( _Left ` B ) C_ No /\ A e. ( _Left ` B ) ) -> ( -us ` A ) e. ( -us " ( _Left ` B ) ) )
27 16 17 25 26 mp3an12i 
 |-  ( ph -> ( -us ` A ) e. ( -us " ( _Left ` B ) ) )
28 12 15 27 ssltsepcd 
 |-  ( ph -> ( -us ` B )