Metamath Proof Explorer


Theorem noresle

Description: Restriction law for surreals. Lemma 2.1.4 of Lipparini p. 3. (Contributed by Scott Fenton, 5-Dec-2021)

Ref Expression
Assertion noresle U No S No dom U A dom S A g A ¬ S suc g < s U suc g ¬ S < s U

Proof

Step Hyp Ref Expression
1 unss dom U A dom S A dom U dom S A
2 ssralv dom U dom S A g A ¬ S suc g < s U suc g g dom U dom S ¬ S suc g < s U suc g
3 1 2 sylbi dom U A dom S A g A ¬ S suc g < s U suc g g dom U dom S ¬ S suc g < s U suc g
4 3 3impia dom U A dom S A g A ¬ S suc g < s U suc g g dom U dom S ¬ S suc g < s U suc g
5 breq1 U = S U < s U S < s U
6 5 notbid U = S ¬ U < s U ¬ S < s U
7 6 biimpd U = S ¬ U < s U ¬ S < s U
8 sltso < s Or No
9 sonr < s Or No U No ¬ U < s U
10 8 9 mpan U No ¬ U < s U
11 10 adantr U No S No ¬ U < s U
12 7 11 impel U = S U No S No ¬ S < s U
13 12 adantrr U = S U No S No g dom U dom S ¬ S suc g < s U suc g ¬ S < s U
14 13 ex U = S U No S No g dom U dom S ¬ S suc g < s U suc g ¬ S < s U
15 simprl U S U No S No g dom U dom S ¬ S suc g < s U suc g U No S No
16 simprll U S U No S No g dom U dom S ¬ S suc g < s U suc g U No
17 simprlr U S U No S No g dom U dom S ¬ S suc g < s U suc g S No
18 simpl U S U No S No g dom U dom S ¬ S suc g < s U suc g U S
19 nosepne U No S No U S U x On | U x S x S x On | U x S x
20 16 17 18 19 syl3anc U S U No S No g dom U dom S ¬ S suc g < s U suc g U x On | U x S x S x On | U x S x
21 nosepon U No S No U S x On | U x S x On
22 16 17 18 21 syl3anc U S U No S No g dom U dom S ¬ S suc g < s U suc g x On | U x S x On
23 sucidg x On | U x S x On x On | U x S x suc x On | U x S x
24 22 23 syl U S U No S No g dom U dom S ¬ S suc g < s U suc g x On | U x S x suc x On | U x S x
25 24 fvresd U S U No S No g dom U dom S ¬ S suc g < s U suc g U suc x On | U x S x x On | U x S x = U x On | U x S x
26 24 fvresd U S U No S No g dom U dom S ¬ S suc g < s U suc g S suc x On | U x S x x On | U x S x = S x On | U x S x
27 20 25 26 3netr4d U S U No S No g dom U dom S ¬ S suc g < s U suc g U suc x On | U x S x x On | U x S x S suc x On | U x S x x On | U x S x
28 27 neneqd U S U No S No g dom U dom S ¬ S suc g < s U suc g ¬ U suc x On | U x S x x On | U x S x = S suc x On | U x S x x On | U x S x
29 fveq1 U suc x On | U x S x = S suc x On | U x S x U suc x On | U x S x x On | U x S x = S suc x On | U x S x x On | U x S x
30 28 29 nsyl U S U No S No g dom U dom S ¬ S suc g < s U suc g ¬ U suc x On | U x S x = S suc x On | U x S x
31 nosepdm U No S No U S x On | U x S x dom U dom S
32 16 17 18 31 syl3anc U S U No S No g dom U dom S ¬ S suc g < s U suc g x On | U x S x dom U dom S
33 simprr U S U No S No g dom U dom S ¬ S suc g < s U suc g g dom U dom S ¬ S suc g < s U suc g
34 suceq g = x On | U x S x suc g = suc x On | U x S x
35 34 reseq2d g = x On | U x S x S suc g = S suc x On | U x S x
36 34 reseq2d g = x On | U x S x U suc g = U suc x On | U x S x
37 35 36 breq12d g = x On | U x S x S suc g < s U suc g S suc x On | U x S x < s U suc x On | U x S x
38 37 notbid g = x On | U x S x ¬ S suc g < s U suc g ¬ S suc x On | U x S x < s U suc x On | U x S x
39 38 rspcv x On | U x S x dom U dom S g dom U dom S ¬ S suc g < s U suc g ¬ S suc x On | U x S x < s U suc x On | U x S x
40 32 33 39 sylc U S U No S No g dom U dom S ¬ S suc g < s U suc g ¬ S suc x On | U x S x < s U suc x On | U x S x
41 suceloni x On | U x S x On suc x On | U x S x On
42 22 41 syl U S U No S No g dom U dom S ¬ S suc g < s U suc g suc x On | U x S x On
43 noreson U No suc x On | U x S x On U suc x On | U x S x No
44 16 42 43 syl2anc U S U No S No g dom U dom S ¬ S suc g < s U suc g U suc x On | U x S x No
45 noreson S No suc x On | U x S x On S suc x On | U x S x No
46 17 42 45 syl2anc U S U No S No g dom U dom S ¬ S suc g < s U suc g S suc x On | U x S x No
47 solin < s Or No U suc x On | U x S x No S suc x On | U x S x No U suc x On | U x S x < s S suc x On | U x S x U suc x On | U x S x = S suc x On | U x S x S suc x On | U x S x < s U suc x On | U x S x
48 8 47 mpan U suc x On | U x S x No S suc x On | U x S x No U suc x On | U x S x < s S suc x On | U x S x U suc x On | U x S x = S suc x On | U x S x S suc x On | U x S x < s U suc x On | U x S x
49 44 46 48 syl2anc U S U No S No g dom U dom S ¬ S suc g < s U suc g U suc x On | U x S x < s S suc x On | U x S x U suc x On | U x S x = S suc x On | U x S x S suc x On | U x S x < s U suc x On | U x S x
50 30 40 49 ecase23d U S U No S No g dom U dom S ¬ S suc g < s U suc g U suc x On | U x S x < s S suc x On | U x S x
51 sltres U No S No suc x On | U x S x On U suc x On | U x S x < s S suc x On | U x S x U < s S
52 16 17 42 51 syl3anc U S U No S No g dom U dom S ¬ S suc g < s U suc g U suc x On | U x S x < s S suc x On | U x S x U < s S
53 50 52 mpd U S U No S No g dom U dom S ¬ S suc g < s U suc g U < s S
54 soasym < s Or No U No S No U < s S ¬ S < s U
55 8 54 mpan U No S No U < s S ¬ S < s U
56 15 53 55 sylc U S U No S No g dom U dom S ¬ S suc g < s U suc g ¬ S < s U
57 56 ex U S U No S No g dom U dom S ¬ S suc g < s U suc g ¬ S < s U
58 14 57 pm2.61ine U No S No g dom U dom S ¬ S suc g < s U suc g ¬ S < s U
59 4 58 sylan2 U No S No dom U A dom S A g A ¬ S suc g < s U suc g ¬ S < s U