Metamath Proof Explorer


Theorem nosupres

Description: A restriction law for surreal supremum when there is no maximum. (Contributed by Scott Fenton, 5-Dec-2021)

Ref Expression
Hypothesis nosupres.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 nosupres ¬ x A y A ¬ x < s y A No A V U A G dom U v A ¬ v < s U U suc G = v suc G S suc G = U suc G

Proof

Step Hyp Ref Expression
1 nosupres.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 dmres dom S suc G = suc G dom S
3 1 nosupno A No A V S No
4 3 3ad2ant2 ¬ x A y A ¬ x < s y A No A V U A G dom U v A ¬ v < s U U suc G = v suc G S No
5 nodmord S No Ord dom S
6 4 5 syl ¬ x A y A ¬ x < s y A No A V U A G dom U v A ¬ v < s U U suc G = v suc G Ord dom S
7 dmeq p = U dom p = dom U
8 7 eleq2d p = U G dom p G dom U
9 breq2 p = U v < s p v < s U
10 9 notbid p = U ¬ v < s p ¬ v < s U
11 reseq1 p = U p suc G = U suc G
12 11 eqeq1d p = U p suc G = v suc G U suc G = v suc G
13 10 12 imbi12d p = U ¬ v < s p p suc G = v suc G ¬ v < s U U suc G = v suc G
14 13 ralbidv p = U v A ¬ v < s p p suc G = v suc G v A ¬ v < s U U suc G = v suc G
15 8 14 anbi12d p = U G dom p v A ¬ v < s p p suc G = v suc G G dom U v A ¬ v < s U U suc G = v suc G
16 15 rspcev U A G dom U v A ¬ v < s U U suc G = v suc G p A G dom p v A ¬ v < s p p suc G = v suc G
17 16 3impb U A G dom U v A ¬ v < s U U suc G = v suc G p A G dom p v A ¬ v < s p p suc G = v suc G
18 dmeq u = p dom u = dom p
19 18 eleq2d u = p G dom u G dom p
20 breq2 u = p v < s u v < s p
21 20 notbid u = p ¬ v < s u ¬ v < s p
22 reseq1 u = p u suc G = p suc G
23 22 eqeq1d u = p u suc G = v suc G p suc G = v suc G
24 21 23 imbi12d u = p ¬ v < s u u suc G = v suc G ¬ v < s p p suc G = v suc G
25 24 ralbidv u = p v A ¬ v < s u u suc G = v suc G v A ¬ v < s p p suc G = v suc G
26 19 25 anbi12d u = p G dom u v A ¬ v < s u u suc G = v suc G G dom p v A ¬ v < s p p suc G = v suc G
27 26 cbvrexvw u A G dom u v A ¬ v < s u u suc G = v suc G p A G dom p v A ¬ v < s p p suc G = v suc G
28 17 27 sylibr 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
29 eleq1 y = G y dom u G dom u
30 suceq y = G suc y = suc G
31 30 reseq2d y = G u suc y = u suc G
32 30 reseq2d y = G v suc y = v suc G
33 31 32 eqeq12d y = G u suc y = v suc y u suc G = v suc G
34 33 imbi2d y = G ¬ v < s u u suc y = v suc y ¬ v < s u u suc G = v suc G
35 34 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
36 29 35 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
37 36 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
38 37 elabg G dom U 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
39 38 3ad2ant2 U A G dom U v A ¬ v < s U U suc G = v suc G 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
40 28 39 mpbird U A G dom U v A ¬ v < s U U suc G = v suc G G y | u A y dom u v A ¬ v < s u u suc y = v suc y
41 40 3ad2ant3 ¬ x A y A ¬ x < s y A No A V U A G dom U v A ¬ v < s U U suc G = v suc G G y | u A y dom u v A ¬ v < s u u suc y = v suc y
42 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
43 1 42 syl5eq ¬ x A y A ¬ x < s y S = 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
44 43 dmeqd ¬ x A y A ¬ x < s y dom S = 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
45 iotaex ι x | u A g dom u v A ¬ v < s u u suc g = v suc g u g = x V
46 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
47 45 46 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
48 44 47 eqtrdi ¬ x A y A ¬ x < s y dom S = y | u A y dom u v A ¬ v < s u u suc y = v suc y
49 48 3ad2ant1 ¬ x A y A ¬ x < s y A No A V U A G dom U v A ¬ v < s U U suc G = v suc G dom S = y | u A y dom u v A ¬ v < s u u suc y = v suc y
50 41 49 eleqtrrd ¬ x A y A ¬ x < s y A No A V U A G dom U v A ¬ v < s U U suc G = v suc G G dom S
51 ordsucss Ord dom S G dom S suc G dom S
52 6 50 51 sylc ¬ x A y A ¬ x < s y A No A V U A G dom U v A ¬ v < s U U suc G = v suc G suc G dom S
53 df-ss suc G dom S suc G dom S = suc G
54 52 53 sylib ¬ x A y A ¬ x < s y A No A V U A G dom U v A ¬ v < s U U suc G = v suc G suc G dom S = suc G
55 2 54 syl5eq ¬ x A y A ¬ x < s y A No A V U A G dom U v A ¬ v < s U U suc G = v suc G dom S suc G = suc G
56 dmres dom U suc G = suc G dom U
57 simp2l ¬ x A y A ¬ x < s y A No A V U A G dom U v A ¬ v < s U U suc G = v suc G A No
58 simp31 ¬ x A y A ¬ x < s y A No A V U A G dom U v A ¬ v < s U U suc G = v suc G U A
59 57 58 sseldd ¬ x A y A ¬ x < s y A No A V U A G dom U v A ¬ v < s U U suc G = v suc G U No
60 nodmord U No Ord dom U
61 59 60 syl ¬ x A y A ¬ x < s y A No A V U A G dom U v A ¬ v < s U U suc G = v suc G Ord dom U
62 simp32 ¬ x A y A ¬ x < s y A No A V U A G dom U v A ¬ v < s U U suc G = v suc G G dom U
63 ordsucss Ord dom U G dom U suc G dom U
64 61 62 63 sylc ¬ x A y A ¬ x < s y A No A V U A G dom U v A ¬ v < s U U suc G = v suc G suc G dom U
65 df-ss suc G dom U suc G dom U = suc G
66 64 65 sylib ¬ x A y A ¬ x < s y A No A V U A G dom U v A ¬ v < s U U suc G = v suc G suc G dom U = suc G
67 56 66 syl5eq ¬ x A y A ¬ x < s y A No A V U A G dom U v A ¬ v < s U U suc G = v suc G dom U suc G = suc G
68 55 67 eqtr4d ¬ x A y A ¬ x < s y A No A V U A G dom U v A ¬ v < s U U suc G = v suc G dom S suc G = dom U suc G
69 55 eleq2d ¬ x A y A ¬ x < s y A No A V U A G dom U v A ¬ v < s U U suc G = v suc G a dom S suc G a suc G
70 simpl1 ¬ x A y A ¬ x < s y A No A V U A G dom U v A ¬ v < s U U suc G = v suc G a suc G ¬ x A y A ¬ x < s y
71 simpl2 ¬ x A y A ¬ x < s y A No A V U A G dom U v A ¬ v < s U U suc G = v suc G a suc G A No A V
72 simpl31 ¬ x A y A ¬ x < s y A No A V U A G dom U v A ¬ v < s U U suc G = v suc G a suc G U A
73 64 sselda ¬ x A y A ¬ x < s y A No A V U A G dom U v A ¬ v < s U U suc G = v suc G a suc G a dom U
74 nodmon U No dom U On
75 59 74 syl ¬ x A y A ¬ x < s y A No A V U A G dom U v A ¬ v < s U U suc G = v suc G dom U On
76 onelon dom U On G dom U G On
77 75 62 76 syl2anc ¬ x A y A ¬ x < s y A No A V U A G dom U v A ¬ v < s U U suc G = v suc G G On
78 eloni G On Ord G
79 77 78 syl ¬ x A y A ¬ x < s y A No A V U A G dom U v A ¬ v < s U U suc G = v suc G Ord G
80 ordsuc Ord G Ord suc G
81 79 80 sylib ¬ x A y A ¬ x < s y A No A V U A G dom U v A ¬ v < s U U suc G = v suc G Ord suc G
82 ordsucss Ord suc G a suc G suc a suc G
83 81 82 syl ¬ x A y A ¬ x < s y A No A V U A G dom U v A ¬ v < s U U suc G = v suc G a suc G suc a suc G
84 83 imp ¬ x A y A ¬ x < s y A No A V U A G dom U v A ¬ v < s U U suc G = v suc G a suc G suc a suc G
85 simpl33 ¬ x A y A ¬ x < s y A No A V U A G dom U v A ¬ v < s U U suc G = v suc G a suc G v A ¬ v < s U U suc G = v suc G
86 reseq1 U suc G = v suc G U suc G suc a = v suc G suc a
87 resabs1 suc a suc G U suc G suc a = U suc a
88 resabs1 suc a suc G v suc G suc a = v suc a
89 87 88 eqeq12d suc a suc G U suc G suc a = v suc G suc a U suc a = v suc a
90 86 89 syl5ib suc a suc G U suc G = v suc G U suc a = v suc a
91 90 imim2d suc a suc G ¬ v < s U U suc G = v suc G ¬ v < s U U suc a = v suc a
92 91 ralimdv suc a suc G v A ¬ v < s U U suc G = v suc G v A ¬ v < s U U suc a = v suc a
93 84 85 92 sylc ¬ x A y A ¬ x < s y A No A V U A G dom U v A ¬ v < s U U suc G = v suc G a suc G v A ¬ v < s U U suc a = v suc a
94 1 nosupfv ¬ x A y A ¬ x < s y A No A V U A a dom U v A ¬ v < s U U suc a = v suc a S a = U a
95 70 71 72 73 93 94 syl113anc ¬ x A y A ¬ x < s y A No A V U A G dom U v A ¬ v < s U U suc G = v suc G a suc G S a = U a
96 simpr ¬ x A y A ¬ x < s y A No A V U A G dom U v A ¬ v < s U U suc G = v suc G a suc G a suc G
97 96 fvresd ¬ x A y A ¬ x < s y A No A V U A G dom U v A ¬ v < s U U suc G = v suc G a suc G S suc G a = S a
98 96 fvresd ¬ x A y A ¬ x < s y A No A V U A G dom U v A ¬ v < s U U suc G = v suc G a suc G U suc G a = U a
99 95 97 98 3eqtr4d ¬ x A y A ¬ x < s y A No A V U A G dom U v A ¬ v < s U U suc G = v suc G a suc G S suc G a = U suc G a
100 99 ex ¬ x A y A ¬ x < s y A No A V U A G dom U v A ¬ v < s U U suc G = v suc G a suc G S suc G a = U suc G a
101 69 100 sylbid ¬ x A y A ¬ x < s y A No A V U A G dom U v A ¬ v < s U U suc G = v suc G a dom S suc G S suc G a = U suc G a
102 101 ralrimiv ¬ x A y A ¬ x < s y A No A V U A G dom U v A ¬ v < s U U suc G = v suc G a dom S suc G S suc G a = U suc G a
103 nofun S No Fun S
104 funres Fun S Fun S suc G
105 4 103 104 3syl ¬ x A y A ¬ x < s y A No A V U A G dom U v A ¬ v < s U U suc G = v suc G Fun S suc G
106 nofun U No Fun U
107 funres Fun U Fun U suc G
108 59 106 107 3syl ¬ x A y A ¬ x < s y A No A V U A G dom U v A ¬ v < s U U suc G = v suc G Fun U suc G
109 eqfunfv Fun S suc G Fun U suc G S suc G = U suc G dom S suc G = dom U suc G a dom S suc G S suc G a = U suc G a
110 105 108 109 syl2anc ¬ x A y A ¬ x < s y A No A V U A G dom U v A ¬ v < s U U suc G = v suc G S suc G = U suc G dom S suc G = dom U suc G a dom S suc G S suc G a = U suc G a
111 68 102 110 mpbir2and ¬ x A y A ¬ x < s y A No A V U A G dom U v A ¬ v < s U U suc G = v suc G S suc G = U suc G