Metamath Proof Explorer


Theorem noinffv

Description: The value of surreal infimum when there is no minimum. (Contributed by Scott Fenton, 8-Aug-2024)

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

Proof

Step Hyp Ref Expression
1 noinffv.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 iffalse ¬ x B y B ¬ y < s 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 = 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
3 1 2 syl5eq ¬ x B y B ¬ y < s x T = 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
4 3 fveq1d ¬ x B y B ¬ y < s x T G = 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 G
5 4 3ad2ant1 ¬ x B y B ¬ y < s x B No B V U B G dom U v B ¬ U < s v U suc G = v suc G T G = 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 G
6 dmeq u = U dom u = dom U
7 6 eleq2d u = U G dom u G dom U
8 breq1 u = U u < s v U < s v
9 8 notbid u = U ¬ u < s v ¬ U < s v
10 reseq1 u = U u suc G = U suc G
11 10 eqeq1d u = U u suc G = v suc G U suc G = v suc G
12 9 11 imbi12d u = U ¬ u < s v u suc G = v suc G ¬ U < s v U suc G = v suc G
13 12 ralbidv u = U v B ¬ u < s v u suc G = v suc G v B ¬ U < s v U suc G = v suc G
14 7 13 anbi12d u = U G dom u v B ¬ u < s v u suc G = v suc G G dom U v B ¬ U < s v U suc G = v suc G
15 14 rspcev U B G dom U v B ¬ U < s v U suc G = v suc G u B G dom u v B ¬ u < s v u suc G = v suc G
16 15 3impb U B G dom U v B ¬ U < s v U suc G = v suc G u B G dom u v B ¬ u < s v u suc G = v suc G
17 16 3ad2ant3 ¬ x B y B ¬ y < s x B No B V U B G dom U v B ¬ U < s v U suc G = v suc G u B G dom u v B ¬ u < s v u suc G = v suc G
18 simp32 ¬ x B y B ¬ y < s x B No B V U B G dom U v B ¬ U < s v U suc G = v suc G G dom U
19 eleq1 y = G y dom u G dom u
20 suceq y = G suc y = suc G
21 20 reseq2d y = G u suc y = u suc G
22 20 reseq2d y = G v suc y = v suc G
23 21 22 eqeq12d y = G u suc y = v suc y u suc G = v suc G
24 23 imbi2d y = G ¬ u < s v u suc y = v suc y ¬ u < s v u suc G = v suc G
25 24 ralbidv y = G v B ¬ u < s v u suc y = v suc y v B ¬ u < s v u suc G = v suc G
26 19 25 anbi12d y = G y dom u v B ¬ u < s v u suc y = v suc y G dom u v B ¬ u < s v u suc G = v suc G
27 26 rexbidv y = G u B y dom u v B ¬ u < s v u suc y = v suc y u B G dom u v B ¬ u < s v u suc G = v suc G
28 27 elabg G dom U G y | u B y dom u v B ¬ u < s v u suc y = v suc y u B G dom u v B ¬ u < s v u suc G = v suc G
29 18 28 syl ¬ x B y B ¬ y < s x B No B V U B G dom U v B ¬ U < s v U suc G = v suc G G y | u B y dom u v B ¬ u < s v u suc y = v suc y u B G dom u v B ¬ u < s v u suc G = v suc G
30 17 29 mpbird ¬ x B y B ¬ y < s x B No B V U B G dom U v B ¬ U < s v U suc G = v suc G G y | u B y dom u v B ¬ u < s v u suc y = v suc y
31 eleq1 g = G g dom u G dom u
32 suceq g = G suc g = suc G
33 32 reseq2d g = G u suc g = u suc G
34 32 reseq2d g = G v suc g = v suc G
35 33 34 eqeq12d g = G u suc g = v suc g u suc G = v suc G
36 35 imbi2d g = G ¬ u < s v u suc g = v suc g ¬ u < s v u suc G = v suc G
37 36 ralbidv g = G v B ¬ u < s v u suc g = v suc g v B ¬ u < s v u suc G = v suc G
38 fveqeq2 g = G u g = x u G = x
39 31 37 38 3anbi123d g = G g dom u v B ¬ u < s v u suc g = v suc g u g = x G dom u v B ¬ u < s v u suc G = v suc G u G = x
40 39 rexbidv g = G u B g dom u v B ¬ u < s v u suc g = v suc g u g = x u B G dom u v B ¬ u < s v u suc G = v suc G u G = x
41 40 iotabidv g = G ι x | u B g dom u v B ¬ u < s v u suc g = v suc g u g = x = ι x | u B G dom u v B ¬ u < s v u suc G = v suc G u G = x
42 eqid 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 = 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
43 iotaex ι x | u B G dom u v B ¬ u < s v u suc G = v suc G u G = x V
44 41 42 43 fvmpt G y | u B y dom u v B ¬ u < s v u suc y = v suc y 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 G = ι x | u B G dom u v B ¬ u < s v u suc G = v suc G u G = x
45 30 44 syl ¬ x B y B ¬ y < s x B No B V U B G dom U v B ¬ U < s v U suc G = v suc G 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 G = ι x | u B G dom u v B ¬ u < s v u suc G = v suc G u G = x
46 simp1 U B G dom U v B ¬ U < s v U suc G = v suc G U B
47 simp2 U B G dom U v B ¬ U < s v U suc G = v suc G G dom U
48 simp3 U B G dom U v B ¬ U < s v U suc G = v suc G v B ¬ U < s v U suc G = v suc G
49 eqidd U B G dom U v B ¬ U < s v U suc G = v suc G U G = U G
50 fveq1 u = U u G = U G
51 50 eqeq1d u = U u G = U G U G = U G
52 7 13 51 3anbi123d u = U G dom u v B ¬ u < s v u suc G = v suc G u G = U G G dom U v B ¬ U < s v U suc G = v suc G U G = U G
53 52 rspcev U B G dom U v B ¬ U < s v U suc G = v suc G U G = U G u B G dom u v B ¬ u < s v u suc G = v suc G u G = U G
54 46 47 48 49 53 syl13anc U B G dom U v B ¬ U < s v U suc G = v suc G u B G dom u v B ¬ u < s v u suc G = v suc G u G = U G
55 54 3ad2ant3 ¬ x B y B ¬ y < s x B No B V U B G dom U v B ¬ U < s v U suc G = v suc G u B G dom u v B ¬ u < s v u suc G = v suc G u G = U G
56 fvex U G V
57 eqid u G = u G
58 fvex u G V
59 eqeq2 x = u G u G = x u G = u G
60 59 3anbi3d x = u G G dom u v B ¬ u < s v u suc G = v suc G u G = x G dom u v B ¬ u < s v u suc G = v suc G u G = u G
61 58 60 spcev G dom u v B ¬ u < s v u suc G = v suc G u G = u G x G dom u v B ¬ u < s v u suc G = v suc G u G = x
62 57 61 mp3an3 G dom u v B ¬ u < s v u suc G = v suc G x G dom u v B ¬ u < s v u suc G = v suc G u G = x
63 62 reximi u B G dom u v B ¬ u < s v u suc G = v suc G u B x G dom u v B ¬ u < s v u suc G = v suc G u G = x
64 rexcom4 u B x G dom u v B ¬ u < s v u suc G = v suc G u G = x x u B G dom u v B ¬ u < s v u suc G = v suc G u G = x
65 63 64 sylib u B G dom u v B ¬ u < s v u suc G = v suc G x u B G dom u v B ¬ u < s v u suc G = v suc G u G = x
66 16 65 syl U B G dom U v B ¬ U < s v U suc G = v suc G x u B G dom u v B ¬ u < s v u suc G = v suc G u G = x
67 66 3ad2ant3 ¬ x B y B ¬ y < s x B No B V U B G dom U v B ¬ U < s v U suc G = v suc G x u B G dom u v B ¬ u < s v u suc G = v suc G u G = x
68 simp2l ¬ x B y B ¬ y < s x B No B V U B G dom U v B ¬ U < s v U suc G = v suc G B No
69 noinfprefixmo B No * x u B G dom u v B ¬ u < s v u suc G = v suc G u G = x
70 68 69 syl ¬ x B y B ¬ y < s x B No B V U B G dom U v B ¬ U < s v U suc G = v suc G * x u B G dom u v B ¬ u < s v u suc G = v suc G u G = x
71 df-eu ∃! x u B G dom u v B ¬ u < s v u suc G = v suc G u G = x x u B G dom u v B ¬ u < s v u suc G = v suc G u G = x * x u B G dom u v B ¬ u < s v u suc G = v suc G u G = x
72 67 70 71 sylanbrc ¬ x B y B ¬ y < s x B No B V U B G dom U v B ¬ U < s v U suc G = v suc G ∃! x u B G dom u v B ¬ u < s v u suc G = v suc G u G = x
73 eqeq2 x = U G u G = x u G = U G
74 73 3anbi3d x = U G G dom u v B ¬ u < s v u suc G = v suc G u G = x G dom u v B ¬ u < s v u suc G = v suc G u G = U G
75 74 rexbidv x = U G u B G dom u v B ¬ u < s v u suc G = v suc G u G = x u B G dom u v B ¬ u < s v u suc G = v suc G u G = U G
76 75 iota2 U G V ∃! x u B G dom u v B ¬ u < s v u suc G = v suc G u G = x u B G dom u v B ¬ u < s v u suc G = v suc G u G = U G ι x | u B G dom u v B ¬ u < s v u suc G = v suc G u G = x = U G
77 56 72 76 sylancr ¬ x B y B ¬ y < s x B No B V U B G dom U v B ¬ U < s v U suc G = v suc G u B G dom u v B ¬ u < s v u suc G = v suc G u G = U G ι x | u B G dom u v B ¬ u < s v u suc G = v suc G u G = x = U G
78 55 77 mpbid ¬ x B y B ¬ y < s x B No B V U B G dom U v B ¬ U < s v U suc G = v suc G ι x | u B G dom u v B ¬ u < s v u suc G = v suc G u G = x = U G
79 5 45 78 3eqtrd ¬ x B y B ¬ y < s x B No B V U B G dom U v B ¬ U < s v U suc G = v suc G T G = U G