Metamath Proof Explorer


Theorem sltres

Description: If the restrictions of two surreals to a given ordinal obey surreal less than, then so do the two surreals themselves. (Contributed by Scott Fenton, 4-Sep-2011)

Ref Expression
Assertion sltres A No B No X On A X < s B X A < s B

Proof

Step Hyp Ref Expression
1 noreson A No X On A X No
2 1 3adant2 A No B No X On A X No
3 noreson B No X On B X No
4 3 3adant1 A No B No X On B X No
5 sltintdifex A X No B X No A X < s B X a On | A X a B X a V
6 onintrab a On | A X a B X a V a On | A X a B X a On
7 5 6 syl6ib A X No B X No A X < s B X a On | A X a B X a On
8 2 4 7 syl2anc A No B No X On A X < s B X a On | A X a B X a On
9 8 imp A No B No X On A X < s B X a On | A X a B X a On
10 simpl3 A No B No X On A X < s B X X On
11 sltval2 A X No B X No A X < s B X A X a On | A X a B X a 1 𝑜 1 𝑜 2 𝑜 2 𝑜 B X a On | A X a B X a
12 2 4 11 syl2anc A No B No X On A X < s B X A X a On | A X a B X a 1 𝑜 1 𝑜 2 𝑜 2 𝑜 B X a On | A X a B X a
13 fvex A X a On | A X a B X a V
14 fvex B X a On | A X a B X a V
15 13 14 brtp A X a On | A X a B X a 1 𝑜 1 𝑜 2 𝑜 2 𝑜 B X a On | A X a B X a A X a On | A X a B X a = 1 𝑜 B X a On | A X a B X a = A X a On | A X a B X a = 1 𝑜 B X a On | A X a B X a = 2 𝑜 A X a On | A X a B X a = B X a On | A X a B X a = 2 𝑜
16 1n0 1 𝑜
17 16 neii ¬ 1 𝑜 =
18 eqeq1 A X a On | A X a B X a = 1 𝑜 A X a On | A X a B X a = 1 𝑜 =
19 17 18 mtbiri A X a On | A X a B X a = 1 𝑜 ¬ A X a On | A X a B X a =
20 ndmfv ¬ a On | A X a B X a dom A X A X a On | A X a B X a =
21 19 20 nsyl2 A X a On | A X a B X a = 1 𝑜 a On | A X a B X a dom A X
22 21 adantr A X a On | A X a B X a = 1 𝑜 B X a On | A X a B X a = a On | A X a B X a dom A X
23 22 orcd A X a On | A X a B X a = 1 𝑜 B X a On | A X a B X a = a On | A X a B X a dom A X a On | A X a B X a dom B X
24 21 adantr A X a On | A X a B X a = 1 𝑜 B X a On | A X a B X a = 2 𝑜 a On | A X a B X a dom A X
25 24 orcd A X a On | A X a B X a = 1 𝑜 B X a On | A X a B X a = 2 𝑜 a On | A X a B X a dom A X a On | A X a B X a dom B X
26 2on 2 𝑜 On
27 26 elexi 2 𝑜 V
28 27 prid2 2 𝑜 1 𝑜 2 𝑜
29 28 nosgnn0i 2 𝑜
30 29 neii ¬ = 2 𝑜
31 eqeq1 B X a On | A X a B X a = 2 𝑜 B X a On | A X a B X a = 2 𝑜 =
32 eqcom 2 𝑜 = = 2 𝑜
33 31 32 bitrdi B X a On | A X a B X a = 2 𝑜 B X a On | A X a B X a = = 2 𝑜
34 30 33 mtbiri B X a On | A X a B X a = 2 𝑜 ¬ B X a On | A X a B X a =
35 ndmfv ¬ a On | A X a B X a dom B X B X a On | A X a B X a =
36 34 35 nsyl2 B X a On | A X a B X a = 2 𝑜 a On | A X a B X a dom B X
37 36 adantl A X a On | A X a B X a = B X a On | A X a B X a = 2 𝑜 a On | A X a B X a dom B X
38 37 olcd A X a On | A X a B X a = B X a On | A X a B X a = 2 𝑜 a On | A X a B X a dom A X a On | A X a B X a dom B X
39 23 25 38 3jaoi A X a On | A X a B X a = 1 𝑜 B X a On | A X a B X a = A X a On | A X a B X a = 1 𝑜 B X a On | A X a B X a = 2 𝑜 A X a On | A X a B X a = B X a On | A X a B X a = 2 𝑜 a On | A X a B X a dom A X a On | A X a B X a dom B X
40 15 39 sylbi A X a On | A X a B X a 1 𝑜 1 𝑜 2 𝑜 2 𝑜 B X a On | A X a B X a a On | A X a B X a dom A X a On | A X a B X a dom B X
41 12 40 syl6bi A No B No X On A X < s B X a On | A X a B X a dom A X a On | A X a B X a dom B X
42 41 imp A No B No X On A X < s B X a On | A X a B X a dom A X a On | A X a B X a dom B X
43 dmres dom A X = X dom A
44 43 elin2 a On | A X a B X a dom A X a On | A X a B X a X a On | A X a B X a dom A
45 44 simplbi a On | A X a B X a dom A X a On | A X a B X a X
46 dmres dom B X = X dom B
47 46 elin2 a On | A X a B X a dom B X a On | A X a B X a X a On | A X a B X a dom B
48 47 simplbi a On | A X a B X a dom B X a On | A X a B X a X
49 45 48 jaoi a On | A X a B X a dom A X a On | A X a B X a dom B X a On | A X a B X a X
50 42 49 syl A No B No X On A X < s B X a On | A X a B X a X
51 onelss X On a On | A X a B X a X a On | A X a B X a X
52 10 50 51 sylc A No B No X On A X < s B X a On | A X a B X a X
53 52 sselda A No B No X On A X < s B X y a On | A X a B X a y X
54 onelon a On | A X a B X a On y a On | A X a B X a y On
55 9 54 sylan A No B No X On A X < s B X y a On | A X a B X a y On
56 intss1 y a On | A X a B X a a On | A X a B X a y
57 ontri1 a On | A X a B X a On y On a On | A X a B X a y ¬ y a On | A X a B X a
58 56 57 syl5ib a On | A X a B X a On y On y a On | A X a B X a ¬ y a On | A X a B X a
59 58 con2d a On | A X a B X a On y On y a On | A X a B X a ¬ y a On | A X a B X a
60 9 59 sylan A No B No X On A X < s B X y On y a On | A X a B X a ¬ y a On | A X a B X a
61 60 impancom A No B No X On A X < s B X y a On | A X a B X a y On ¬ y a On | A X a B X a
62 55 61 mpd A No B No X On A X < s B X y a On | A X a B X a ¬ y a On | A X a B X a
63 fveq2 a = y A X a = A X y
64 fveq2 a = y B X a = B X y
65 63 64 neeq12d a = y A X a B X a A X y B X y
66 65 elrab y a On | A X a B X a y On A X y B X y
67 66 simplbi2 y On A X y B X y y a On | A X a B X a
68 67 con3d y On ¬ y a On | A X a B X a ¬ A X y B X y
69 55 62 68 sylc A No B No X On A X < s B X y a On | A X a B X a ¬ A X y B X y
70 df-ne A X y B X y ¬ A X y = B X y
71 70 con2bii A X y = B X y ¬ A X y B X y
72 69 71 sylibr A No B No X On A X < s B X y a On | A X a B X a A X y = B X y
73 fvres y X A X y = A y
74 fvres y X B X y = B y
75 73 74 eqeq12d y X A X y = B X y A y = B y
76 75 biimpd y X A X y = B X y A y = B y
77 53 72 76 sylc A No B No X On A X < s B X y a On | A X a B X a A y = B y
78 77 ralrimiva A No B No X On A X < s B X y a On | A X a B X a A y = B y
79 fvresval A X a On | A X a B X a = A a On | A X a B X a A X a On | A X a B X a =
80 79 ori ¬ A X a On | A X a B X a = A a On | A X a B X a A X a On | A X a B X a =
81 19 80 nsyl2 A X a On | A X a B X a = 1 𝑜 A X a On | A X a B X a = A a On | A X a B X a
82 81 eqcomd A X a On | A X a B X a = 1 𝑜 A a On | A X a B X a = A X a On | A X a B X a
83 eqeq2 A X a On | A X a B X a = 1 𝑜 A a On | A X a B X a = A X a On | A X a B X a A a On | A X a B X a = 1 𝑜
84 82 83 mpbid A X a On | A X a B X a = 1 𝑜 A a On | A X a B X a = 1 𝑜
85 84 adantr A X a On | A X a B X a = 1 𝑜 B X a On | A X a B X a = A a On | A X a B X a = 1 𝑜
86 85 a1i A No B No X On A X a On | A X a B X a = 1 𝑜 B X a On | A X a B X a = A a On | A X a B X a = 1 𝑜
87 21 ad2antrl A No B No X On A X a On | A X a B X a = 1 𝑜 B X a On | A X a B X a = a On | A X a B X a dom A X
88 87 45 syl A No B No X On A X a On | A X a B X a = 1 𝑜 B X a On | A X a B X a = a On | A X a B X a X
89 nofun B X No Fun B X
90 fvelrn Fun B X a On | A X a B X a dom B X B X a On | A X a B X a ran B X
91 90 ex Fun B X a On | A X a B X a dom B X B X a On | A X a B X a ran B X
92 89 91 syl B X No a On | A X a B X a dom B X B X a On | A X a B X a ran B X
93 norn B X No ran B X 1 𝑜 2 𝑜
94 93 sseld B X No B X a On | A X a B X a ran B X B X a On | A X a B X a 1 𝑜 2 𝑜
95 92 94 syld B X No a On | A X a B X a dom B X B X a On | A X a B X a 1 𝑜 2 𝑜
96 nosgnn0 ¬ 1 𝑜 2 𝑜
97 eleq1 B X a On | A X a B X a = B X a On | A X a B X a 1 𝑜 2 𝑜 1 𝑜 2 𝑜
98 96 97 mtbiri B X a On | A X a B X a = ¬ B X a On | A X a B X a 1 𝑜 2 𝑜
99 95 98 nsyli B X No B X a On | A X a B X a = ¬ a On | A X a B X a dom B X
100 4 99 syl A No B No X On B X a On | A X a B X a = ¬ a On | A X a B X a dom B X
101 100 imp A No B No X On B X a On | A X a B X a = ¬ a On | A X a B X a dom B X
102 101 adantrl A No B No X On A X a On | A X a B X a = 1 𝑜 B X a On | A X a B X a = ¬ a On | A X a B X a dom B X
103 47 simplbi2 a On | A X a B X a X a On | A X a B X a dom B a On | A X a B X a dom B X
104 103 con3d a On | A X a B X a X ¬ a On | A X a B X a dom B X ¬ a On | A X a B X a dom B
105 88 102 104 sylc A No B No X On A X a On | A X a B X a = 1 𝑜 B X a On | A X a B X a = ¬ a On | A X a B X a dom B
106 ndmfv ¬ a On | A X a B X a dom B B a On | A X a B X a =
107 105 106 syl A No B No X On A X a On | A X a B X a = 1 𝑜 B X a On | A X a B X a = B a On | A X a B X a =
108 107 ex A No B No X On A X a On | A X a B X a = 1 𝑜 B X a On | A X a B X a = B a On | A X a B X a =
109 86 108 jcad A No B No X On A X a On | A X a B X a = 1 𝑜 B X a On | A X a B X a = A a On | A X a B X a = 1 𝑜 B a On | A X a B X a =
110 fvresval B X a On | A X a B X a = B a On | A X a B X a B X a On | A X a B X a =
111 110 ori ¬ B X a On | A X a B X a = B a On | A X a B X a B X a On | A X a B X a =
112 34 111 nsyl2 B X a On | A X a B X a = 2 𝑜 B X a On | A X a B X a = B a On | A X a B X a
113 112 eqcomd B X a On | A X a B X a = 2 𝑜 B a On | A X a B X a = B X a On | A X a B X a
114 eqeq2 B X a On | A X a B X a = 2 𝑜 B a On | A X a B X a = B X a On | A X a B X a B a On | A X a B X a = 2 𝑜
115 113 114 mpbid B X a On | A X a B X a = 2 𝑜 B a On | A X a B X a = 2 𝑜
116 84 115 anim12i A X a On | A X a B X a = 1 𝑜 B X a On | A X a B X a = 2 𝑜 A a On | A X a B X a = 1 𝑜 B a On | A X a B X a = 2 𝑜
117 116 a1i A No B No X On A X a On | A X a B X a = 1 𝑜 B X a On | A X a B X a = 2 𝑜 A a On | A X a B X a = 1 𝑜 B a On | A X a B X a = 2 𝑜
118 36 ad2antll A No B No X On A X a On | A X a B X a = B X a On | A X a B X a = 2 𝑜 a On | A X a B X a dom B X
119 118 48 syl A No B No X On A X a On | A X a B X a = B X a On | A X a B X a = 2 𝑜 a On | A X a B X a X
120 nofun A X No Fun A X
121 fvelrn Fun A X a On | A X a B X a dom A X A X a On | A X a B X a ran A X
122 121 ex Fun A X a On | A X a B X a dom A X A X a On | A X a B X a ran A X
123 120 122 syl A X No a On | A X a B X a dom A X A X a On | A X a B X a ran A X
124 norn A X No ran A X 1 𝑜 2 𝑜
125 124 sseld A X No A X a On | A X a B X a ran A X A X a On | A X a B X a 1 𝑜 2 𝑜
126 123 125 syld A X No a On | A X a B X a dom A X A X a On | A X a B X a 1 𝑜 2 𝑜
127 eleq1 A X a On | A X a B X a = A X a On | A X a B X a 1 𝑜 2 𝑜 1 𝑜 2 𝑜
128 96 127 mtbiri A X a On | A X a B X a = ¬ A X a On | A X a B X a 1 𝑜 2 𝑜
129 126 128 nsyli A X No A X a On | A X a B X a = ¬ a On | A X a B X a dom A X
130 2 129 syl A No B No X On A X a On | A X a B X a = ¬ a On | A X a B X a dom A X
131 130 imp A No B No X On A X a On | A X a B X a = ¬ a On | A X a B X a dom A X
132 131 adantrr A No B No X On A X a On | A X a B X a = B X a On | A X a B X a = 2 𝑜 ¬ a On | A X a B X a dom A X
133 44 simplbi2 a On | A X a B X a X a On | A X a B X a dom A a On | A X a B X a dom A X
134 133 con3d a On | A X a B X a X ¬ a On | A X a B X a dom A X ¬ a On | A X a B X a dom A
135 119 132 134 sylc A No B No X On A X a On | A X a B X a = B X a On | A X a B X a = 2 𝑜 ¬ a On | A X a B X a dom A
136 135 ex A No B No X On A X a On | A X a B X a = B X a On | A X a B X a = 2 𝑜 ¬ a On | A X a B X a dom A
137 ndmfv ¬ a On | A X a B X a dom A A a On | A X a B X a =
138 136 137 syl6 A No B No X On A X a On | A X a B X a = B X a On | A X a B X a = 2 𝑜 A a On | A X a B X a =
139 115 adantl A X a On | A X a B X a = B X a On | A X a B X a = 2 𝑜 B a On | A X a B X a = 2 𝑜
140 139 a1i A No B No X On A X a On | A X a B X a = B X a On | A X a B X a = 2 𝑜 B a On | A X a B X a = 2 𝑜
141 138 140 jcad A No B No X On A X a On | A X a B X a = B X a On | A X a B X a = 2 𝑜 A a On | A X a B X a = B a On | A X a B X a = 2 𝑜
142 109 117 141 3orim123d A No B No X On A X a On | A X a B X a = 1 𝑜 B X a On | A X a B X a = A X a On | A X a B X a = 1 𝑜 B X a On | A X a B X a = 2 𝑜 A X a On | A X a B X a = B X a On | A X a B X a = 2 𝑜 A a On | A X a B X a = 1 𝑜 B a On | A X a B X a = A a On | A X a B X a = 1 𝑜 B a On | A X a B X a = 2 𝑜 A a On | A X a B X a = B a On | A X a B X a = 2 𝑜
143 fvex A a On | A X a B X a V
144 fvex B a On | A X a B X a V
145 143 144 brtp A a On | A X a B X a 1 𝑜 1 𝑜 2 𝑜 2 𝑜 B a On | A X a B X a A a On | A X a B X a = 1 𝑜 B a On | A X a B X a = A a On | A X a B X a = 1 𝑜 B a On | A X a B X a = 2 𝑜 A a On | A X a B X a = B a On | A X a B X a = 2 𝑜
146 142 15 145 3imtr4g A No B No X On A X a On | A X a B X a 1 𝑜 1 𝑜 2 𝑜 2 𝑜 B X a On | A X a B X a A a On | A X a B X a 1 𝑜 1 𝑜 2 𝑜 2 𝑜 B a On | A X a B X a
147 12 146 sylbid A No B No X On A X < s B X A a On | A X a B X a 1 𝑜 1 𝑜 2 𝑜 2 𝑜 B a On | A X a B X a
148 147 imp A No B No X On A X < s B X A a On | A X a B X a 1 𝑜 1 𝑜 2 𝑜 2 𝑜 B a On | A X a B X a
149 raleq x = a On | A X a B X a y x A y = B y y a On | A X a B X a A y = B y
150 fveq2 x = a On | A X a B X a A x = A a On | A X a B X a
151 fveq2 x = a On | A X a B X a B x = B a On | A X a B X a
152 150 151 breq12d x = a On | A X a B X a A x 1 𝑜 1 𝑜 2 𝑜 2 𝑜 B x A a On | A X a B X a 1 𝑜 1 𝑜 2 𝑜 2 𝑜 B a On | A X a B X a
153 149 152 anbi12d x = a On | A X a B X a y x A y = B y A x 1 𝑜 1 𝑜 2 𝑜 2 𝑜 B x y a On | A X a B X a A y = B y A a On | A X a B X a 1 𝑜 1 𝑜 2 𝑜 2 𝑜 B a On | A X a B X a
154 153 rspcev a On | A X a B X a On y a On | A X a B X a A y = B y A a On | A X a B X a 1 𝑜 1 𝑜 2 𝑜 2 𝑜 B a On | A X a B X a x On y x A y = B y A x 1 𝑜 1 𝑜 2 𝑜 2 𝑜 B x
155 9 78 148 154 syl12anc A No B No X On A X < s B X x On y x A y = B y A x 1 𝑜 1 𝑜 2 𝑜 2 𝑜 B x
156 sltval A No B No A < s B x On y x A y = B y A x 1 𝑜 1 𝑜 2 𝑜 2 𝑜 B x
157 156 3adant3 A No B No X On A < s B x On y x A y = B y A x 1 𝑜 1 𝑜 2 𝑜 2 𝑜 B x
158 157 adantr A No B No X On A X < s B X A < s B x On y x A y = B y A x 1 𝑜 1 𝑜 2 𝑜 2 𝑜 B x
159 155 158 mpbird A No B No X On A X < s B X A < s B
160 159 ex A No B No X On A X < s B X A < s B