Metamath Proof Explorer

Theorem onscutlt

Description: A surreal ordinal is the simplest number greater than all previous surreal ordinals. Theorem 15 of Conway p. 28. (Contributed by Scott Fenton, 4-Nov-2025)

Ref Expression
Assertion onscutlt 
|- ( A e. On_s -> A = ( { x e. On_s | x

Proof

Step Hyp Ref Expression
1 onsno 
 |-  ( A e. On_s -> A e. No )
2 sltonex 
 |-  ( A e. No -> { x e. On_s | x
3 1 2 syl 
 |-  ( A e. On_s -> { x e. On_s | x
4 snexg 
 |-  ( A e. On_s -> { A } e. _V )
5 ssrab2 
 |-  { x e. On_s | x
6 onssno 
 |-  On_s C_ No
7 5 6 sstri 
 |-  { x e. On_s | x
8 7 a1i 
 |-  ( A e. On_s -> { x e. On_s | x
9 1 snssd 
 |-  ( A e. On_s -> { A } C_ No )
10 breq1 
 |-  ( x = y -> ( x  y
11 10 elrab 
 |-  ( y e. { x e. On_s | x  ( y e. On_s /\ y
12 11 simprbi 
 |-  ( y e. { x e. On_s | x  y
13 velsn 
 |-  ( z e. { A } <-> z = A )
14 breq2 
 |-  ( z = A -> ( y  y
15 13 14 sylbi 
 |-  ( z e. { A } -> ( y  y
16 12 15 syl5ibrcom 
 |-  ( y e. { x e. On_s | x  ( z e. { A } -> y
17 16 imp 
 |-  ( ( y e. { x e. On_s | x  y
18 17 3adant1 
 |-  ( ( A e. On_s /\ y e. { x e. On_s | x  y
19 3 4 8 9 18 ssltd 
 |-  ( A e. On_s -> { x e. On_s | x
20 snelpwi 
 |-  ( A e. No -> { A } e. ~P No )
21 nulssgt 
 |-  ( { A } e. ~P No -> { A } <
22 1 20 21 3syl 
 |-  ( A e. On_s -> { A } <
23 ssltsep 
 |-  ( { x e. On_s | x  A. z e. { x e. On_s | x
24 vex 
 |-  y e. _V
25 breq2 
 |-  ( w = y -> ( z  z
26 24 25 ralsn 
 |-  ( A. w e. { y } z  z
27 26 ralbii 
 |-  ( A. z e. { x e. On_s | x  A. z e. { x e. On_s | x
28 breq1 
 |-  ( x = z -> ( x  z
29 28 ralrab 
 |-  ( A. z e. { x e. On_s | x  A. z e. On_s ( z  z
30 27 29 bitri 
 |-  ( A. z e. { x e. On_s | x  A. z e. On_s ( z  z
31 23 30 sylib 
 |-  ( { x e. On_s | x  A. z e. On_s ( z  z
32 fvex 
 |-  ( _Left ` y ) e. _V
33 fvex 
 |-  ( _Right ` y ) e. _V
34 32 33 unex 
 |-  ( ( _Left ` y ) u. ( _Right ` y ) ) e. _V
35 34 a1i 
 |-  ( ( ( A e. On_s /\ y e. No ) /\ ( bday ` y ) e. ( bday ` A ) ) -> ( ( _Left ` y ) u. ( _Right ` y ) ) e. _V )
36 leftssno 
 |-  ( _Left ` y ) C_ No
37 rightssno 
 |-  ( _Right ` y ) C_ No
38 36 37 unssi 
 |-  ( ( _Left ` y ) u. ( _Right ` y ) ) C_ No
39 38 a1i 
 |-  ( ( ( A e. On_s /\ y e. No ) /\ ( bday ` y ) e. ( bday ` A ) ) -> ( ( _Left ` y ) u. ( _Right ` y ) ) C_ No )
40 eqidd 
 |-  ( ( ( A e. On_s /\ y e. No ) /\ ( bday ` y ) e. ( bday ` A ) ) -> ( ( ( _Left ` y ) u. ( _Right ` y ) ) |s (/) ) = ( ( ( _Left ` y ) u. ( _Right ` y ) ) |s (/) ) )
41 35 39 40 elons2d 
 |-  ( ( ( A e. On_s /\ y e. No ) /\ ( bday ` y ) e. ( bday ` A ) ) -> ( ( ( _Left ` y ) u. ( _Right ` y ) ) |s (/) ) e. On_s )
42 34 elpw 
 |-  ( ( ( _Left ` y ) u. ( _Right ` y ) ) e. ~P No <-> ( ( _Left ` y ) u. ( _Right ` y ) ) C_ No )
43 38 42 mpbir 
 |-  ( ( _Left ` y ) u. ( _Right ` y ) ) e. ~P No
44 nulssgt 
 |-  ( ( ( _Left ` y ) u. ( _Right ` y ) ) e. ~P No -> ( ( _Left ` y ) u. ( _Right ` y ) ) <
45 43 44 mp1i 
 |-  ( ( ( A e. On_s /\ y e. No ) /\ ( bday ` y ) e. ( bday ` A ) ) -> ( ( _Left ` y ) u. ( _Right ` y ) ) <
46 un0 
 |-  ( ( ( _Left ` y ) u. ( _Right ` y ) ) u. (/) ) = ( ( _Left ` y ) u. ( _Right ` y ) )
47 lrold 
 |-  ( ( _Left ` y ) u. ( _Right ` y ) ) = ( _Old ` ( bday ` y ) )
48 46 47 eqtri 
 |-  ( ( ( _Left ` y ) u. ( _Right ` y ) ) u. (/) ) = ( _Old ` ( bday ` y ) )
49 48 imaeq2i 
 |-  ( bday " ( ( ( _Left ` y ) u. ( _Right ` y ) ) u. (/) ) ) = ( bday " ( _Old ` ( bday ` y ) ) )
50 simpr 
 |-  ( ( ( ( A e. On_s /\ y e. No ) /\ ( bday ` y ) e. ( bday ` A ) ) /\ z e. ( _Old ` ( bday ` y ) ) ) -> z e. ( _Old ` ( bday ` y ) ) )
51 bdayelon 
 |-  ( bday ` y ) e. On
52 oldssno 
 |-  ( _Old ` ( bday ` y ) ) C_ No
53 52 sseli 
 |-  ( z e. ( _Old ` ( bday ` y ) ) -> z e. No )
54 53 adantl 
 |-  ( ( ( ( A e. On_s /\ y e. No ) /\ ( bday ` y ) e. ( bday ` A ) ) /\ z e. ( _Old ` ( bday ` y ) ) ) -> z e. No )
55 oldbday 
 |-  ( ( ( bday ` y ) e. On /\ z e. No ) -> ( z e. ( _Old ` ( bday ` y ) ) <-> ( bday ` z ) e. ( bday ` y ) ) )
56 51 54 55 sylancr 
 |-  ( ( ( ( A e. On_s /\ y e. No ) /\ ( bday ` y ) e. ( bday ` A ) ) /\ z e. ( _Old ` ( bday ` y ) ) ) -> ( z e. ( _Old ` ( bday ` y ) ) <-> ( bday ` z ) e. ( bday ` y ) ) )
57 50 56 mpbid 
 |-  ( ( ( ( A e. On_s /\ y e. No ) /\ ( bday ` y ) e. ( bday ` A ) ) /\ z e. ( _Old ` ( bday ` y ) ) ) -> ( bday ` z ) e. ( bday ` y ) )
58 57 ralrimiva 
 |-  ( ( ( A e. On_s /\ y e. No ) /\ ( bday ` y ) e. ( bday ` A ) ) -> A. z e. ( _Old ` ( bday ` y ) ) ( bday ` z ) e. ( bday ` y ) )
59 bdayfun 
 |-  Fun bday
60 bdaydm 
 |-  dom bday = No
61 52 60 sseqtrri 
 |-  ( _Old ` ( bday ` y ) ) C_ dom bday
62 funimass4 
 |-  ( ( Fun bday /\ ( _Old ` ( bday ` y ) ) C_ dom bday ) -> ( ( bday " ( _Old ` ( bday ` y ) ) ) C_ ( bday ` y ) <-> A. z e. ( _Old ` ( bday ` y ) ) ( bday ` z ) e. ( bday ` y ) ) )
63 59 61 62 mp2an 
 |-  ( ( bday " ( _Old ` ( bday ` y ) ) ) C_ ( bday ` y ) <-> A. z e. ( _Old ` ( bday ` y ) ) ( bday ` z ) e. ( bday ` y ) )
64 58 63 sylibr 
 |-  ( ( ( A e. On_s /\ y e. No ) /\ ( bday ` y ) e. ( bday ` A ) ) -> ( bday " ( _Old ` ( bday ` y ) ) ) C_ ( bday ` y ) )
65 49 64 eqsstrid 
 |-  ( ( ( A e. On_s /\ y e. No ) /\ ( bday ` y ) e. ( bday ` A ) ) -> ( bday " ( ( ( _Left ` y ) u. ( _Right ` y ) ) u. (/) ) ) C_ ( bday ` y ) )
66 scutbdaybnd 
 |-  ( ( ( ( _Left ` y ) u. ( _Right ` y ) ) < ( bday ` ( ( ( _Left ` y ) u. ( _Right ` y ) ) |s (/) ) ) C_ ( bday ` y ) )
67 51 66 mp3an2 
 |-  ( ( ( ( _Left ` y ) u. ( _Right ` y ) ) < ( bday ` ( ( ( _Left ` y ) u. ( _Right ` y ) ) |s (/) ) ) C_ ( bday ` y ) )
68 45 65 67 syl2anc 
 |-  ( ( ( A e. On_s /\ y e. No ) /\ ( bday ` y ) e. ( bday ` A ) ) -> ( bday ` ( ( ( _Left ` y ) u. ( _Right ` y ) ) |s (/) ) ) C_ ( bday ` y ) )
69 simpr 
 |-  ( ( ( A e. On_s /\ y e. No ) /\ ( bday ` y ) e. ( bday ` A ) ) -> ( bday ` y ) e. ( bday ` A ) )
70 bdayelon 
 |-  ( bday ` ( ( ( _Left ` y ) u. ( _Right ` y ) ) |s (/) ) ) e. On
71 bdayelon 
 |-  ( bday ` A ) e. On
72 ontr2 
 |-  ( ( ( bday ` ( ( ( _Left ` y ) u. ( _Right ` y ) ) |s (/) ) ) e. On /\ ( bday ` A ) e. On ) -> ( ( ( bday ` ( ( ( _Left ` y ) u. ( _Right ` y ) ) |s (/) ) ) C_ ( bday ` y ) /\ ( bday ` y ) e. ( bday ` A ) ) -> ( bday ` ( ( ( _Left ` y ) u. ( _Right ` y ) ) |s (/) ) ) e. ( bday ` A ) ) )
73 70 71 72 mp2an 
 |-  ( ( ( bday ` ( ( ( _Left ` y ) u. ( _Right ` y ) ) |s (/) ) ) C_ ( bday ` y ) /\ ( bday ` y ) e. ( bday ` A ) ) -> ( bday ` ( ( ( _Left ` y ) u. ( _Right ` y ) ) |s (/) ) ) e. ( bday ` A ) )
74 68 69 73 syl2anc 
 |-  ( ( ( A e. On_s /\ y e. No ) /\ ( bday ` y ) e. ( bday ` A ) ) -> ( bday ` ( ( ( _Left ` y ) u. ( _Right ` y ) ) |s (/) ) ) e. ( bday ` A ) )
75 45 scutcld 
 |-  ( ( ( A e. On_s /\ y e. No ) /\ ( bday ` y ) e. ( bday ` A ) ) -> ( ( ( _Left ` y ) u. ( _Right ` y ) ) |s (/) ) e. No )
76 oldbday 
 |-  ( ( ( bday ` A ) e. On /\ ( ( ( _Left ` y ) u. ( _Right ` y ) ) |s (/) ) e. No ) -> ( ( ( ( _Left ` y ) u. ( _Right ` y ) ) |s (/) ) e. ( _Old ` ( bday ` A ) ) <-> ( bday ` ( ( ( _Left ` y ) u. ( _Right ` y ) ) |s (/) ) ) e. ( bday ` A ) ) )
77 71 75 76 sylancr 
 |-  ( ( ( A e. On_s /\ y e. No ) /\ ( bday ` y ) e. ( bday ` A ) ) -> ( ( ( ( _Left ` y ) u. ( _Right ` y ) ) |s (/) ) e. ( _Old ` ( bday ` A ) ) <-> ( bday ` ( ( ( _Left ` y ) u. ( _Right ` y ) ) |s (/) ) ) e. ( bday ` A ) ) )
78 74 77 mpbird 
 |-  ( ( ( A e. On_s /\ y e. No ) /\ ( bday ` y ) e. ( bday ` A ) ) -> ( ( ( _Left ` y ) u. ( _Right ` y ) ) |s (/) ) e. ( _Old ` ( bday ` A ) ) )
79 elons 
 |-  ( A e. On_s <-> ( A e. No /\ ( _Right ` A ) = (/) ) )
80 79 simprbi 
 |-  ( A e. On_s -> ( _Right ` A ) = (/) )
81 80 ad2antrr 
 |-  ( ( ( A e. On_s /\ y e. No ) /\ ( bday ` y ) e. ( bday ` A ) ) -> ( _Right ` A ) = (/) )
82 81 uneq2d 
 |-  ( ( ( A e. On_s /\ y e. No ) /\ ( bday ` y ) e. ( bday ` A ) ) -> ( ( _Left ` A ) u. ( _Right ` A ) ) = ( ( _Left ` A ) u. (/) ) )
83 lrold 
 |-  ( ( _Left ` A ) u. ( _Right ` A ) ) = ( _Old ` ( bday ` A ) )
84 un0 
 |-  ( ( _Left ` A ) u. (/) ) = ( _Left ` A )
85 82 83 84 3eqtr3g 
 |-  ( ( ( A e. On_s /\ y e. No ) /\ ( bday ` y ) e. ( bday ` A ) ) -> ( _Old ` ( bday ` A ) ) = ( _Left ` A ) )
86 78 85 eleqtrd 
 |-  ( ( ( A e. On_s /\ y e. No ) /\ ( bday ` y ) e. ( bday ` A ) ) -> ( ( ( _Left ` y ) u. ( _Right ` y ) ) |s (/) ) e. ( _Left ` A ) )
87 leftlt 
 |-  ( ( ( ( _Left ` y ) u. ( _Right ` y ) ) |s (/) ) e. ( _Left ` A ) -> ( ( ( _Left ` y ) u. ( _Right ` y ) ) |s (/) )
88 86 87 syl 
 |-  ( ( ( A e. On_s /\ y e. No ) /\ ( bday ` y ) e. ( bday ` A ) ) -> ( ( ( _Left ` y ) u. ( _Right ` y ) ) |s (/) )
89 simplr 
 |-  ( ( ( A e. On_s /\ y e. No ) /\ ( bday ` y ) e. ( bday ` A ) ) -> y e. No )
90 slerflex 
 |-  ( y e. No -> y <_s y )
91 lrcut 
 |-  ( y e. No -> ( ( _Left ` y ) |s ( _Right ` y ) ) = y )
92 90 91 breqtrrd 
 |-  ( y e. No -> y <_s ( ( _Left ` y ) |s ( _Right ` y ) ) )
93 89 92 syl 
 |-  ( ( ( A e. On_s /\ y e. No ) /\ ( bday ` y ) e. ( bday ` A ) ) -> y <_s ( ( _Left ` y ) |s ( _Right ` y ) ) )
94 uneq2 
 |-  ( ( _Right ` y ) = (/) -> ( ( _Left ` y ) u. ( _Right ` y ) ) = ( ( _Left ` y ) u. (/) ) )
95 un0 
 |-  ( ( _Left ` y ) u. (/) ) = ( _Left ` y )
96 94 95 eqtrdi 
 |-  ( ( _Right ` y ) = (/) -> ( ( _Left ` y ) u. ( _Right ` y ) ) = ( _Left ` y ) )
97 eqcom 
 |-  ( ( _Right ` y ) = (/) <-> (/) = ( _Right ` y ) )
98 97 biimpi 
 |-  ( ( _Right ` y ) = (/) -> (/) = ( _Right ` y ) )
99 96 98 oveq12d 
 |-  ( ( _Right ` y ) = (/) -> ( ( ( _Left ` y ) u. ( _Right ` y ) ) |s (/) ) = ( ( _Left ` y ) |s ( _Right ` y ) ) )
100 99 breq2d 
 |-  ( ( _Right ` y ) = (/) -> ( y <_s ( ( ( _Left ` y ) u. ( _Right ` y ) ) |s (/) ) <-> y <_s ( ( _Left ` y ) |s ( _Right ` y ) ) ) )
101 93 100 imbitrrid 
 |-  ( ( _Right ` y ) = (/) -> ( ( ( A e. On_s /\ y e. No ) /\ ( bday ` y ) e. ( bday ` A ) ) -> y <_s ( ( ( _Left ` y ) u. ( _Right ` y ) ) |s (/) ) ) )
102 simprlr 
 |-  ( ( ( _Right ` y ) =/= (/) /\ ( ( A e. On_s /\ y e. No ) /\ ( bday ` y ) e. ( bday ` A ) ) ) -> y e. No )
103 75 adantl 
 |-  ( ( ( _Right ` y ) =/= (/) /\ ( ( A e. On_s /\ y e. No ) /\ ( bday ` y ) e. ( bday ` A ) ) ) -> ( ( ( _Left ` y ) u. ( _Right ` y ) ) |s (/) ) e. No )
104 n0 
 |-  ( ( _Right ` y ) =/= (/) <-> E. w w e. ( _Right ` y ) )
105 breq2 
 |-  ( z = w -> ( y <_s z <-> y <_s w ) )
106 elun2 
 |-  ( w e. ( _Right ` y ) -> w e. ( ( _Left ` y ) u. ( _Right ` y ) ) )
107 106 adantr 
 |-  ( ( w e. ( _Right ` y ) /\ ( ( A e. On_s /\ y e. No ) /\ ( bday ` y ) e. ( bday ` A ) ) ) -> w e. ( ( _Left ` y ) u. ( _Right ` y ) ) )
108 simprlr 
 |-  ( ( w e. ( _Right ` y ) /\ ( ( A e. On_s /\ y e. No ) /\ ( bday ` y ) e. ( bday ` A ) ) ) -> y e. No )
109 37 sseli 
 |-  ( w e. ( _Right ` y ) -> w e. No )
110 109 adantr 
 |-  ( ( w e. ( _Right ` y ) /\ ( ( A e. On_s /\ y e. No ) /\ ( bday ` y ) e. ( bday ` A ) ) ) -> w e. No )
111 rightgt 
 |-  ( w e. ( _Right ` y ) -> y
112 111 adantr 
 |-  ( ( w e. ( _Right ` y ) /\ ( ( A e. On_s /\ y e. No ) /\ ( bday ` y ) e. ( bday ` A ) ) ) -> y
113 108 110 112 sltled 
 |-  ( ( w e. ( _Right ` y ) /\ ( ( A e. On_s /\ y e. No ) /\ ( bday ` y ) e. ( bday ` A ) ) ) -> y <_s w )
114 105 107 113 rspcedvdw 
 |-  ( ( w e. ( _Right ` y ) /\ ( ( A e. On_s /\ y e. No ) /\ ( bday ` y ) e. ( bday ` A ) ) ) -> E. z e. ( ( _Left ` y ) u. ( _Right ` y ) ) y <_s z )
115 114 ex 
 |-  ( w e. ( _Right ` y ) -> ( ( ( A e. On_s /\ y e. No ) /\ ( bday ` y ) e. ( bday ` A ) ) -> E. z e. ( ( _Left ` y ) u. ( _Right ` y ) ) y <_s z ) )
116 115 exlimiv 
 |-  ( E. w w e. ( _Right ` y ) -> ( ( ( A e. On_s /\ y e. No ) /\ ( bday ` y ) e. ( bday ` A ) ) -> E. z e. ( ( _Left ` y ) u. ( _Right ` y ) ) y <_s z ) )
117 104 116 sylbi 
 |-  ( ( _Right ` y ) =/= (/) -> ( ( ( A e. On_s /\ y e. No ) /\ ( bday ` y ) e. ( bday ` A ) ) -> E. z e. ( ( _Left ` y ) u. ( _Right ` y ) ) y <_s z ) )
118 117 imp 
 |-  ( ( ( _Right ` y ) =/= (/) /\ ( ( A e. On_s /\ y e. No ) /\ ( bday ` y ) e. ( bday ` A ) ) ) -> E. z e. ( ( _Left ` y ) u. ( _Right ` y ) ) y <_s z )
119 118 orcd 
 |-  ( ( ( _Right ` y ) =/= (/) /\ ( ( A e. On_s /\ y e. No ) /\ ( bday ` y ) e. ( bday ` A ) ) ) -> ( E. z e. ( ( _Left ` y ) u. ( _Right ` y ) ) y <_s z \/ E. w e. ( _Right ` y ) w <_s ( ( ( _Left ` y ) u. ( _Right ` y ) ) |s (/) ) ) )
120 lltropt 
 |-  ( _Left ` y ) <
121 120 a1i 
 |-  ( ( ( _Right ` y ) =/= (/) /\ ( ( A e. On_s /\ y e. No ) /\ ( bday ` y ) e. ( bday ` A ) ) ) -> ( _Left ` y ) <
122 43 44 mp1i 
 |-  ( ( ( _Right ` y ) =/= (/) /\ ( ( A e. On_s /\ y e. No ) /\ ( bday ` y ) e. ( bday ` A ) ) ) -> ( ( _Left ` y ) u. ( _Right ` y ) ) <
123 102 91 syl 
 |-  ( ( ( _Right ` y ) =/= (/) /\ ( ( A e. On_s /\ y e. No ) /\ ( bday ` y ) e. ( bday ` A ) ) ) -> ( ( _Left ` y ) |s ( _Right ` y ) ) = y )
124 123 eqcomd 
 |-  ( ( ( _Right ` y ) =/= (/) /\ ( ( A e. On_s /\ y e. No ) /\ ( bday ` y ) e. ( bday ` A ) ) ) -> y = ( ( _Left ` y ) |s ( _Right ` y ) ) )
125 eqidd 
 |-  ( ( ( _Right ` y ) =/= (/) /\ ( ( A e. On_s /\ y e. No ) /\ ( bday ` y ) e. ( bday ` A ) ) ) -> ( ( ( _Left ` y ) u. ( _Right ` y ) ) |s (/) ) = ( ( ( _Left ` y ) u. ( _Right ` y ) ) |s (/) ) )
126 sltrec 
 |-  ( ( ( ( _Left ` y ) < ( y  ( E. z e. ( ( _Left ` y ) u. ( _Right ` y ) ) y <_s z \/ E. w e. ( _Right ` y ) w <_s ( ( ( _Left ` y ) u. ( _Right ` y ) ) |s (/) ) ) ) )
127 121 122 124 125 126 syl22anc 
 |-  ( ( ( _Right ` y ) =/= (/) /\ ( ( A e. On_s /\ y e. No ) /\ ( bday ` y ) e. ( bday ` A ) ) ) -> ( y  ( E. z e. ( ( _Left ` y ) u. ( _Right ` y ) ) y <_s z \/ E. w e. ( _Right ` y ) w <_s ( ( ( _Left ` y ) u. ( _Right ` y ) ) |s (/) ) ) ) )
128 119 127 mpbird 
 |-  ( ( ( _Right ` y ) =/= (/) /\ ( ( A e. On_s /\ y e. No ) /\ ( bday ` y ) e. ( bday ` A ) ) ) -> y
129 102 103 128 sltled 
 |-  ( ( ( _Right ` y ) =/= (/) /\ ( ( A e. On_s /\ y e. No ) /\ ( bday ` y ) e. ( bday ` A ) ) ) -> y <_s ( ( ( _Left ` y ) u. ( _Right ` y ) ) |s (/) ) )
130 129 ex 
 |-  ( ( _Right ` y ) =/= (/) -> ( ( ( A e. On_s /\ y e. No ) /\ ( bday ` y ) e. ( bday ` A ) ) -> y <_s ( ( ( _Left ` y ) u. ( _Right ` y ) ) |s (/) ) ) )
131 101 130 pm2.61ine 
 |-  ( ( ( A e. On_s /\ y e. No ) /\ ( bday ` y ) e. ( bday ` A ) ) -> y <_s ( ( ( _Left ` y ) u. ( _Right ` y ) ) |s (/) ) )
132 slenlt 
 |-  ( ( y e. No /\ ( ( ( _Left ` y ) u. ( _Right ` y ) ) |s (/) ) e. No ) -> ( y <_s ( ( ( _Left ` y ) u. ( _Right ` y ) ) |s (/) ) <-> -. ( ( ( _Left ` y ) u. ( _Right ` y ) ) |s (/) )
133 89 75 132 syl2anc 
 |-  ( ( ( A e. On_s /\ y e. No ) /\ ( bday ` y ) e. ( bday ` A ) ) -> ( y <_s ( ( ( _Left ` y ) u. ( _Right ` y ) ) |s (/) ) <-> -. ( ( ( _Left ` y ) u. ( _Right ` y ) ) |s (/) )
134 131 133 mpbid 
 |-  ( ( ( A e. On_s /\ y e. No ) /\ ( bday ` y ) e. ( bday ` A ) ) -> -. ( ( ( _Left ` y ) u. ( _Right ` y ) ) |s (/) )
135 breq1 
 |-  ( z = ( ( ( _Left ` y ) u. ( _Right ` y ) ) |s (/) ) -> ( z  ( ( ( _Left ` y ) u. ( _Right ` y ) ) |s (/) )
136 breq1 
 |-  ( z = ( ( ( _Left ` y ) u. ( _Right ` y ) ) |s (/) ) -> ( z  ( ( ( _Left ` y ) u. ( _Right ` y ) ) |s (/) )
137 136 notbid 
 |-  ( z = ( ( ( _Left ` y ) u. ( _Right ` y ) ) |s (/) ) -> ( -. z  -. ( ( ( _Left ` y ) u. ( _Right ` y ) ) |s (/) )
138 135 137 anbi12d 
 |-  ( z = ( ( ( _Left ` y ) u. ( _Right ` y ) ) |s (/) ) -> ( ( z  ( ( ( ( _Left ` y ) u. ( _Right ` y ) ) |s (/) )
139 138 rspcev 
 |-  ( ( ( ( ( _Left ` y ) u. ( _Right ` y ) ) |s (/) ) e. On_s /\ ( ( ( ( _Left ` y ) u. ( _Right ` y ) ) |s (/) )  E. z e. On_s ( z
140 41 88 134 139 syl12anc 
 |-  ( ( ( A e. On_s /\ y e. No ) /\ ( bday ` y ) e. ( bday ` A ) ) -> E. z e. On_s ( z
141 140 ex 
 |-  ( ( A e. On_s /\ y e. No ) -> ( ( bday ` y ) e. ( bday ` A ) -> E. z e. On_s ( z
142 ontri1 
 |-  ( ( ( bday ` A ) e. On /\ ( bday ` y ) e. On ) -> ( ( bday ` A ) C_ ( bday ` y ) <-> -. ( bday ` y ) e. ( bday ` A ) ) )
143 71 51 142 mp2an 
 |-  ( ( bday ` A ) C_ ( bday ` y ) <-> -. ( bday ` y ) e. ( bday ` A ) )
144 143 con2bii 
 |-  ( ( bday ` y ) e. ( bday ` A ) <-> -. ( bday ` A ) C_ ( bday ` y ) )
145 rexanali 
 |-  ( E. z e. On_s ( z  -. A. z e. On_s ( z  z
146 141 144 145 3imtr3g 
 |-  ( ( A e. On_s /\ y e. No ) -> ( -. ( bday ` A ) C_ ( bday ` y ) -> -. A. z e. On_s ( z  z
147 146 con4d 
 |-  ( ( A e. On_s /\ y e. No ) -> ( A. z e. On_s ( z  z  ( bday ` A ) C_ ( bday ` y ) ) )
148 31 147 syl5 
 |-  ( ( A e. On_s /\ y e. No ) -> ( { x e. On_s | x  ( bday ` A ) C_ ( bday ` y ) ) )
149 148 adantrd 
 |-  ( ( A e. On_s /\ y e. No ) -> ( ( { x e. On_s | x  ( bday ` A ) C_ ( bday ` y ) ) )
150 149 ralrimiva 
 |-  ( A e. On_s -> A. y e. No ( ( { x e. On_s | x  ( bday ` A ) C_ ( bday ` y ) ) )
151 3 8 elpwd 
 |-  ( A e. On_s -> { x e. On_s | x
152 nulssgt 
 |-  ( { x e. On_s | x  { x e. On_s | x
153 151 152 syl 
 |-  ( A e. On_s -> { x e. On_s | x
154 eqscut2 
 |-  ( ( { x e. On_s | x  ( ( { x e. On_s | x  ( { x e. On_s | x  ( bday ` A ) C_ ( bday ` y ) ) ) ) )
155 153 1 154 syl2anc 
 |-  ( A e. On_s -> ( ( { x e. On_s | x  ( { x e. On_s | x  ( bday ` A ) C_ ( bday ` y ) ) ) ) )
156 19 22 150 155 mpbir3and 
 |-  ( A e. On_s -> ( { x e. On_s | x
157 156 eqcomd 
 |-  ( A e. On_s -> A = ( { x e. On_s | x