Metamath Proof Explorer


Theorem nosupno

Description: The next several theorems deal with a surreal "supremum". This surreal will ultimately be shown to bound A below and bound the restriction of any surreal above. We begin by showing that the given expression actually defines a surreal number. (Contributed by Scott Fenton, 5-Dec-2021)

Ref Expression
Hypothesis nosupno.1 S = if x A y A ¬ x < s y ι x A | y A ¬ x < s y dom ι x A | y A ¬ x < s y 2 𝑜 g y | u A y dom u v A ¬ v < s u u suc y = v suc y ι x | u A g dom u v A ¬ v < s u u suc g = v suc g u g = x
Assertion nosupno A No A V S No

Proof

Step Hyp Ref Expression
1 nosupno.1 S = if x A y A ¬ x < s y ι x A | y A ¬ x < s y dom ι x A | y A ¬ x < s y 2 𝑜 g y | u A y dom u v A ¬ v < s u u suc y = v suc y ι x | u A g dom u v A ¬ v < s u u suc g = v suc g u g = x
2 elex A V A V
3 iftrue x A y A ¬ x < s y if x A y A ¬ x < s y ι x A | y A ¬ x < s y dom ι x A | y A ¬ x < s y 2 𝑜 g y | u A y dom u v A ¬ v < s u u suc y = v suc y ι x | u A g dom u v A ¬ v < s u u suc g = v suc g u g = x = ι x A | y A ¬ x < s y dom ι x A | y A ¬ x < s y 2 𝑜
4 3 adantr x A y A ¬ x < s y A No A V if x A y A ¬ x < s y ι x A | y A ¬ x < s y dom ι x A | y A ¬ x < s y 2 𝑜 g y | u A y dom u v A ¬ v < s u u suc y = v suc y ι x | u A g dom u v A ¬ v < s u u suc g = v suc g u g = x = ι x A | y A ¬ x < s y dom ι x A | y A ¬ x < s y 2 𝑜
5 simprl x A y A ¬ x < s y A No A V A No
6 simpl x A y A ¬ x < s y A No A V x A y A ¬ x < s y
7 nomaxmo A No * x A y A ¬ x < s y
8 7 ad2antrl x A y A ¬ x < s y A No A V * x A y A ¬ x < s y
9 reu5 ∃! x A y A ¬ x < s y x A y A ¬ x < s y * x A y A ¬ x < s y
10 6 8 9 sylanbrc x A y A ¬ x < s y A No A V ∃! x A y A ¬ x < s y
11 riotacl ∃! x A y A ¬ x < s y ι x A | y A ¬ x < s y A
12 10 11 syl x A y A ¬ x < s y A No A V ι x A | y A ¬ x < s y A
13 5 12 sseldd x A y A ¬ x < s y A No A V ι x A | y A ¬ x < s y No
14 2on 2 𝑜 On
15 14 elexi 2 𝑜 V
16 15 prid2 2 𝑜 1 𝑜 2 𝑜
17 16 noextend ι x A | y A ¬ x < s y No ι x A | y A ¬ x < s y dom ι x A | y A ¬ x < s y 2 𝑜 No
18 13 17 syl x A y A ¬ x < s y A No A V ι x A | y A ¬ x < s y dom ι x A | y A ¬ x < s y 2 𝑜 No
19 4 18 eqeltrd x A y A ¬ x < s y A No A V if x A y A ¬ x < s y ι x A | y A ¬ x < s y dom ι x A | y A ¬ x < s y 2 𝑜 g y | u A y dom u v A ¬ v < s u u suc y = v suc y ι x | u A g dom u v A ¬ v < s u u suc g = v suc g u g = x No
20 iffalse ¬ x A y A ¬ x < s y if x A y A ¬ x < s y ι x A | y A ¬ x < s y dom ι x A | y A ¬ x < s y 2 𝑜 g y | u A y dom u v A ¬ v < s u u suc y = v suc y ι x | u A g dom u v A ¬ v < s u u suc g = v suc g u g = x = g y | u A y dom u v A ¬ v < s u u suc y = v suc y ι x | u A g dom u v A ¬ v < s u u suc g = v suc g u g = x
21 20 adantr ¬ x A y A ¬ x < s y A No A V if x A y A ¬ x < s y ι x A | y A ¬ x < s y dom ι x A | y A ¬ x < s y 2 𝑜 g y | u A y dom u v A ¬ v < s u u suc y = v suc y ι x | u A g dom u v A ¬ v < s u u suc g = v suc g u g = x = g y | u A y dom u v A ¬ v < s u u suc y = v suc y ι x | u A g dom u v A ¬ v < s u u suc g = v suc g u g = x
22 funmpt Fun g y | u A y dom u v A ¬ v < s u u suc y = v suc y ι x | u A g dom u v A ¬ v < s u u suc g = v suc g u g = x
23 22 a1i ¬ x A y A ¬ x < s y A No A V Fun g y | u A y dom u v A ¬ v < s u u suc y = v suc y ι x | u A g dom u v A ¬ v < s u u suc g = v suc g u g = x
24 iotaex ι x | u A g dom u v A ¬ v < s u u suc g = v suc g u g = x V
25 eqid g y | u A y dom u v A ¬ v < s u u suc y = v suc y ι x | u A g dom u v A ¬ v < s u u suc g = v suc g u g = x = g y | u A y dom u v A ¬ v < s u u suc y = v suc y ι x | u A g dom u v A ¬ v < s u u suc g = v suc g u g = x
26 24 25 dmmpti dom g y | u A y dom u v A ¬ v < s u u suc y = v suc y ι x | u A g dom u v A ¬ v < s u u suc g = v suc g u g = x = y | u A y dom u v A ¬ v < s u u suc y = v suc y
27 ssel2 A No u A u No
28 nodmon u No dom u On
29 27 28 syl A No u A dom u On
30 onss dom u On dom u On
31 29 30 syl A No u A dom u On
32 31 sseld A No u A y dom u y On
33 32 adantrd A No u A y dom u v A ¬ v < s u u suc y = v suc y y On
34 33 rexlimdva A No u A y dom u v A ¬ v < s u u suc y = v suc y y On
35 34 abssdv A No y | u A y dom u v A ¬ v < s u u suc y = v suc y On
36 simplr A No a b u A a b
37 29 adantlr A No a b u A dom u On
38 ontr1 dom u On a b b dom u a dom u
39 37 38 syl A No a b u A a b b dom u a dom u
40 36 39 mpand A No a b u A b dom u a dom u
41 40 adantrd A No a b u A b dom u v A ¬ v < s u u suc b = v suc b a dom u
42 reseq1 u suc b = v suc b u suc b suc a = v suc b suc a
43 onelon dom u On b dom u b On
44 37 43 sylan A No a b u A b dom u b On
45 suceloni b On suc b On
46 44 45 syl A No a b u A b dom u suc b On
47 simpllr A No a b u A b dom u a b
48 eloni b On Ord b
49 44 48 syl A No a b u A b dom u Ord b
50 ordsucelsuc Ord b a b suc a suc b
51 49 50 syl A No a b u A b dom u a b suc a suc b
52 47 51 mpbid A No a b u A b dom u suc a suc b
53 onelss suc b On suc a suc b suc a suc b
54 46 52 53 sylc A No a b u A b dom u suc a suc b
55 54 resabs1d A No a b u A b dom u u suc b suc a = u suc a
56 54 resabs1d A No a b u A b dom u v suc b suc a = v suc a
57 55 56 eqeq12d A No a b u A b dom u u suc b suc a = v suc b suc a u suc a = v suc a
58 42 57 syl5ib A No a b u A b dom u u suc b = v suc b u suc a = v suc a
59 58 imim2d A No a b u A b dom u ¬ v < s u u suc b = v suc b ¬ v < s u u suc a = v suc a
60 59 ralimdv A No a b u A b dom u v A ¬ v < s u u suc b = v suc b v A ¬ v < s u u suc a = v suc a
61 60 expimpd A No a b u A b dom u v A ¬ v < s u u suc b = v suc b v A ¬ v < s u u suc a = v suc a
62 41 61 jcad A No a b u A b dom u v A ¬ v < s u u suc b = v suc b a dom u v A ¬ v < s u u suc a = v suc a
63 62 reximdva A No a b u A b dom u v A ¬ v < s u u suc b = v suc b u A a dom u v A ¬ v < s u u suc a = v suc a
64 63 expimpd A No a b u A b dom u v A ¬ v < s u u suc b = v suc b u A a dom u v A ¬ v < s u u suc a = v suc a
65 vex b V
66 eleq1w y = b y dom u b dom u
67 suceq y = b suc y = suc b
68 67 reseq2d y = b u suc y = u suc b
69 67 reseq2d y = b v suc y = v suc b
70 68 69 eqeq12d y = b u suc y = v suc y u suc b = v suc b
71 70 imbi2d y = b ¬ v < s u u suc y = v suc y ¬ v < s u u suc b = v suc b
72 71 ralbidv y = b v A ¬ v < s u u suc y = v suc y v A ¬ v < s u u suc b = v suc b
73 66 72 anbi12d y = b y dom u v A ¬ v < s u u suc y = v suc y b dom u v A ¬ v < s u u suc b = v suc b
74 73 rexbidv y = b u A y dom u v A ¬ v < s u u suc y = v suc y u A b dom u v A ¬ v < s u u suc b = v suc b
75 65 74 elab b y | u A y dom u v A ¬ v < s u u suc y = v suc y u A b dom u v A ¬ v < s u u suc b = v suc b
76 75 anbi2i a b b y | u A y dom u v A ¬ v < s u u suc y = v suc y a b u A b dom u v A ¬ v < s u u suc b = v suc b
77 vex a V
78 eleq1w y = a y dom u a dom u
79 suceq y = a suc y = suc a
80 79 reseq2d y = a u suc y = u suc a
81 79 reseq2d y = a v suc y = v suc a
82 80 81 eqeq12d y = a u suc y = v suc y u suc a = v suc a
83 82 imbi2d y = a ¬ v < s u u suc y = v suc y ¬ v < s u u suc a = v suc a
84 83 ralbidv y = a v A ¬ v < s u u suc y = v suc y v A ¬ v < s u u suc a = v suc a
85 78 84 anbi12d y = a y dom u v A ¬ v < s u u suc y = v suc y a dom u v A ¬ v < s u u suc a = v suc a
86 85 rexbidv y = a u A y dom u v A ¬ v < s u u suc y = v suc y u A a dom u v A ¬ v < s u u suc a = v suc a
87 77 86 elab a y | u A y dom u v A ¬ v < s u u suc y = v suc y u A a dom u v A ¬ v < s u u suc a = v suc a
88 64 76 87 3imtr4g A No a b b y | u A y dom u v A ¬ v < s u u suc y = v suc y a y | u A y dom u v A ¬ v < s u u suc y = v suc y
89 88 alrimivv A No a b a b b y | u A y dom u v A ¬ v < s u u suc y = v suc y a y | u A y dom u v A ¬ v < s u u suc y = v suc y
90 dftr2 Tr y | u A y dom u v A ¬ v < s u u suc y = v suc y a b a b b y | u A y dom u v A ¬ v < s u u suc y = v suc y a y | u A y dom u v A ¬ v < s u u suc y = v suc y
91 89 90 sylibr A No Tr y | u A y dom u v A ¬ v < s u u suc y = v suc y
92 dford5 Ord y | u A y dom u v A ¬ v < s u u suc y = v suc y y | u A y dom u v A ¬ v < s u u suc y = v suc y On Tr y | u A y dom u v A ¬ v < s u u suc y = v suc y
93 35 91 92 sylanbrc A No Ord y | u A y dom u v A ¬ v < s u u suc y = v suc y
94 93 adantr A No A V Ord y | u A y dom u v A ¬ v < s u u suc y = v suc y
95 bdayfo bday : No onto On
96 fofun bday : No onto On Fun bday
97 95 96 ax-mp Fun bday
98 funimaexg Fun bday A V bday A V
99 97 98 mpan A V bday A V
100 uniexg bday A V bday A V
101 99 100 syl A V bday A V
102 101 adantl A No A V bday A V
103 simpl y dom u v A ¬ v < s u u suc y = v suc y y dom u
104 103 reximi u A y dom u v A ¬ v < s u u suc y = v suc y u A y dom u
105 104 ss2abi y | u A y dom u v A ¬ v < s u u suc y = v suc y y | u A y dom u
106 bdayval u No bday u = dom u
107 27 106 syl A No u A bday u = dom u
108 fofn bday : No onto On bday Fn No
109 95 108 ax-mp bday Fn No
110 fnfvima bday Fn No A No u A bday u bday A
111 109 110 mp3an1 A No u A bday u bday A
112 107 111 eqeltrrd A No u A dom u bday A
113 elssuni dom u bday A dom u bday A
114 112 113 syl A No u A dom u bday A
115 114 sseld A No u A y dom u y bday A
116 115 rexlimdva A No u A y dom u y bday A
117 116 abssdv A No y | u A y dom u bday A
118 117 adantr A No A V y | u A y dom u bday A
119 105 118 sstrid A No A V y | u A y dom u v A ¬ v < s u u suc y = v suc y bday A
120 102 119 ssexd A No A V y | u A y dom u v A ¬ v < s u u suc y = v suc y V
121 elong y | u A y dom u v A ¬ v < s u u suc y = v suc y V y | u A y dom u v A ¬ v < s u u suc y = v suc y On Ord y | u A y dom u v A ¬ v < s u u suc y = v suc y
122 120 121 syl A No A V y | u A y dom u v A ¬ v < s u u suc y = v suc y On Ord y | u A y dom u v A ¬ v < s u u suc y = v suc y
123 94 122 mpbird A No A V y | u A y dom u v A ¬ v < s u u suc y = v suc y On
124 26 123 eqeltrid A No A V dom g y | u A y dom u v A ¬ v < s u u suc y = v suc y ι x | u A g dom u v A ¬ v < s u u suc g = v suc g u g = x On
125 124 adantl ¬ x A y A ¬ x < s y A No A V dom g y | u A y dom u v A ¬ v < s u u suc y = v suc y ι x | u A g dom u v A ¬ v < s u u suc g = v suc g u g = x On
126 25 rnmpt ran g y | u A y dom u v A ¬ v < s u u suc y = v suc y ι x | u A g dom u v A ¬ v < s u u suc g = v suc g u g = x = z | g y | u A y dom u v A ¬ v < s u u suc y = v suc y z = ι x | u A g dom u v A ¬ v < s u u suc g = v suc g u g = x
127 vex g V
128 eleq1w y = g y dom u g dom u
129 suceq y = g suc y = suc g
130 129 reseq2d y = g u suc y = u suc g
131 129 reseq2d y = g v suc y = v suc g
132 130 131 eqeq12d y = g u suc y = v suc y u suc g = v suc g
133 132 imbi2d y = g ¬ v < s u u suc y = v suc y ¬ v < s u u suc g = v suc g
134 133 ralbidv y = g v A ¬ v < s u u suc y = v suc y v A ¬ v < s u u suc g = v suc g
135 128 134 anbi12d y = g y dom u v A ¬ v < s u u suc y = v suc y g dom u v A ¬ v < s u u suc g = v suc g
136 135 rexbidv y = g u A y dom u v A ¬ v < s u u suc y = v suc y u A g dom u v A ¬ v < s u u suc g = v suc g
137 127 136 elab g y | u A y dom u v A ¬ v < s u u suc y = v suc y u A g dom u v A ¬ v < s u u suc g = v suc g
138 eqid u g = u g
139 fvex u g V
140 eqeq2 x = u g u g = x u g = u g
141 140 3anbi3d x = u g g dom u v A ¬ v < s u u suc g = v suc g u g = x g dom u v A ¬ v < s u u suc g = v suc g u g = u g
142 139 141 spcev g dom u v A ¬ v < s u u suc g = v suc g u g = u g x g dom u v A ¬ v < s u u suc g = v suc g u g = x
143 138 142 mp3an3 g dom u v A ¬ v < s u u suc g = v suc g x g dom u v A ¬ v < s u u suc g = v suc g u g = x
144 143 reximi u A g dom u v A ¬ v < s u u suc g = v suc g u A x g dom u v A ¬ v < s u u suc g = v suc g u g = x
145 rexcom4 u A x g dom u v A ¬ v < s u u suc g = v suc g u g = x x u A g dom u v A ¬ v < s u u suc g = v suc g u g = x
146 144 145 sylib u A g dom u v A ¬ v < s u u suc g = v suc g x u A g dom u v A ¬ v < s u u suc g = v suc g u g = x
147 146 adantl A No u A g dom u v A ¬ v < s u u suc g = v suc g x u A g dom u v A ¬ v < s u u suc g = v suc g u g = x
148 noprefixmo A No * x u A g dom u v A ¬ v < s u u suc g = v suc g u g = x
149 148 adantr A No u A g dom u v A ¬ v < s u u suc g = v suc g * x u A g dom u v A ¬ v < s u u suc g = v suc g u g = x
150 df-eu ∃! x u A g dom u v A ¬ v < s u u suc g = v suc g u g = x x u A g dom u v A ¬ v < s u u suc g = v suc g u g = x * x u A g dom u v A ¬ v < s u u suc g = v suc g u g = x
151 147 149 150 sylanbrc A No u A g dom u v A ¬ v < s u u suc g = v suc g ∃! x u A g dom u v A ¬ v < s u u suc g = v suc g u g = x
152 vex z V
153 eqeq2 x = z u g = x u g = z
154 153 3anbi3d x = z g dom u v A ¬ v < s u u suc g = v suc g u g = x g dom u v A ¬ v < s u u suc g = v suc g u g = z
155 154 rexbidv x = z u A g dom u v A ¬ v < s u u suc g = v suc g u g = x u A g dom u v A ¬ v < s u u suc g = v suc g u g = z
156 155 iota2 z V ∃! x u A g dom u v A ¬ v < s u u suc g = v suc g u g = x u A g dom u v A ¬ v < s u u suc g = v suc g u g = z ι x | u A g dom u v A ¬ v < s u u suc g = v suc g u g = x = z
157 152 156 mpan ∃! x u A g dom u v A ¬ v < s u u suc g = v suc g u g = x u A g dom u v A ¬ v < s u u suc g = v suc g u g = z ι x | u A g dom u v A ¬ v < s u u suc g = v suc g u g = x = z
158 151 157 syl A No u A g dom u v A ¬ v < s u u suc g = v suc g u A g dom u v A ¬ v < s u u suc g = v suc g u g = z ι x | u A g dom u v A ¬ v < s u u suc g = v suc g u g = x = z
159 eqcom ι x | u A g dom u v A ¬ v < s u u suc g = v suc g u g = x = z z = ι x | u A g dom u v A ¬ v < s u u suc g = v suc g u g = x
160 158 159 syl6bb A No u A g dom u v A ¬ v < s u u suc g = v suc g u A g dom u v A ¬ v < s u u suc g = v suc g u g = z z = ι x | u A g dom u v A ¬ v < s u u suc g = v suc g u g = x
161 simprr3 A No u A g dom u v A ¬ v < s u u suc g = v suc g u g = z u g = z
162 27 adantrr A No u A g dom u v A ¬ v < s u u suc g = v suc g u g = z u No
163 norn u No ran u 1 𝑜 2 𝑜
164 162 163 syl A No u A g dom u v A ¬ v < s u u suc g = v suc g u g = z ran u 1 𝑜 2 𝑜
165 nofun u No Fun u
166 162 165 syl A No u A g dom u v A ¬ v < s u u suc g = v suc g u g = z Fun u
167 simprr1 A No u A g dom u v A ¬ v < s u u suc g = v suc g u g = z g dom u
168 fvelrn Fun u g dom u u g ran u
169 166 167 168 syl2anc A No u A g dom u v A ¬ v < s u u suc g = v suc g u g = z u g ran u
170 164 169 sseldd A No u A g dom u v A ¬ v < s u u suc g = v suc g u g = z u g 1 𝑜 2 𝑜
171 161 170 eqeltrrd A No u A g dom u v A ¬ v < s u u suc g = v suc g u g = z z 1 𝑜 2 𝑜
172 171 rexlimdvaa A No u A g dom u v A ¬ v < s u u suc g = v suc g u g = z z 1 𝑜 2 𝑜
173 172 adantr A No u A g dom u v A ¬ v < s u u suc g = v suc g u A g dom u v A ¬ v < s u u suc g = v suc g u g = z z 1 𝑜 2 𝑜
174 160 173 sylbird A No u A g dom u v A ¬ v < s u u suc g = v suc g z = ι x | u A g dom u v A ¬ v < s u u suc g = v suc g u g = x z 1 𝑜 2 𝑜
175 137 174 sylan2b A No g y | u A y dom u v A ¬ v < s u u suc y = v suc y z = ι x | u A g dom u v A ¬ v < s u u suc g = v suc g u g = x z 1 𝑜 2 𝑜
176 175 rexlimdva A No g y | u A y dom u v A ¬ v < s u u suc y = v suc y z = ι x | u A g dom u v A ¬ v < s u u suc g = v suc g u g = x z 1 𝑜 2 𝑜
177 176 abssdv A No z | g y | u A y dom u v A ¬ v < s u u suc y = v suc y z = ι x | u A g dom u v A ¬ v < s u u suc g = v suc g u g = x 1 𝑜 2 𝑜
178 126 177 eqsstrid A No ran g y | u A y dom u v A ¬ v < s u u suc y = v suc y ι x | u A g dom u v A ¬ v < s u u suc g = v suc g u g = x 1 𝑜 2 𝑜
179 178 ad2antrl ¬ x A y A ¬ x < s y A No A V ran g y | u A y dom u v A ¬ v < s u u suc y = v suc y ι x | u A g dom u v A ¬ v < s u u suc g = v suc g u g = x 1 𝑜 2 𝑜
180 elno2 g y | u A y dom u v A ¬ v < s u u suc y = v suc y ι x | u A g dom u v A ¬ v < s u u suc g = v suc g u g = x No Fun g y | u A y dom u v A ¬ v < s u u suc y = v suc y ι x | u A g dom u v A ¬ v < s u u suc g = v suc g u g = x dom g y | u A y dom u v A ¬ v < s u u suc y = v suc y ι x | u A g dom u v A ¬ v < s u u suc g = v suc g u g = x On ran g y | u A y dom u v A ¬ v < s u u suc y = v suc y ι x | u A g dom u v A ¬ v < s u u suc g = v suc g u g = x 1 𝑜 2 𝑜
181 23 125 179 180 syl3anbrc ¬ x A y A ¬ x < s y A No A V g y | u A y dom u v A ¬ v < s u u suc y = v suc y ι x | u A g dom u v A ¬ v < s u u suc g = v suc g u g = x No
182 21 181 eqeltrd ¬ x A y A ¬ x < s y A No A V if x A y A ¬ x < s y ι x A | y A ¬ x < s y dom ι x A | y A ¬ x < s y 2 𝑜 g y | u A y dom u v A ¬ v < s u u suc y = v suc y ι x | u A g dom u v A ¬ v < s u u suc g = v suc g u g = x No
183 19 182 pm2.61ian A No A V if x A y A ¬ x < s y ι x A | y A ¬ x < s y dom ι x A | y A ¬ x < s y 2 𝑜 g y | u A y dom u v A ¬ v < s u u suc y = v suc y ι x | u A g dom u v A ¬ v < s u u suc g = v suc g u g = x No
184 1 183 eqeltrid A No A V S No
185 2 184 sylan2 A No A V S No