Metamath Proof Explorer

Theorem scutun12

Description: Union law for surreal cuts. (Contributed by Scott Fenton, 9-Dec-2021)

Ref Expression
Assertion scutun12 
|- ( ( A < ( ( A u. C ) |s ( B u. D ) ) = ( A |s B ) )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( A < A <
2 scutcut 
 |-  ( A < ( ( A |s B ) e. No /\ A <
3 1 2 syl 
 |-  ( ( A < ( ( A |s B ) e. No /\ A <
4 3 simp2d 
 |-  ( ( A < A <
5 simp2 
 |-  ( ( A < C <
6 ssltun1 
 |-  ( ( A < ( A u. C ) <
7 4 5 6 syl2anc 
 |-  ( ( A < ( A u. C ) <
8 3 simp3d 
 |-  ( ( A < { ( A |s B ) } <
9 simp3 
 |-  ( ( A < { ( A |s B ) } <
10 ssltun2 
 |-  ( ( { ( A |s B ) } < { ( A |s B ) } <
11 8 9 10 syl2anc 
 |-  ( ( A < { ( A |s B ) } <
12 ovex 
 |-  ( A |s B ) e. _V
13 12 snnz 
 |-  { ( A |s B ) } =/= (/)
14 sslttr 
 |-  ( ( ( A u. C ) < ( A u. C ) <
15 13 14 mp3an3 
 |-  ( ( ( A u. C ) < ( A u. C ) <
16 7 11 15 syl2anc 
 |-  ( ( A < ( A u. C ) <
17 scutval 
 |-  ( ( A u. C ) < ( ( A u. C ) |s ( B u. D ) ) = ( iota_ x e. { y e. No | ( ( A u. C ) <
18 16 17 syl 
 |-  ( ( A < ( ( A u. C ) |s ( B u. D ) ) = ( iota_ x e. { y e. No | ( ( A u. C ) <
19 vex 
 |-  x e. _V
20 19 elima 
 |-  ( x e. ( bday " { y e. No | ( ( A u. C ) < E. z e. { y e. No | ( ( A u. C ) <
21 sneq 
 |-  ( y = z -> { y } = { z } )
22 21 breq2d 
 |-  ( y = z -> ( ( A u. C ) < ( A u. C ) <
23 21 breq1d 
 |-  ( y = z -> ( { y } < { z } <
24 22 23 anbi12d 
 |-  ( y = z -> ( ( ( A u. C ) < ( ( A u. C ) <
25 24 rexrab 
 |-  ( E. z e. { y e. No | ( ( A u. C ) < E. z e. No ( ( ( A u. C ) <
26 20 25 bitri 
 |-  ( x e. ( bday " { y e. No | ( ( A u. C ) < E. z e. No ( ( ( A u. C ) <
27 simplr 
 |-  ( ( ( ( A < z e. No )
28 bdayfn 
 |-  bday Fn No
29 fnbrfvb 
 |-  ( ( bday Fn No /\ z e. No ) -> ( ( bday ` z ) = x <-> z bday x ) )
30 28 29 mpan 
 |-  ( z e. No -> ( ( bday ` z ) = x <-> z bday x ) )
31 27 30 syl 
 |-  ( ( ( ( A < ( ( bday ` z ) = x <-> z bday x ) )
32 simpll1 
 |-  ( ( ( ( A < A <
33 scutbday 
 |-  ( A < ( bday ` ( A |s B ) ) = |^| ( bday " { y e. No | ( A <
34 32 33 syl 
 |-  ( ( ( ( A < ( bday ` ( A |s B ) ) = |^| ( bday " { y e. No | ( A <
35 simprl 
 |-  ( ( ( ( A < ( A u. C ) <
36 ssun1 
 |-  A C_ ( A u. C )
37 sssslt1 
 |-  ( ( ( A u. C ) < A <
38 36 37 mpan2 
 |-  ( ( A u. C ) < A <
39 35 38 syl 
 |-  ( ( ( ( A < A <
40 simprr 
 |-  ( ( ( ( A < { z } <
41 ssun1 
 |-  B C_ ( B u. D )
42 sssslt2 
 |-  ( ( { z } < { z } <
43 41 42 mpan2 
 |-  ( { z } < { z } <
44 40 43 syl 
 |-  ( ( ( ( A < { z } <
45 39 44 jca 
 |-  ( ( ( ( A < ( A <
46 21 breq2d 
 |-  ( y = z -> ( A < A <
47 21 breq1d 
 |-  ( y = z -> ( { y } < { z } <
48 46 47 anbi12d 
 |-  ( y = z -> ( ( A < ( A <
49 48 elrab 
 |-  ( z e. { y e. No | ( A < ( z e. No /\ ( A <
50 27 45 49 sylanbrc 
 |-  ( ( ( ( A < z e. { y e. No | ( A <
51 ssrab2 
 |-  { y e. No | ( A <
52 fnfvima 
 |-  ( ( bday Fn No /\ { y e. No | ( A < ( bday ` z ) e. ( bday " { y e. No | ( A <
53 28 51 52 mp3an12 
 |-  ( z e. { y e. No | ( A < ( bday ` z ) e. ( bday " { y e. No | ( A <
54 50 53 syl 
 |-  ( ( ( ( A < ( bday ` z ) e. ( bday " { y e. No | ( A <
55 intss1 
 |-  ( ( bday ` z ) e. ( bday " { y e. No | ( A < |^| ( bday " { y e. No | ( A <
56 54 55 syl 
 |-  ( ( ( ( A < |^| ( bday " { y e. No | ( A <
57 34 56 eqsstrd 
 |-  ( ( ( ( A < ( bday ` ( A |s B ) ) C_ ( bday ` z ) )
58 sseq2 
 |-  ( ( bday ` z ) = x -> ( ( bday ` ( A |s B ) ) C_ ( bday ` z ) <-> ( bday ` ( A |s B ) ) C_ x ) )
59 58 biimpd 
 |-  ( ( bday ` z ) = x -> ( ( bday ` ( A |s B ) ) C_ ( bday ` z ) -> ( bday ` ( A |s B ) ) C_ x ) )
60 59 com12 
 |-  ( ( bday ` ( A |s B ) ) C_ ( bday ` z ) -> ( ( bday ` z ) = x -> ( bday ` ( A |s B ) ) C_ x ) )
61 57 60 syl 
 |-  ( ( ( ( A < ( ( bday ` z ) = x -> ( bday ` ( A |s B ) ) C_ x ) )
62 31 61 sylbird 
 |-  ( ( ( ( A < ( z bday x -> ( bday ` ( A |s B ) ) C_ x ) )
63 62 ex 
 |-  ( ( ( A < ( ( ( A u. C ) < ( z bday x -> ( bday ` ( A |s B ) ) C_ x ) ) )
64 63 impd 
 |-  ( ( ( A < ( ( ( ( A u. C ) < ( bday ` ( A |s B ) ) C_ x ) )
65 64 rexlimdva 
 |-  ( ( A < ( E. z e. No ( ( ( A u. C ) < ( bday ` ( A |s B ) ) C_ x ) )
66 26 65 syl5bi 
 |-  ( ( A < ( x e. ( bday " { y e. No | ( ( A u. C ) < ( bday ` ( A |s B ) ) C_ x ) )
67 66 ralrimiv 
 |-  ( ( A < A. x e. ( bday " { y e. No | ( ( A u. C ) <
68 ssint 
 |-  ( ( bday ` ( A |s B ) ) C_ |^| ( bday " { y e. No | ( ( A u. C ) < A. x e. ( bday " { y e. No | ( ( A u. C ) <
69 67 68 sylibr 
 |-  ( ( A < ( bday ` ( A |s B ) ) C_ |^| ( bday " { y e. No | ( ( A u. C ) <
70 3 simp1d 
 |-  ( ( A < ( A |s B ) e. No )
71 7 11 jca 
 |-  ( ( A < ( ( A u. C ) <
72 sneq 
 |-  ( y = ( A |s B ) -> { y } = { ( A |s B ) } )
73 72 breq2d 
 |-  ( y = ( A |s B ) -> ( ( A u. C ) < ( A u. C ) <
74 72 breq1d 
 |-  ( y = ( A |s B ) -> ( { y } < { ( A |s B ) } <
75 73 74 anbi12d 
 |-  ( y = ( A |s B ) -> ( ( ( A u. C ) < ( ( A u. C ) <
76 75 elrab 
 |-  ( ( A |s B ) e. { y e. No | ( ( A u. C ) < ( ( A |s B ) e. No /\ ( ( A u. C ) <
77 70 71 76 sylanbrc 
 |-  ( ( A < ( A |s B ) e. { y e. No | ( ( A u. C ) <
78 ssrab2 
 |-  { y e. No | ( ( A u. C ) <
79 fnfvima 
 |-  ( ( bday Fn No /\ { y e. No | ( ( A u. C ) < ( bday ` ( A |s B ) ) e. ( bday " { y e. No | ( ( A u. C ) <
80 28 78 79 mp3an12 
 |-  ( ( A |s B ) e. { y e. No | ( ( A u. C ) < ( bday ` ( A |s B ) ) e. ( bday " { y e. No | ( ( A u. C ) <
81 77 80 syl 
 |-  ( ( A < ( bday ` ( A |s B ) ) e. ( bday " { y e. No | ( ( A u. C ) <
82 intss1 
 |-  ( ( bday ` ( A |s B ) ) e. ( bday " { y e. No | ( ( A u. C ) < |^| ( bday " { y e. No | ( ( A u. C ) <
83 81 82 syl 
 |-  ( ( A < |^| ( bday " { y e. No | ( ( A u. C ) <
84 69 83 eqssd 
 |-  ( ( A < ( bday ` ( A |s B ) ) = |^| ( bday " { y e. No | ( ( A u. C ) <
85 conway 
 |-  ( ( A u. C ) < E! x e. { y e. No | ( ( A u. C ) <
86 16 85 syl 
 |-  ( ( A < E! x e. { y e. No | ( ( A u. C ) <
87 fveqeq2 
 |-  ( x = ( A |s B ) -> ( ( bday ` x ) = |^| ( bday " { y e. No | ( ( A u. C ) < ( bday ` ( A |s B ) ) = |^| ( bday " { y e. No | ( ( A u. C ) <
88 87 riota2 
 |-  ( ( ( A |s B ) e. { y e. No | ( ( A u. C ) < ( ( bday ` ( A |s B ) ) = |^| ( bday " { y e. No | ( ( A u. C ) < ( iota_ x e. { y e. No | ( ( A u. C ) <
89 77 86 88 syl2anc 
 |-  ( ( A < ( ( bday ` ( A |s B ) ) = |^| ( bday " { y e. No | ( ( A u. C ) < ( iota_ x e. { y e. No | ( ( A u. C ) <
90 84 89 mpbid 
 |-  ( ( A < ( iota_ x e. { y e. No | ( ( A u. C ) <
91 90 eqcomd 
 |-  ( ( A < ( A |s B ) = ( iota_ x e. { y e. No | ( ( A u. C ) <
92 18 91 eqtr4d 
 |-  ( ( A < ( ( A u. C ) |s ( B u. D ) ) = ( A |s B ) )