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 99 uniexd A V bday A V
101 100 adantl A No A V bday A V
102 simpl y dom u v A ¬ v < s u u suc y = v suc y y dom u
103 102 reximi u A y dom u v A ¬ v < s u u suc y = v suc y u A y dom u
104 103 ss2abi y | u A y dom u v A ¬ v < s u u suc y = v suc y y | u A y dom u
105 bdayval u No bday u = dom u
106 27 105 syl A No u A bday u = dom u
107 fofn bday : No onto On bday Fn No
108 95 107 ax-mp bday Fn No
109 fnfvima bday Fn No A No u A bday u bday A
110 108 109 mp3an1 A No u A bday u bday A
111 106 110 eqeltrrd A No u A dom u bday A
112 elssuni dom u bday A dom u bday A
113 111 112 syl A No u A dom u bday A
114 113 sseld A No u A y dom u y bday A
115 114 rexlimdva A No u A y dom u y bday A
116 115 abssdv A No y | u A y dom u bday A
117 116 adantr A No A V y | u A y dom u bday A
118 104 117 sstrid A No A V y | u A y dom u v A ¬ v < s u u suc y = v suc y bday A
119 101 118 ssexd A No A V y | u A y dom u v A ¬ v < s u u suc y = v suc y V
120 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
121 119 120 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
122 94 121 mpbird A No A V y | u A y dom u v A ¬ v < s u u suc y = v suc y On
123 26 122 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
124 123 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
125 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
126 vex g V
127 eleq1w y = g y dom u g dom u
128 suceq y = g suc y = suc g
129 128 reseq2d y = g u suc y = u suc g
130 128 reseq2d y = g v suc y = v suc g
131 129 130 eqeq12d y = g u suc y = v suc y u suc g = v suc g
132 131 imbi2d y = g ¬ v < s u u suc y = v suc y ¬ v < s u u suc g = v suc g
133 132 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
134 127 133 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
135 134 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
136 126 135 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
137 eqid u g = u g
138 fvex u g V
139 eqeq2 x = u g u g = x u g = u g
140 139 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
141 138 140 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
142 137 141 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
143 142 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
144 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
145 143 144 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
146 145 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
147 nosupprefixmo A No * x u A g dom u v A ¬ v < s u u suc g = v suc g u g = x
148 147 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
149 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
150 146 148 149 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
151 vex z V
152 eqeq2 x = z u g = x u g = z
153 152 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
154 153 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
155 154 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
156 151 155 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
157 150 156 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
158 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
159 157 158 bitrdi 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
160 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
161 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
162 norn u No ran u 1 𝑜 2 𝑜
163 161 162 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 𝑜
164 nofun u No Fun u
165 161 164 syl A No u A g dom u v A ¬ v < s u u suc g = v suc g u g = z Fun u
166 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
167 fvelrn Fun u g dom u u g ran u
168 165 166 167 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
169 163 168 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 𝑜
170 160 169 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 𝑜
171 170 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 𝑜
172 171 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 𝑜
173 159 172 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 𝑜
174 136 173 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 𝑜
175 174 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 𝑜
176 175 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 𝑜
177 125 176 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 𝑜
178 177 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 𝑜
179 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 𝑜
180 23 124 178 179 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
181 21 180 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
182 19 181 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
183 1 182 eqeltrid A No A V S No
184 2 183 sylan2 A No A V S No