Metamath Proof Explorer


Theorem noinfbnd2lem1

Description: Bounding law from below when a set of surreals has a minimum. (Contributed by Scott Fenton, 9-Aug-2024)

Ref Expression
Assertion noinfbnd2lem1 U B y B ¬ y < s U B No B V Z No b B Z < s b ¬ U dom U 1 𝑜 < s Z suc dom U

Proof

Step Hyp Ref Expression
1 breq2 b = U Z < s b Z < s U
2 simp3 U B y B ¬ y < s U B No B V Z No b B Z < s b b B Z < s b
3 simp1l U B y B ¬ y < s U B No B V Z No b B Z < s b U B
4 1 2 3 rspcdva U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U
5 simpl21 U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U B No
6 simpl1l U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U U B
7 5 6 sseldd U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U U No
8 nodmon U No dom U On
9 7 8 syl U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U dom U On
10 onelon dom U On x On | U x Z x dom U x On | U x Z x On
11 9 10 sylan U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x dom U x On | U x Z x On
12 simpr U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x dom U q x On | U x Z x q x On | U x Z x
13 simplr U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x dom U q x On | U x Z x x On | U x Z x dom U
14 9 adantr U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x dom U dom U On
15 14 adantr U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x dom U q x On | U x Z x dom U On
16 ontr1 dom U On q x On | U x Z x x On | U x Z x dom U q dom U
17 15 16 syl U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x dom U q x On | U x Z x q x On | U x Z x x On | U x Z x dom U q dom U
18 12 13 17 mp2and U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x dom U q x On | U x Z x q dom U
19 18 fvresd U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x dom U q x On | U x Z x Z dom U q = Z q
20 onelon x On | U x Z x On q x On | U x Z x q On
21 11 20 sylan U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x dom U q x On | U x Z x q On
22 fveq2 x = q U x = U q
23 fveq2 x = q Z x = Z q
24 22 23 neeq12d x = q U x Z x U q Z q
25 24 onnminsb q On q x On | U x Z x ¬ U q Z q
26 21 12 25 sylc U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x dom U q x On | U x Z x ¬ U q Z q
27 df-ne U q Z q ¬ U q = Z q
28 27 con2bii U q = Z q ¬ U q Z q
29 26 28 sylibr U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x dom U q x On | U x Z x U q = Z q
30 19 29 eqtr4d U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x dom U q x On | U x Z x Z dom U q = U q
31 30 ralrimiva U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x dom U q x On | U x Z x Z dom U q = U q
32 simpr U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x dom U x On | U x Z x dom U
33 32 fvresd U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x dom U Z dom U x On | U x Z x = Z x On | U x Z x
34 simplr U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x dom U Z < s U
35 simpl23 U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U Z No
36 7 adantr U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x dom U U No
37 sltval2 Z No U No Z < s U Z x On | Z x U x 1 𝑜 1 𝑜 2 𝑜 2 𝑜 U x On | Z x U x
38 35 36 37 syl2an2r U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x dom U Z < s U Z x On | Z x U x 1 𝑜 1 𝑜 2 𝑜 2 𝑜 U x On | Z x U x
39 34 38 mpbid U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x dom U Z x On | Z x U x 1 𝑜 1 𝑜 2 𝑜 2 𝑜 U x On | Z x U x
40 necom U x Z x Z x U x
41 40 rabbii x On | U x Z x = x On | Z x U x
42 41 inteqi x On | U x Z x = x On | Z x U x
43 42 fveq2i Z x On | U x Z x = Z x On | Z x U x
44 42 fveq2i U x On | U x Z x = U x On | Z x U x
45 39 43 44 3brtr4g U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x dom U Z x On | U x Z x 1 𝑜 1 𝑜 2 𝑜 2 𝑜 U x On | U x Z x
46 33 45 eqbrtrd U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x dom U Z dom U x On | U x Z x 1 𝑜 1 𝑜 2 𝑜 2 𝑜 U x On | U x Z x
47 raleq p = x On | U x Z x q p Z dom U q = U q q x On | U x Z x Z dom U q = U q
48 fveq2 p = x On | U x Z x Z dom U p = Z dom U x On | U x Z x
49 fveq2 p = x On | U x Z x U p = U x On | U x Z x
50 48 49 breq12d p = x On | U x Z x Z dom U p 1 𝑜 1 𝑜 2 𝑜 2 𝑜 U p Z dom U x On | U x Z x 1 𝑜 1 𝑜 2 𝑜 2 𝑜 U x On | U x Z x
51 47 50 anbi12d p = x On | U x Z x q p Z dom U q = U q Z dom U p 1 𝑜 1 𝑜 2 𝑜 2 𝑜 U p q x On | U x Z x Z dom U q = U q Z dom U x On | U x Z x 1 𝑜 1 𝑜 2 𝑜 2 𝑜 U x On | U x Z x
52 51 rspcev x On | U x Z x On q x On | U x Z x Z dom U q = U q Z dom U x On | U x Z x 1 𝑜 1 𝑜 2 𝑜 2 𝑜 U x On | U x Z x p On q p Z dom U q = U q Z dom U p 1 𝑜 1 𝑜 2 𝑜 2 𝑜 U p
53 11 31 46 52 syl12anc U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x dom U p On q p Z dom U q = U q Z dom U p 1 𝑜 1 𝑜 2 𝑜 2 𝑜 U p
54 noreson Z No dom U On Z dom U No
55 35 9 54 syl2anc U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U Z dom U No
56 sltval Z dom U No U No Z dom U < s U p On q p Z dom U q = U q Z dom U p 1 𝑜 1 𝑜 2 𝑜 2 𝑜 U p
57 55 36 56 syl2an2r U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x dom U Z dom U < s U p On q p Z dom U q = U q Z dom U p 1 𝑜 1 𝑜 2 𝑜 2 𝑜 U p
58 53 57 mpbird U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x dom U Z dom U < s U
59 sssucid dom U suc dom U
60 resabs1 dom U suc dom U Z suc dom U dom U = Z dom U
61 59 60 mp1i U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x dom U Z suc dom U dom U = Z dom U
62 resundir U dom U 1 𝑜 dom U = U dom U dom U 1 𝑜 dom U
63 nofun U No Fun U
64 7 63 syl U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U Fun U
65 funrel Fun U Rel U
66 64 65 syl U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U Rel U
67 66 adantr U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x dom U Rel U
68 resdm Rel U U dom U = U
69 67 68 syl U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x dom U U dom U = U
70 nodmord U No Ord dom U
71 7 70 syl U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U Ord dom U
72 71 adantr U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x dom U Ord dom U
73 ordirr Ord dom U ¬ dom U dom U
74 72 73 syl U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x dom U ¬ dom U dom U
75 1oex 1 𝑜 V
76 75 snres0 dom U 1 𝑜 dom U = ¬ dom U dom U
77 74 76 sylibr U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x dom U dom U 1 𝑜 dom U =
78 69 77 uneq12d U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x dom U U dom U dom U 1 𝑜 dom U = U
79 un0 U = U
80 78 79 eqtrdi U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x dom U U dom U dom U 1 𝑜 dom U = U
81 62 80 syl5eq U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x dom U U dom U 1 𝑜 dom U = U
82 58 61 81 3brtr4d U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x dom U Z suc dom U dom U < s U dom U 1 𝑜 dom U
83 sucelon dom U On suc dom U On
84 9 83 sylib U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U suc dom U On
85 noreson Z No suc dom U On Z suc dom U No
86 35 84 85 syl2anc U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U Z suc dom U No
87 86 adantr U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x dom U Z suc dom U No
88 75 prid1 1 𝑜 1 𝑜 2 𝑜
89 88 noextend U No U dom U 1 𝑜 No
90 7 89 syl U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U U dom U 1 𝑜 No
91 90 adantr U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x dom U U dom U 1 𝑜 No
92 sltres Z suc dom U No U dom U 1 𝑜 No dom U On Z suc dom U dom U < s U dom U 1 𝑜 dom U Z suc dom U < s U dom U 1 𝑜
93 87 91 14 92 syl3anc U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x dom U Z suc dom U dom U < s U dom U 1 𝑜 dom U Z suc dom U < s U dom U 1 𝑜
94 82 93 mpd U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x dom U Z suc dom U < s U dom U 1 𝑜
95 sltso < s Or No
96 soasym < s Or No Z suc dom U No U dom U 1 𝑜 No Z suc dom U < s U dom U 1 𝑜 ¬ U dom U 1 𝑜 < s Z suc dom U
97 95 96 mpan Z suc dom U No U dom U 1 𝑜 No Z suc dom U < s U dom U 1 𝑜 ¬ U dom U 1 𝑜 < s Z suc dom U
98 86 91 97 syl2an2r U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x dom U Z suc dom U < s U dom U 1 𝑜 ¬ U dom U 1 𝑜 < s Z suc dom U
99 94 98 mpd U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x dom U ¬ U dom U 1 𝑜 < s Z suc dom U
100 sonr < s Or No U dom U 1 𝑜 No ¬ U dom U 1 𝑜 < s U dom U 1 𝑜
101 95 90 100 sylancr U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U ¬ U dom U 1 𝑜 < s U dom U 1 𝑜
102 101 adantr U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x = dom U ¬ U dom U 1 𝑜 < s U dom U 1 𝑜
103 df-suc suc dom U = dom U dom U
104 103 reseq2i Z suc dom U = Z dom U dom U
105 resundi Z dom U dom U = Z dom U Z dom U
106 104 105 eqtri Z suc dom U = Z dom U Z dom U
107 dmres dom Z dom U = dom U dom Z
108 42 eqeq1i x On | U x Z x = dom U x On | Z x U x = dom U
109 108 biimpi x On | U x Z x = dom U x On | Z x U x = dom U
110 109 adantl U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x = dom U x On | Z x U x = dom U
111 35 adantr U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x = dom U Z No
112 7 adantr U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x = dom U U No
113 simp23 U B y B ¬ y < s U B No B V Z No b B Z < s b Z No
114 sonr < s Or No Z No ¬ Z < s Z
115 95 113 114 sylancr U B y B ¬ y < s U B No B V Z No b B Z < s b ¬ Z < s Z
116 breq2 U = Z Z < s U Z < s Z
117 116 notbid U = Z ¬ Z < s U ¬ Z < s Z
118 115 117 syl5ibrcom U B y B ¬ y < s U B No B V Z No b B Z < s b U = Z ¬ Z < s U
119 118 necon2ad U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U U Z
120 119 imp U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U U Z
121 120 necomd U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U Z U
122 121 adantr U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x = dom U Z U
123 nosepssdm Z No U No Z U x On | Z x U x dom Z
124 111 112 122 123 syl3anc U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x = dom U x On | Z x U x dom Z
125 110 124 eqsstrrd U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x = dom U dom U dom Z
126 df-ss dom U dom Z dom U dom Z = dom U
127 125 126 sylib U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x = dom U dom U dom Z = dom U
128 107 127 syl5eq U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x = dom U dom Z dom U = dom U
129 128 eleq2d U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x = dom U q dom Z dom U q dom U
130 simpr U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x = dom U q dom U q dom U
131 130 fvresd U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x = dom U q dom U Z dom U q = Z q
132 112 8 syl U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x = dom U dom U On
133 onelon dom U On q dom U q On
134 132 133 sylan U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x = dom U q dom U q On
135 simpr U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x = dom U x On | U x Z x = dom U
136 135 eleq2d U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x = dom U q x On | U x Z x q dom U
137 136 biimpar U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x = dom U q dom U q x On | U x Z x
138 134 137 25 sylc U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x = dom U q dom U ¬ U q Z q
139 nesym U q Z q ¬ Z q = U q
140 139 con2bii Z q = U q ¬ U q Z q
141 138 140 sylibr U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x = dom U q dom U Z q = U q
142 131 141 eqtrd U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x = dom U q dom U Z dom U q = U q
143 142 ex U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x = dom U q dom U Z dom U q = U q
144 129 143 sylbid U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x = dom U q dom Z dom U Z dom U q = U q
145 144 ralrimiv U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x = dom U q dom Z dom U Z dom U q = U q
146 nofun Z No Fun Z
147 111 146 syl U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x = dom U Fun Z
148 147 funresd U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x = dom U Fun Z dom U
149 64 adantr U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x = dom U Fun U
150 eqfunfv Fun Z dom U Fun U Z dom U = U dom Z dom U = dom U q dom Z dom U Z dom U q = U q
151 148 149 150 syl2anc U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x = dom U Z dom U = U dom Z dom U = dom U q dom Z dom U Z dom U q = U q
152 128 145 151 mpbir2and U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x = dom U Z dom U = U
153 35 146 syl U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U Fun Z
154 153 funfnd U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U Z Fn dom Z
155 112 70 syl U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x = dom U Ord dom U
156 155 73 syl U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x = dom U ¬ dom U dom U
157 ndmfv ¬ dom U dom U U dom U =
158 2on0 2 𝑜
159 158 necomi 2 𝑜
160 neeq1 U dom U = U dom U 2 𝑜 2 𝑜
161 159 160 mpbiri U dom U = U dom U 2 𝑜
162 161 neneqd U dom U = ¬ U dom U = 2 𝑜
163 157 162 syl ¬ dom U dom U ¬ U dom U = 2 𝑜
164 156 163 syl U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x = dom U ¬ U dom U = 2 𝑜
165 164 intnand U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x = dom U ¬ Z dom U = U dom U = 2 𝑜
166 simpr U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U Z < s U
167 35 7 37 syl2anc U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U Z < s U Z x On | Z x U x 1 𝑜 1 𝑜 2 𝑜 2 𝑜 U x On | Z x U x
168 166 167 mpbid U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U Z x On | Z x U x 1 𝑜 1 𝑜 2 𝑜 2 𝑜 U x On | Z x U x
169 168 adantr U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x = dom U Z x On | Z x U x 1 𝑜 1 𝑜 2 𝑜 2 𝑜 U x On | Z x U x
170 110 fveq2d U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x = dom U Z x On | Z x U x = Z dom U
171 110 fveq2d U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x = dom U U x On | Z x U x = U dom U
172 169 170 171 3brtr3d U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x = dom U Z dom U 1 𝑜 1 𝑜 2 𝑜 2 𝑜 U dom U
173 fvex Z dom U V
174 fvex U dom U V
175 173 174 brtp Z dom U 1 𝑜 1 𝑜 2 𝑜 2 𝑜 U dom U Z dom U = 1 𝑜 U dom U = Z dom U = 1 𝑜 U dom U = 2 𝑜 Z dom U = U dom U = 2 𝑜
176 172 175 sylib U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x = dom U Z dom U = 1 𝑜 U dom U = Z dom U = 1 𝑜 U dom U = 2 𝑜 Z dom U = U dom U = 2 𝑜
177 3orel3 ¬ Z dom U = U dom U = 2 𝑜 Z dom U = 1 𝑜 U dom U = Z dom U = 1 𝑜 U dom U = 2 𝑜 Z dom U = U dom U = 2 𝑜 Z dom U = 1 𝑜 U dom U = Z dom U = 1 𝑜 U dom U = 2 𝑜
178 165 176 177 sylc U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x = dom U Z dom U = 1 𝑜 U dom U = Z dom U = 1 𝑜 U dom U = 2 𝑜
179 andi Z dom U = 1 𝑜 U dom U = U dom U = 2 𝑜 Z dom U = 1 𝑜 U dom U = Z dom U = 1 𝑜 U dom U = 2 𝑜
180 178 179 sylibr U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x = dom U Z dom U = 1 𝑜 U dom U = U dom U = 2 𝑜
181 180 simpld U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x = dom U Z dom U = 1 𝑜
182 ndmfv ¬ dom U dom Z Z dom U =
183 1n0 1 𝑜
184 183 necomi 1 𝑜
185 neeq1 Z dom U = Z dom U 1 𝑜 1 𝑜
186 184 185 mpbiri Z dom U = Z dom U 1 𝑜
187 186 neneqd Z dom U = ¬ Z dom U = 1 𝑜
188 182 187 syl ¬ dom U dom Z ¬ Z dom U = 1 𝑜
189 188 con4i Z dom U = 1 𝑜 dom U dom Z
190 181 189 syl U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x = dom U dom U dom Z
191 fnressn Z Fn dom Z dom U dom Z Z dom U = dom U Z dom U
192 154 190 191 syl2an2r U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x = dom U Z dom U = dom U Z dom U
193 181 opeq2d U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x = dom U dom U Z dom U = dom U 1 𝑜
194 193 sneqd U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x = dom U dom U Z dom U = dom U 1 𝑜
195 192 194 eqtrd U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x = dom U Z dom U = dom U 1 𝑜
196 152 195 uneq12d U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x = dom U Z dom U Z dom U = U dom U 1 𝑜
197 106 196 syl5eq U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x = dom U Z suc dom U = U dom U 1 𝑜
198 197 breq2d U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x = dom U U dom U 1 𝑜 < s Z suc dom U U dom U 1 𝑜 < s U dom U 1 𝑜
199 102 198 mtbird U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x = dom U ¬ U dom U 1 𝑜 < s Z suc dom U
200 nosepssdm U No Z No U Z x On | U x Z x dom U
201 7 35 120 200 syl3anc U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x dom U
202 nosepon U No Z No U Z x On | U x Z x On
203 7 35 120 202 syl3anc U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x On
204 onsseleq x On | U x Z x On dom U On x On | U x Z x dom U x On | U x Z x dom U x On | U x Z x = dom U
205 203 9 204 syl2anc U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x dom U x On | U x Z x dom U x On | U x Z x = dom U
206 201 205 mpbid U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U x On | U x Z x dom U x On | U x Z x = dom U
207 99 199 206 mpjaodan U B y B ¬ y < s U B No B V Z No b B Z < s b Z < s U ¬ U dom U 1 𝑜 < s Z suc dom U
208 4 207 mpdan U B y B ¬ y < s U B No B V Z No b B Z < s b ¬ U dom U 1 𝑜 < s Z suc dom U