Metamath Proof Explorer

Theorem addsproplem7

Description: Lemma for surreal addition properties. Putting together the three previous lemmas, we now show the second half of the inductive hypothesis unconditionally. (Contributed by Scott Fenton, 21-Jan-2025)

Ref Expression
Hypotheses addsproplem.1 
|- ( ph -> A. x e. No A. y e. No A. z e. No ( ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) -> ( ( x +s y ) e. No /\ ( y  ( y +s x )
addspropord.2 
|- ( ph -> X e. No )
addspropord.3 
|- ( ph -> Y e. No )
addspropord.4 
|- ( ph -> Z e. No )
addspropord.5 
|- ( ph -> Y
Assertion addsproplem7 
|- ( ph -> ( Y +s X )

Proof

Step Hyp Ref Expression
1 addsproplem.1 
 |-  ( ph -> A. x e. No A. y e. No A. z e. No ( ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) -> ( ( x +s y ) e. No /\ ( y  ( y +s x )
2 addspropord.2 
 |-  ( ph -> X e. No )
3 addspropord.3 
 |-  ( ph -> Y e. No )
4 addspropord.4 
 |-  ( ph -> Z e. No )
5 addspropord.5 
 |-  ( ph -> Y
6 bdayelon 
 |-  ( bday ` Y ) e. On
7 fvex 
 |-  ( bday ` Y ) e. _V
8 7 elon 
 |-  ( ( bday ` Y ) e. On <-> Ord ( bday ` Y ) )
9 6 8 mpbi 
 |-  Ord ( bday ` Y )
10 bdayelon 
 |-  ( bday ` Z ) e. On
11 fvex 
 |-  ( bday ` Z ) e. _V
12 11 elon 
 |-  ( ( bday ` Z ) e. On <-> Ord ( bday ` Z ) )
13 10 12 mpbi 
 |-  Ord ( bday ` Z )
14 ordtri3or 
 |-  ( ( Ord ( bday ` Y ) /\ Ord ( bday ` Z ) ) -> ( ( bday ` Y ) e. ( bday ` Z ) \/ ( bday ` Y ) = ( bday ` Z ) \/ ( bday ` Z ) e. ( bday ` Y ) ) )
15 9 13 14 mp2an 
 |-  ( ( bday ` Y ) e. ( bday ` Z ) \/ ( bday ` Y ) = ( bday ` Z ) \/ ( bday ` Z ) e. ( bday ` Y ) )
16 simpl 
 |-  ( ( ph /\ ( bday ` Y ) e. ( bday ` Z ) ) -> ph )
17 16 1 syl 
 |-  ( ( ph /\ ( bday ` Y ) e. ( bday ` Z ) ) -> A. x e. No A. y e. No A. z e. No ( ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) -> ( ( x +s y ) e. No /\ ( y  ( y +s x )
18 16 2 syl 
 |-  ( ( ph /\ ( bday ` Y ) e. ( bday ` Z ) ) -> X e. No )
19 16 3 syl 
 |-  ( ( ph /\ ( bday ` Y ) e. ( bday ` Z ) ) -> Y e. No )
20 16 4 syl 
 |-  ( ( ph /\ ( bday ` Y ) e. ( bday ` Z ) ) -> Z e. No )
21 16 5 syl 
 |-  ( ( ph /\ ( bday ` Y ) e. ( bday ` Z ) ) -> Y
22 simpr 
 |-  ( ( ph /\ ( bday ` Y ) e. ( bday ` Z ) ) -> ( bday ` Y ) e. ( bday ` Z ) )
23 17 18 19 20 21 22 addsproplem4 
 |-  ( ( ph /\ ( bday ` Y ) e. ( bday ` Z ) ) -> ( Y +s X )
24 23 ex 
 |-  ( ph -> ( ( bday ` Y ) e. ( bday ` Z ) -> ( Y +s X )
25 simpl 
 |-  ( ( ph /\ ( bday ` Y ) = ( bday ` Z ) ) -> ph )
26 25 1 syl 
 |-  ( ( ph /\ ( bday ` Y ) = ( bday ` Z ) ) -> A. x e. No A. y e. No A. z e. No ( ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) -> ( ( x +s y ) e. No /\ ( y  ( y +s x )
27 25 2 syl 
 |-  ( ( ph /\ ( bday ` Y ) = ( bday ` Z ) ) -> X e. No )
28 25 3 syl 
 |-  ( ( ph /\ ( bday ` Y ) = ( bday ` Z ) ) -> Y e. No )
29 25 4 syl 
 |-  ( ( ph /\ ( bday ` Y ) = ( bday ` Z ) ) -> Z e. No )
30 25 5 syl 
 |-  ( ( ph /\ ( bday ` Y ) = ( bday ` Z ) ) -> Y
31 simpr 
 |-  ( ( ph /\ ( bday ` Y ) = ( bday ` Z ) ) -> ( bday ` Y ) = ( bday ` Z ) )
32 26 27 28 29 30 31 addsproplem6 
 |-  ( ( ph /\ ( bday ` Y ) = ( bday ` Z ) ) -> ( Y +s X )
33 32 ex 
 |-  ( ph -> ( ( bday ` Y ) = ( bday ` Z ) -> ( Y +s X )
34 1 adantr 
 |-  ( ( ph /\ ( bday ` Z ) e. ( bday ` Y ) ) -> A. x e. No A. y e. No A. z e. No ( ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) -> ( ( x +s y ) e. No /\ ( y  ( y +s x )
35 2 adantr 
 |-  ( ( ph /\ ( bday ` Z ) e. ( bday ` Y ) ) -> X e. No )
36 3 adantr 
 |-  ( ( ph /\ ( bday ` Z ) e. ( bday ` Y ) ) -> Y e. No )
37 4 adantr 
 |-  ( ( ph /\ ( bday ` Z ) e. ( bday ` Y ) ) -> Z e. No )
38 5 adantr 
 |-  ( ( ph /\ ( bday ` Z ) e. ( bday ` Y ) ) -> Y
39 simpr 
 |-  ( ( ph /\ ( bday ` Z ) e. ( bday ` Y ) ) -> ( bday ` Z ) e. ( bday ` Y ) )
40 34 35 36 37 38 39 addsproplem5 
 |-  ( ( ph /\ ( bday ` Z ) e. ( bday ` Y ) ) -> ( Y +s X )
41 40 ex 
 |-  ( ph -> ( ( bday ` Z ) e. ( bday ` Y ) -> ( Y +s X )
42 24 33 41 3jaod 
 |-  ( ph -> ( ( ( bday ` Y ) e. ( bday ` Z ) \/ ( bday ` Y ) = ( bday ` Z ) \/ ( bday ` Z ) e. ( bday ` Y ) ) -> ( Y +s X )
43 15 42 mpi 
 |-  ( ph -> ( Y +s X )