Metamath Proof Explorer


Theorem noinfbnd2

Description: Bounding law from below for the surreal infimum. Analagous to proposition 4.3 of Lipparini p. 6. (Contributed by Scott Fenton, 9-Aug-2024)

Ref Expression
Hypothesis noinfbnd2.1 T = if x B y B ¬ y < s x ι x B | y B ¬ y < s x dom ι x B | y B ¬ y < s x 1 𝑜 g y | u B y dom u v B ¬ u < s v u suc y = v suc y ι x | u B g dom u v B ¬ u < s v u suc g = v suc g u g = x
Assertion noinfbnd2 B No B V Z No b B Z < s b ¬ T < s Z dom T

Proof

Step Hyp Ref Expression
1 noinfbnd2.1 T = if x B y B ¬ y < s x ι x B | y B ¬ y < s x dom ι x B | y B ¬ y < s x 1 𝑜 g y | u B y dom u v B ¬ u < s v u suc y = v suc y ι x | u B g dom u v B ¬ u < s v u suc g = v suc g u g = x
2 nfv x B No B V Z No b B Z < s b
3 nfre1 x x B y B ¬ y < s x
4 nfriota1 _ x ι x B | y B ¬ y < s x
5 4 nfdm _ x dom ι x B | y B ¬ y < s x
6 nfcv _ x 1 𝑜
7 5 6 nfop _ x dom ι x B | y B ¬ y < s x 1 𝑜
8 7 nfsn _ x dom ι x B | y B ¬ y < s x 1 𝑜
9 4 8 nfun _ x ι x B | y B ¬ y < s x dom ι x B | y B ¬ y < s x 1 𝑜
10 nfcv _ x y | u B y dom u v B ¬ u < s v u suc y = v suc y
11 nfiota1 _ x ι x | u B g dom u v B ¬ u < s v u suc g = v suc g u g = x
12 10 11 nfmpt _ x g y | u B y dom u v B ¬ u < s v u suc y = v suc y ι x | u B g dom u v B ¬ u < s v u suc g = v suc g u g = x
13 3 9 12 nfif _ x if x B y B ¬ y < s x ι x B | y B ¬ y < s x dom ι x B | y B ¬ y < s x 1 𝑜 g y | u B y dom u v B ¬ u < s v u suc y = v suc y ι x | u B g dom u v B ¬ u < s v u suc g = v suc g u g = x
14 1 13 nfcxfr _ x T
15 nfcv _ x < s
16 nfcv _ x Z
17 14 nfdm _ x dom T
18 16 17 nfres _ x Z dom T
19 14 15 18 nfbr x T < s Z dom T
20 19 nfn x ¬ T < s Z dom T
21 2 20 nfim x B No B V Z No b B Z < s b ¬ T < s Z dom T
22 noinfbnd2lem1 x B y B ¬ y < s x B No B V Z No b B Z < s b ¬ x dom x 1 𝑜 < s Z suc dom x
23 22 3expb x B y B ¬ y < s x B No B V Z No b B Z < s b ¬ x dom x 1 𝑜 < s Z suc dom x
24 rspe x B y B ¬ y < s x x B y B ¬ y < s x
25 24 adantr x B y B ¬ y < s x B No B V Z No b B Z < s b x B y B ¬ y < s x
26 25 iftrued x B y B ¬ y < s x B No B V Z No b B Z < s b if x B y B ¬ y < s x ι x B | y B ¬ y < s x dom ι x B | y B ¬ y < s x 1 𝑜 g y | u B y dom u v B ¬ u < s v u suc y = v suc y ι x | u B g dom u v B ¬ u < s v u suc g = v suc g u g = x = ι x B | y B ¬ y < s x dom ι x B | y B ¬ y < s x 1 𝑜
27 simpl x B y B ¬ y < s x B No B V Z No b B Z < s b x B y B ¬ y < s x
28 simprl1 x B y B ¬ y < s x B No B V Z No b B Z < s b B No
29 nominmo B No * x B y B ¬ y < s x
30 28 29 syl x B y B ¬ y < s x B No B V Z No b B Z < s b * x B y B ¬ y < s x
31 reu5 ∃! x B y B ¬ y < s x x B y B ¬ y < s x * x B y B ¬ y < s x
32 25 30 31 sylanbrc x B y B ¬ y < s x B No B V Z No b B Z < s b ∃! x B y B ¬ y < s x
33 riota1 ∃! x B y B ¬ y < s x x B y B ¬ y < s x ι x B | y B ¬ y < s x = x
34 32 33 syl x B y B ¬ y < s x B No B V Z No b B Z < s b x B y B ¬ y < s x ι x B | y B ¬ y < s x = x
35 27 34 mpbid x B y B ¬ y < s x B No B V Z No b B Z < s b ι x B | y B ¬ y < s x = x
36 35 dmeqd x B y B ¬ y < s x B No B V Z No b B Z < s b dom ι x B | y B ¬ y < s x = dom x
37 36 opeq1d x B y B ¬ y < s x B No B V Z No b B Z < s b dom ι x B | y B ¬ y < s x 1 𝑜 = dom x 1 𝑜
38 37 sneqd x B y B ¬ y < s x B No B V Z No b B Z < s b dom ι x B | y B ¬ y < s x 1 𝑜 = dom x 1 𝑜
39 35 38 uneq12d x B y B ¬ y < s x B No B V Z No b B Z < s b ι x B | y B ¬ y < s x dom ι x B | y B ¬ y < s x 1 𝑜 = x dom x 1 𝑜
40 26 39 eqtrd x B y B ¬ y < s x B No B V Z No b B Z < s b if x B y B ¬ y < s x ι x B | y B ¬ y < s x dom ι x B | y B ¬ y < s x 1 𝑜 g y | u B y dom u v B ¬ u < s v u suc y = v suc y ι x | u B g dom u v B ¬ u < s v u suc g = v suc g u g = x = x dom x 1 𝑜
41 1 40 syl5eq x B y B ¬ y < s x B No B V Z No b B Z < s b T = x dom x 1 𝑜
42 41 dmeqd x B y B ¬ y < s x B No B V Z No b B Z < s b dom T = dom x dom x 1 𝑜
43 1oex 1 𝑜 V
44 43 dmsnop dom dom x 1 𝑜 = dom x
45 44 uneq2i dom x dom dom x 1 𝑜 = dom x dom x
46 dmun dom x dom x 1 𝑜 = dom x dom dom x 1 𝑜
47 df-suc suc dom x = dom x dom x
48 45 46 47 3eqtr4ri suc dom x = dom x dom x 1 𝑜
49 42 48 eqtr4di x B y B ¬ y < s x B No B V Z No b B Z < s b dom T = suc dom x
50 49 reseq2d x B y B ¬ y < s x B No B V Z No b B Z < s b Z dom T = Z suc dom x
51 41 50 breq12d x B y B ¬ y < s x B No B V Z No b B Z < s b T < s Z dom T x dom x 1 𝑜 < s Z suc dom x
52 23 51 mtbird x B y B ¬ y < s x B No B V Z No b B Z < s b ¬ T < s Z dom T
53 52 exp31 x B y B ¬ y < s x B No B V Z No b B Z < s b ¬ T < s Z dom T
54 21 53 rexlimi x B y B ¬ y < s x B No B V Z No b B Z < s b ¬ T < s Z dom T
55 54 imp x B y B ¬ y < s x B No B V Z No b B Z < s b ¬ T < s Z dom T
56 simprl3 ¬ x B y B ¬ y < s x B No B V Z No b B Z < s b Z No
57 1 noinfno B No B V T No
58 57 3adant3 B No B V Z No T No
59 58 ad2antrl ¬ x B y B ¬ y < s x B No B V Z No b B Z < s b T No
60 nodmon T No dom T On
61 59 60 syl ¬ x B y B ¬ y < s x B No B V Z No b B Z < s b dom T On
62 noreson Z No dom T On Z dom T No
63 56 61 62 syl2anc ¬ x B y B ¬ y < s x B No B V Z No b B Z < s b Z dom T No
64 nofun T No Fun T
65 funrel Fun T Rel T
66 58 64 65 3syl B No B V Z No Rel T
67 66 ad2antrl ¬ x B y B ¬ y < s x B No B V Z No b B Z < s b Rel T
68 resdm Rel T T dom T = T
69 67 68 syl ¬ x B y B ¬ y < s x B No B V Z No b B Z < s b T dom T = T
70 69 59 eqeltrd ¬ x B y B ¬ y < s x B No B V Z No b B Z < s b T dom T No
71 resdmss dom Z dom T dom T
72 71 a1i ¬ x B y B ¬ y < s x B No B V Z No b B Z < s b dom Z dom T dom T
73 resdmss dom T dom T dom T
74 73 a1i ¬ x B y B ¬ y < s x B No B V Z No b B Z < s b dom T dom T dom T
75 1 noinfdm ¬ x B y B ¬ y < s x dom T = g | p B g dom p q B ¬ p < s q p suc g = q suc g
76 75 abeq2d ¬ x B y B ¬ y < s x g dom T p B g dom p q B ¬ p < s q p suc g = q suc g
77 76 adantr ¬ x B y B ¬ y < s x B No B V Z No b B Z < s b g dom T p B g dom p q B ¬ p < s q p suc g = q suc g
78 simpll ¬ x B y B ¬ y < s x B No B V Z No b B Z < s b p B g dom p q B ¬ p < s q p suc g = q suc g ¬ x B y B ¬ y < s x
79 simprl1 ¬ x B y B ¬ y < s x B No B V Z No b B Z < s b B No
80 79 adantr ¬ x B y B ¬ y < s x B No B V Z No b B Z < s b p B g dom p q B ¬ p < s q p suc g = q suc g B No
81 simprl2 ¬ x B y B ¬ y < s x B No B V Z No b B Z < s b B V
82 81 adantr ¬ x B y B ¬ y < s x B No B V Z No b B Z < s b p B g dom p q B ¬ p < s q p suc g = q suc g B V
83 simprl ¬ x B y B ¬ y < s x B No B V Z No b B Z < s b p B g dom p q B ¬ p < s q p suc g = q suc g p B
84 simprrl ¬ x B y B ¬ y < s x B No B V Z No b B Z < s b p B g dom p q B ¬ p < s q p suc g = q suc g g dom p
85 simprrr ¬ x B y B ¬ y < s x B No B V Z No b B Z < s b p B g dom p q B ¬ p < s q p suc g = q suc g q B ¬ p < s q p suc g = q suc g
86 breq2 q = v p < s q p < s v
87 86 notbid q = v ¬ p < s q ¬ p < s v
88 reseq1 q = v q suc g = v suc g
89 88 eqeq2d q = v p suc g = q suc g p suc g = v suc g
90 87 89 imbi12d q = v ¬ p < s q p suc g = q suc g ¬ p < s v p suc g = v suc g
91 90 cbvralvw q B ¬ p < s q p suc g = q suc g v B ¬ p < s v p suc g = v suc g
92 85 91 sylib ¬ x B y B ¬ y < s x B No B V Z No b B Z < s b p B g dom p q B ¬ p < s q p suc g = q suc g v B ¬ p < s v p suc g = v suc g
93 1 noinfres ¬ x B y B ¬ y < s x B No B V p B g dom p v B ¬ p < s v p suc g = v suc g T suc g = p suc g
94 78 80 82 83 84 92 93 syl123anc ¬ x B y B ¬ y < s x B No B V Z No b B Z < s b p B g dom p q B ¬ p < s q p suc g = q suc g T suc g = p suc g
95 breq2 b = p Z < s b Z < s p
96 simplrr ¬ x B y B ¬ y < s x B No B V Z No b B Z < s b p B g dom p q B ¬ p < s q p suc g = q suc g b B Z < s b
97 95 96 83 rspcdva ¬ x B y B ¬ y < s x B No B V Z No b B Z < s b p B g dom p q B ¬ p < s q p suc g = q suc g Z < s p
98 56 adantr ¬ x B y B ¬ y < s x B No B V Z No b B Z < s b p B g dom p q B ¬ p < s q p suc g = q suc g Z No
99 80 83 sseldd ¬ x B y B ¬ y < s x B No B V Z No b B Z < s b p B g dom p q B ¬ p < s q p suc g = q suc g p No
100 sltso < s Or No
101 soasym < s Or No Z No p No Z < s p ¬ p < s Z
102 100 101 mpan Z No p No Z < s p ¬ p < s Z
103 98 99 102 syl2anc ¬ x B y B ¬ y < s x B No B V Z No b B Z < s b p B g dom p q B ¬ p < s q p suc g = q suc g Z < s p ¬ p < s Z
104 97 103 mpd ¬ x B y B ¬ y < s x B No B V Z No b B Z < s b p B g dom p q B ¬ p < s q p suc g = q suc g ¬ p < s Z
105 nodmon p No dom p On
106 99 105 syl ¬ x B y B ¬ y < s x B No B V Z No b B Z < s b p B g dom p q B ¬ p < s q p suc g = q suc g dom p On
107 onelon dom p On g dom p g On
108 106 84 107 syl2anc ¬ x B y B ¬ y < s x B No B V Z No b B Z < s b p B g dom p q B ¬ p < s q p suc g = q suc g g On
109 sucelon g On suc g On
110 108 109 sylib ¬ x B y B ¬ y < s x B No B V Z No b B Z < s b p B g dom p q B ¬ p < s q p suc g = q suc g suc g On
111 sltres p No Z No suc g On p suc g < s Z suc g p < s Z
112 99 98 110 111 syl3anc ¬ x B y B ¬ y < s x B No B V Z No b B Z < s b p B g dom p q B ¬ p < s q p suc g = q suc g p suc g < s Z suc g p < s Z
113 104 112 mtod ¬ x B y B ¬ y < s x B No B V Z No b B Z < s b p B g dom p q B ¬ p < s q p suc g = q suc g ¬ p suc g < s Z suc g
114 94 113 eqnbrtrd ¬ x B y B ¬ y < s x B No B V Z No b B Z < s b p B g dom p q B ¬ p < s q p suc g = q suc g ¬ T suc g < s Z suc g
115 114 rexlimdvaa ¬ x B y B ¬ y < s x B No B V Z No b B Z < s b p B g dom p q B ¬ p < s q p suc g = q suc g ¬ T suc g < s Z suc g
116 77 115 sylbid ¬ x B y B ¬ y < s x B No B V Z No b B Z < s b g dom T ¬ T suc g < s Z suc g
117 116 imp ¬ x B y B ¬ y < s x B No B V Z No b B Z < s b g dom T ¬ T suc g < s Z suc g
118 nodmord T No Ord dom T
119 ordsucss Ord dom T g dom T suc g dom T
120 59 118 119 3syl ¬ x B y B ¬ y < s x B No B V Z No b B Z < s b g dom T suc g dom T
121 120 imp ¬ x B y B ¬ y < s x B No B V Z No b B Z < s b g dom T suc g dom T
122 121 resabs1d ¬ x B y B ¬ y < s x B No B V Z No b B Z < s b g dom T T dom T suc g = T suc g
123 121 resabs1d ¬ x B y B ¬ y < s x B No B V Z No b B Z < s b g dom T Z dom T suc g = Z suc g
124 122 123 breq12d ¬ x B y B ¬ y < s x B No B V Z No b B Z < s b g dom T T dom T suc g < s Z dom T suc g T suc g < s Z suc g
125 117 124 mtbird ¬ x B y B ¬ y < s x B No B V Z No b B Z < s b g dom T ¬ T dom T suc g < s Z dom T suc g
126 125 ralrimiva ¬ x B y B ¬ y < s x B No B V Z No b B Z < s b g dom T ¬ T dom T suc g < s Z dom T suc g
127 noresle Z dom T No T dom T No dom Z dom T dom T dom T dom T dom T g dom T ¬ T dom T suc g < s Z dom T suc g ¬ T dom T < s Z dom T
128 63 70 72 74 126 127 syl23anc ¬ x B y B ¬ y < s x B No B V Z No b B Z < s b ¬ T dom T < s Z dom T
129 69 breq1d ¬ x B y B ¬ y < s x B No B V Z No b B Z < s b T dom T < s Z dom T T < s Z dom T
130 128 129 mtbid ¬ x B y B ¬ y < s x B No B V Z No b B Z < s b ¬ T < s Z dom T
131 55 130 pm2.61ian B No B V Z No b B Z < s b ¬ T < s Z dom T
132 simplr B No B V Z No ¬ T < s Z dom T b B ¬ T < s Z dom T
133 simpll1 B No B V Z No ¬ T < s Z dom T b B B No
134 simpll2 B No B V Z No ¬ T < s Z dom T b B B V
135 simpr B No B V Z No ¬ T < s Z dom T b B b B
136 1 noinfbnd1 B No B V b B T < s b dom T
137 133 134 135 136 syl3anc B No B V Z No ¬ T < s Z dom T b B T < s b dom T
138 simpl3 B No B V Z No ¬ T < s Z dom T Z No
139 simpl1 B No B V Z No ¬ T < s Z dom T B No
140 simpl2 B No B V Z No ¬ T < s Z dom T B V
141 139 140 57 syl2anc B No B V Z No ¬ T < s Z dom T T No
142 141 60 syl B No B V Z No ¬ T < s Z dom T dom T On
143 138 142 62 syl2anc B No B V Z No ¬ T < s Z dom T Z dom T No
144 143 adantr B No B V Z No ¬ T < s Z dom T b B Z dom T No
145 141 adantr B No B V Z No ¬ T < s Z dom T b B T No
146 139 sselda B No B V Z No ¬ T < s Z dom T b B b No
147 142 adantr B No B V Z No ¬ T < s Z dom T b B dom T On
148 noreson b No dom T On b dom T No
149 146 147 148 syl2anc B No B V Z No ¬ T < s Z dom T b B b dom T No
150 sotr2 < s Or No Z dom T No T No b dom T No ¬ T < s Z dom T T < s b dom T Z dom T < s b dom T
151 100 150 mpan Z dom T No T No b dom T No ¬ T < s Z dom T T < s b dom T Z dom T < s b dom T
152 144 145 149 151 syl3anc B No B V Z No ¬ T < s Z dom T b B ¬ T < s Z dom T T < s b dom T Z dom T < s b dom T
153 132 137 152 mp2and B No B V Z No ¬ T < s Z dom T b B Z dom T < s b dom T
154 simpll3 B No B V Z No ¬ T < s Z dom T b B Z No
155 sltres Z No b No dom T On Z dom T < s b dom T Z < s b
156 154 146 147 155 syl3anc B No B V Z No ¬ T < s Z dom T b B Z dom T < s b dom T Z < s b
157 153 156 mpd B No B V Z No ¬ T < s Z dom T b B Z < s b
158 157 ralrimiva B No B V Z No ¬ T < s Z dom T b B Z < s b
159 131 158 impbida B No B V Z No b B Z < s b ¬ T < s Z dom T