Metamath Proof Explorer

Theorem negsproplem7

Description: Lemma for surreal negation. Show the second half of the inductive hypothesis unconditionally. (Contributed by Scott Fenton, 3-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
Assertion negsproplem7 
|- ( 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 bdayelon 
 |-  ( bday ` A ) e. On
6 5 onordi 
 |-  Ord ( bday ` A )
7 bdayelon 
 |-  ( bday ` B ) e. On
8 7 onordi 
 |-  Ord ( bday ` B )
9 ordtri3or 
 |-  ( ( Ord ( bday ` A ) /\ Ord ( bday ` B ) ) -> ( ( bday ` A ) e. ( bday ` B ) \/ ( bday ` A ) = ( bday ` B ) \/ ( bday ` B ) e. ( bday ` A ) ) )
10 6 8 9 mp2an 
 |-  ( ( bday ` A ) e. ( bday ` B ) \/ ( bday ` A ) = ( bday ` B ) \/ ( bday ` B ) e. ( bday ` A ) )
11 1 adantr 
 |-  ( ( ph /\ ( bday ` A ) e. ( bday ` B ) ) -> 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 )
12 2 adantr 
 |-  ( ( ph /\ ( bday ` A ) e. ( bday ` B ) ) -> A e. No )
13 3 adantr 
 |-  ( ( ph /\ ( bday ` A ) e. ( bday ` B ) ) -> B e. No )
14 4 adantr 
 |-  ( ( ph /\ ( bday ` A ) e. ( bday ` B ) ) -> A
15 simpr 
 |-  ( ( ph /\ ( bday ` A ) e. ( bday ` B ) ) -> ( bday ` A ) e. ( bday ` B ) )
16 11 12 13 14 15 negsproplem4 
 |-  ( ( ph /\ ( bday ` A ) e. ( bday ` B ) ) -> ( -us ` B )
17 16 ex 
 |-  ( ph -> ( ( bday ` A ) e. ( bday ` B ) -> ( -us ` B )
18 1 adantr 
 |-  ( ( ph /\ ( bday ` A ) = ( bday ` B ) ) -> 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 )
19 2 adantr 
 |-  ( ( ph /\ ( bday ` A ) = ( bday ` B ) ) -> A e. No )
20 3 adantr 
 |-  ( ( ph /\ ( bday ` A ) = ( bday ` B ) ) -> B e. No )
21 4 adantr 
 |-  ( ( ph /\ ( bday ` A ) = ( bday ` B ) ) -> A
22 simpr 
 |-  ( ( ph /\ ( bday ` A ) = ( bday ` B ) ) -> ( bday ` A ) = ( bday ` B ) )
23 18 19 20 21 22 negsproplem6 
 |-  ( ( ph /\ ( bday ` A ) = ( bday ` B ) ) -> ( -us ` B )
24 23 ex 
 |-  ( ph -> ( ( bday ` A ) = ( bday ` B ) -> ( -us ` B )
25 1 adantr 
 |-  ( ( ph /\ ( bday ` B ) e. ( bday ` A ) ) -> 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 )
26 2 adantr 
 |-  ( ( ph /\ ( bday ` B ) e. ( bday ` A ) ) -> A e. No )
27 3 adantr 
 |-  ( ( ph /\ ( bday ` B ) e. ( bday ` A ) ) -> B e. No )
28 4 adantr 
 |-  ( ( ph /\ ( bday ` B ) e. ( bday ` A ) ) -> A
29 simpr 
 |-  ( ( ph /\ ( bday ` B ) e. ( bday ` A ) ) -> ( bday ` B ) e. ( bday ` A ) )
30 25 26 27 28 29 negsproplem5 
 |-  ( ( ph /\ ( bday ` B ) e. ( bday ` A ) ) -> ( -us ` B )
31 30 ex 
 |-  ( ph -> ( ( bday ` B ) e. ( bday ` A ) -> ( -us ` B )
32 17 24 31 3jaod 
 |-  ( ph -> ( ( ( bday ` A ) e. ( bday ` B ) \/ ( bday ` A ) = ( bday ` B ) \/ ( bday ` B ) e. ( bday ` A ) ) -> ( -us ` B )
33 10 32 mpi 
 |-  ( ph -> ( -us ` B )