Metamath Proof Explorer


Theorem noinfprefixmo

Description: In any class of surreals, there is at most one value of the prefix property. (Contributed by Scott Fenton, 8-Aug-2024)

Ref Expression
Assertion noinfprefixmo A No * x u A G dom u v A ¬ u < s v u suc G = v suc G u G = x

Proof

Step Hyp Ref Expression
1 reeanv u A p A G dom u v A ¬ u < s v u suc G = v suc G u G = x G dom p v A ¬ p < s v p suc G = v suc G p G = y u A G dom u v A ¬ u < s v u suc G = v suc G u G = x p A G dom p v A ¬ p < s v p suc G = v suc G p G = y
2 breq2 v = p u < s v u < s p
3 2 notbid v = p ¬ u < s v ¬ u < s p
4 reseq1 v = p v suc G = p suc G
5 4 eqeq2d v = p u suc G = v suc G u suc G = p suc G
6 3 5 imbi12d v = p ¬ u < s v u suc G = v suc G ¬ u < s p u suc G = p suc G
7 simprl2 u A p A G dom u v A ¬ u < s v u suc G = v suc G u G = x G dom p v A ¬ p < s v p suc G = v suc G p G = y v A ¬ u < s v u suc G = v suc G
8 7 adantl A No u A p A G dom u v A ¬ u < s v u suc G = v suc G u G = x G dom p v A ¬ p < s v p suc G = v suc G p G = y v A ¬ u < s v u suc G = v suc G
9 simprlr A No u A p A G dom u v A ¬ u < s v u suc G = v suc G u G = x G dom p v A ¬ p < s v p suc G = v suc G p G = y p A
10 6 8 9 rspcdva A No u A p A G dom u v A ¬ u < s v u suc G = v suc G u G = x G dom p v A ¬ p < s v p suc G = v suc G p G = y ¬ u < s p u suc G = p suc G
11 breq2 v = u p < s v p < s u
12 11 notbid v = u ¬ p < s v ¬ p < s u
13 reseq1 v = u v suc G = u suc G
14 13 eqeq2d v = u p suc G = v suc G p suc G = u suc G
15 12 14 imbi12d v = u ¬ p < s v p suc G = v suc G ¬ p < s u p suc G = u suc G
16 simprr2 u A p A G dom u v A ¬ u < s v u suc G = v suc G u G = x G dom p v A ¬ p < s v p suc G = v suc G p G = y v A ¬ p < s v p suc G = v suc G
17 16 adantl A No u A p A G dom u v A ¬ u < s v u suc G = v suc G u G = x G dom p v A ¬ p < s v p suc G = v suc G p G = y v A ¬ p < s v p suc G = v suc G
18 simprll A No u A p A G dom u v A ¬ u < s v u suc G = v suc G u G = x G dom p v A ¬ p < s v p suc G = v suc G p G = y u A
19 15 17 18 rspcdva A No u A p A G dom u v A ¬ u < s v u suc G = v suc G u G = x G dom p v A ¬ p < s v p suc G = v suc G p G = y ¬ p < s u p suc G = u suc G
20 eqcom p suc G = u suc G u suc G = p suc G
21 19 20 syl6ib A No u A p A G dom u v A ¬ u < s v u suc G = v suc G u G = x G dom p v A ¬ p < s v p suc G = v suc G p G = y ¬ p < s u u suc G = p suc G
22 simpl A No u A p A G dom u v A ¬ u < s v u suc G = v suc G u G = x G dom p v A ¬ p < s v p suc G = v suc G p G = y A No
23 22 18 sseldd A No u A p A G dom u v A ¬ u < s v u suc G = v suc G u G = x G dom p v A ¬ p < s v p suc G = v suc G p G = y u No
24 22 9 sseldd A No u A p A G dom u v A ¬ u < s v u suc G = v suc G u G = x G dom p v A ¬ p < s v p suc G = v suc G p G = y p No
25 sltso < s Or No
26 soasym < s Or No u No p No u < s p ¬ p < s u
27 25 26 mpan u No p No u < s p ¬ p < s u
28 23 24 27 syl2anc A No u A p A G dom u v A ¬ u < s v u suc G = v suc G u G = x G dom p v A ¬ p < s v p suc G = v suc G p G = y u < s p ¬ p < s u
29 imor u < s p ¬ p < s u ¬ u < s p ¬ p < s u
30 28 29 sylib A No u A p A G dom u v A ¬ u < s v u suc G = v suc G u G = x G dom p v A ¬ p < s v p suc G = v suc G p G = y ¬ u < s p ¬ p < s u
31 10 21 30 mpjaod A No u A p A G dom u v A ¬ u < s v u suc G = v suc G u G = x G dom p v A ¬ p < s v p suc G = v suc G p G = y u suc G = p suc G
32 31 fveq1d A No u A p A G dom u v A ¬ u < s v u suc G = v suc G u G = x G dom p v A ¬ p < s v p suc G = v suc G p G = y u suc G G = p suc G G
33 simprl1 u A p A G dom u v A ¬ u < s v u suc G = v suc G u G = x G dom p v A ¬ p < s v p suc G = v suc G p G = y G dom u
34 33 adantl A No u A p A G dom u v A ¬ u < s v u suc G = v suc G u G = x G dom p v A ¬ p < s v p suc G = v suc G p G = y G dom u
35 sucidg G dom u G suc G
36 34 35 syl A No u A p A G dom u v A ¬ u < s v u suc G = v suc G u G = x G dom p v A ¬ p < s v p suc G = v suc G p G = y G suc G
37 36 fvresd A No u A p A G dom u v A ¬ u < s v u suc G = v suc G u G = x G dom p v A ¬ p < s v p suc G = v suc G p G = y u suc G G = u G
38 36 fvresd A No u A p A G dom u v A ¬ u < s v u suc G = v suc G u G = x G dom p v A ¬ p < s v p suc G = v suc G p G = y p suc G G = p G
39 32 37 38 3eqtr3d A No u A p A G dom u v A ¬ u < s v u suc G = v suc G u G = x G dom p v A ¬ p < s v p suc G = v suc G p G = y u G = p G
40 simprl3 u A p A G dom u v A ¬ u < s v u suc G = v suc G u G = x G dom p v A ¬ p < s v p suc G = v suc G p G = y u G = x
41 40 adantl A No u A p A G dom u v A ¬ u < s v u suc G = v suc G u G = x G dom p v A ¬ p < s v p suc G = v suc G p G = y u G = x
42 simprr3 u A p A G dom u v A ¬ u < s v u suc G = v suc G u G = x G dom p v A ¬ p < s v p suc G = v suc G p G = y p G = y
43 42 adantl A No u A p A G dom u v A ¬ u < s v u suc G = v suc G u G = x G dom p v A ¬ p < s v p suc G = v suc G p G = y p G = y
44 39 41 43 3eqtr3d A No u A p A G dom u v A ¬ u < s v u suc G = v suc G u G = x G dom p v A ¬ p < s v p suc G = v suc G p G = y x = y
45 44 expr A No u A p A G dom u v A ¬ u < s v u suc G = v suc G u G = x G dom p v A ¬ p < s v p suc G = v suc G p G = y x = y
46 45 rexlimdvva A No u A p A G dom u v A ¬ u < s v u suc G = v suc G u G = x G dom p v A ¬ p < s v p suc G = v suc G p G = y x = y
47 1 46 syl5bir A No u A G dom u v A ¬ u < s v u suc G = v suc G u G = x p A G dom p v A ¬ p < s v p suc G = v suc G p G = y x = y
48 47 alrimivv A No x y u A G dom u v A ¬ u < s v u suc G = v suc G u G = x p A G dom p v A ¬ p < s v p suc G = v suc G p G = y x = y
49 eqeq2 x = y u G = x u G = y
50 49 3anbi3d x = y G dom u v A ¬ u < s v u suc G = v suc G u G = x G dom u v A ¬ u < s v u suc G = v suc G u G = y
51 50 rexbidv x = y u A G dom u v A ¬ u < s v u suc G = v suc G u G = x u A G dom u v A ¬ u < s v u suc G = v suc G u G = y
52 dmeq u = p dom u = dom p
53 52 eleq2d u = p G dom u G dom p
54 breq1 u = p u < s v p < s v
55 54 notbid u = p ¬ u < s v ¬ p < s v
56 reseq1 u = p u suc G = p suc G
57 56 eqeq1d u = p u suc G = v suc G p suc G = v suc G
58 55 57 imbi12d u = p ¬ u < s v u suc G = v suc G ¬ p < s v p suc G = v suc G
59 58 ralbidv u = p v A ¬ u < s v u suc G = v suc G v A ¬ p < s v p suc G = v suc G
60 fveq1 u = p u G = p G
61 60 eqeq1d u = p u G = y p G = y
62 53 59 61 3anbi123d u = p G dom u v A ¬ u < s v u suc G = v suc G u G = y G dom p v A ¬ p < s v p suc G = v suc G p G = y
63 62 cbvrexvw u A G dom u v A ¬ u < s v u suc G = v suc G u G = y p A G dom p v A ¬ p < s v p suc G = v suc G p G = y
64 51 63 bitrdi x = y u A G dom u v A ¬ u < s v u suc G = v suc G u G = x p A G dom p v A ¬ p < s v p suc G = v suc G p G = y
65 64 mo4 * x u A G dom u v A ¬ u < s v u suc G = v suc G u G = x x y u A G dom u v A ¬ u < s v u suc G = v suc G u G = x p A G dom p v A ¬ p < s v p suc G = v suc G p G = y x = y
66 48 65 sylibr A No * x u A G dom u v A ¬ u < s v u suc G = v suc G u G = x