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 C_ No -> E* x E. u e. A ( G e. dom u /\ A. v e. A ( -. u  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) )

Proof

Step Hyp Ref Expression
1 reeanv 
 |-  ( E. u e. A E. p e. A ( ( G e. dom u /\ A. v e. A ( -. u  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ ( G e. dom p /\ A. v e. A ( -. p  ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) <-> ( E. u e. A ( G e. dom u /\ A. v e. A ( -. u  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ E. p e. A ( G e. dom p /\ A. v e. A ( -. p  ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) )
2 breq2 
 |-  ( v = p -> ( u  u
3 2 notbid 
 |-  ( v = p -> ( -. u  -. u
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  ( u |` suc G ) = ( v |` suc G ) ) <-> ( -. u  ( u |` suc G ) = ( p |` suc G ) ) ) )
7 simprl2 
 |-  ( ( ( u e. A /\ p e. A ) /\ ( ( G e. dom u /\ A. v e. A ( -. u  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ ( G e. dom p /\ A. v e. A ( -. p  ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) ) -> A. v e. A ( -. u  ( u |` suc G ) = ( v |` suc G ) ) )
8 7 adantl 
 |-  ( ( A C_ No /\ ( ( u e. A /\ p e. A ) /\ ( ( G e. dom u /\ A. v e. A ( -. u  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ ( G e. dom p /\ A. v e. A ( -. p  ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) ) ) -> A. v e. A ( -. u  ( u |` suc G ) = ( v |` suc G ) ) )
9 simprlr 
 |-  ( ( A C_ No /\ ( ( u e. A /\ p e. A ) /\ ( ( G e. dom u /\ A. v e. A ( -. u  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ ( G e. dom p /\ A. v e. A ( -. p  ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) ) ) -> p e. A )
10 6 8 9 rspcdva 
 |-  ( ( A C_ No /\ ( ( u e. A /\ p e. A ) /\ ( ( G e. dom u /\ A. v e. A ( -. u  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ ( G e. dom p /\ A. v e. A ( -. p  ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) ) ) -> ( -. u  ( u |` suc G ) = ( p |` suc G ) ) )
11 breq2 
 |-  ( v = u -> ( p  p
12 11 notbid 
 |-  ( v = u -> ( -. p  -. p
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  ( p |` suc G ) = ( v |` suc G ) ) <-> ( -. p  ( p |` suc G ) = ( u |` suc G ) ) ) )
16 simprr2 
 |-  ( ( ( u e. A /\ p e. A ) /\ ( ( G e. dom u /\ A. v e. A ( -. u  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ ( G e. dom p /\ A. v e. A ( -. p  ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) ) -> A. v e. A ( -. p  ( p |` suc G ) = ( v |` suc G ) ) )
17 16 adantl 
 |-  ( ( A C_ No /\ ( ( u e. A /\ p e. A ) /\ ( ( G e. dom u /\ A. v e. A ( -. u  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ ( G e. dom p /\ A. v e. A ( -. p  ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) ) ) -> A. v e. A ( -. p  ( p |` suc G ) = ( v |` suc G ) ) )
18 simprll 
 |-  ( ( A C_ No /\ ( ( u e. A /\ p e. A ) /\ ( ( G e. dom u /\ A. v e. A ( -. u  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ ( G e. dom p /\ A. v e. A ( -. p  ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) ) ) -> u e. A )
19 15 17 18 rspcdva 
 |-  ( ( A C_ No /\ ( ( u e. A /\ p e. A ) /\ ( ( G e. dom u /\ A. v e. A ( -. u  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ ( G e. dom p /\ A. v e. A ( -. p  ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) ) ) -> ( -. p  ( 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 C_ No /\ ( ( u e. A /\ p e. A ) /\ ( ( G e. dom u /\ A. v e. A ( -. u  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ ( G e. dom p /\ A. v e. A ( -. p  ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) ) ) -> ( -. p  ( u |` suc G ) = ( p |` suc G ) ) )
22 simpl 
 |-  ( ( A C_ No /\ ( ( u e. A /\ p e. A ) /\ ( ( G e. dom u /\ A. v e. A ( -. u  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ ( G e. dom p /\ A. v e. A ( -. p  ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) ) ) -> A C_ No )
23 22 18 sseldd 
 |-  ( ( A C_ No /\ ( ( u e. A /\ p e. A ) /\ ( ( G e. dom u /\ A. v e. A ( -. u  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ ( G e. dom p /\ A. v e. A ( -. p  ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) ) ) -> u e. No )
24 22 9 sseldd 
 |-  ( ( A C_ No /\ ( ( u e. A /\ p e. A ) /\ ( ( G e. dom u /\ A. v e. A ( -. u  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ ( G e. dom p /\ A. v e. A ( -. p  ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) ) ) -> p e. No )
25 sltso 
 |-
26 soasym 
 |-  ( (  ( u  -. p
27 25 26 mpan 
 |-  ( ( u e. No /\ p e. No ) -> ( u  -. p
28 23 24 27 syl2anc 
 |-  ( ( A C_ No /\ ( ( u e. A /\ p e. A ) /\ ( ( G e. dom u /\ A. v e. A ( -. u  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ ( G e. dom p /\ A. v e. A ( -. p  ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) ) ) -> ( u  -. p
29 imor 
 |-  ( ( u  -. p  ( -. u
30 28 29 sylib 
 |-  ( ( A C_ No /\ ( ( u e. A /\ p e. A ) /\ ( ( G e. dom u /\ A. v e. A ( -. u  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ ( G e. dom p /\ A. v e. A ( -. p  ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) ) ) -> ( -. u
31 10 21 30 mpjaod 
 |-  ( ( A C_ No /\ ( ( u e. A /\ p e. A ) /\ ( ( G e. dom u /\ A. v e. A ( -. u  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ ( G e. dom p /\ A. v e. A ( -. p  ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) ) ) -> ( u |` suc G ) = ( p |` suc G ) )
32 31 fveq1d 
 |-  ( ( A C_ No /\ ( ( u e. A /\ p e. A ) /\ ( ( G e. dom u /\ A. v e. A ( -. u  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ ( G e. dom p /\ A. v e. A ( -. p  ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) ) ) -> ( ( u |` suc G ) ` G ) = ( ( p |` suc G ) ` G ) )
33 simprl1 
 |-  ( ( ( u e. A /\ p e. A ) /\ ( ( G e. dom u /\ A. v e. A ( -. u  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ ( G e. dom p /\ A. v e. A ( -. p  ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) ) -> G e. dom u )
34 33 adantl 
 |-  ( ( A C_ No /\ ( ( u e. A /\ p e. A ) /\ ( ( G e. dom u /\ A. v e. A ( -. u  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ ( G e. dom p /\ A. v e. A ( -. p  ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) ) ) -> G e. dom u )
35 sucidg 
 |-  ( G e. dom u -> G e. suc G )
36 34 35 syl 
 |-  ( ( A C_ No /\ ( ( u e. A /\ p e. A ) /\ ( ( G e. dom u /\ A. v e. A ( -. u  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ ( G e. dom p /\ A. v e. A ( -. p  ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) ) ) -> G e. suc G )
37 36 fvresd 
 |-  ( ( A C_ No /\ ( ( u e. A /\ p e. A ) /\ ( ( G e. dom u /\ A. v e. A ( -. u  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ ( G e. dom p /\ A. v e. A ( -. p  ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) ) ) -> ( ( u |` suc G ) ` G ) = ( u ` G ) )
38 36 fvresd 
 |-  ( ( A C_ No /\ ( ( u e. A /\ p e. A ) /\ ( ( G e. dom u /\ A. v e. A ( -. u  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ ( G e. dom p /\ A. v e. A ( -. p  ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) ) ) -> ( ( p |` suc G ) ` G ) = ( p ` G ) )
39 32 37 38 3eqtr3d 
 |-  ( ( A C_ No /\ ( ( u e. A /\ p e. A ) /\ ( ( G e. dom u /\ A. v e. A ( -. u  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ ( G e. dom p /\ A. v e. A ( -. p  ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) ) ) -> ( u ` G ) = ( p ` G ) )
40 simprl3 
 |-  ( ( ( u e. A /\ p e. A ) /\ ( ( G e. dom u /\ A. v e. A ( -. u  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ ( G e. dom p /\ A. v e. A ( -. p  ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) ) -> ( u ` G ) = x )
41 40 adantl 
 |-  ( ( A C_ No /\ ( ( u e. A /\ p e. A ) /\ ( ( G e. dom u /\ A. v e. A ( -. u  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ ( G e. dom p /\ A. v e. A ( -. p  ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) ) ) -> ( u ` G ) = x )
42 simprr3 
 |-  ( ( ( u e. A /\ p e. A ) /\ ( ( G e. dom u /\ A. v e. A ( -. u  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ ( G e. dom p /\ A. v e. A ( -. p  ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) ) -> ( p ` G ) = y )
43 42 adantl 
 |-  ( ( A C_ No /\ ( ( u e. A /\ p e. A ) /\ ( ( G e. dom u /\ A. v e. A ( -. u  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ ( G e. dom p /\ A. v e. A ( -. p  ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) ) ) -> ( p ` G ) = y )
44 39 41 43 3eqtr3d 
 |-  ( ( A C_ No /\ ( ( u e. A /\ p e. A ) /\ ( ( G e. dom u /\ A. v e. A ( -. u  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ ( G e. dom p /\ A. v e. A ( -. p  ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) ) ) -> x = y )
45 44 expr 
 |-  ( ( A C_ No /\ ( u e. A /\ p e. A ) ) -> ( ( ( G e. dom u /\ A. v e. A ( -. u  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ ( G e. dom p /\ A. v e. A ( -. p  ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) -> x = y ) )
46 45 rexlimdvva 
 |-  ( A C_ No -> ( E. u e. A E. p e. A ( ( G e. dom u /\ A. v e. A ( -. u  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ ( G e. dom p /\ A. v e. A ( -. p  ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) -> x = y ) )
47 1 46 syl5bir 
 |-  ( A C_ No -> ( ( E. u e. A ( G e. dom u /\ A. v e. A ( -. u  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ E. p e. A ( G e. dom p /\ A. v e. A ( -. p  ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) -> x = y ) )
48 47 alrimivv 
 |-  ( A C_ No -> A. x A. y ( ( E. u e. A ( G e. dom u /\ A. v e. A ( -. u  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ E. p e. A ( G e. dom p /\ A. v e. A ( -. p  ( 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 e. dom u /\ A. v e. A ( -. u  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) <-> ( G e. dom u /\ A. v e. A ( -. u  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = y ) ) )
51 50 rexbidv 
 |-  ( x = y -> ( E. u e. A ( G e. dom u /\ A. v e. A ( -. u  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) <-> E. u e. A ( G e. dom u /\ A. v e. A ( -. u  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = y ) ) )
52 dmeq 
 |-  ( u = p -> dom u = dom p )
53 52 eleq2d 
 |-  ( u = p -> ( G e. dom u <-> G e. dom p ) )
54 breq1 
 |-  ( u = p -> ( u  p
55 54 notbid 
 |-  ( u = p -> ( -. u  -. p
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  ( u |` suc G ) = ( v |` suc G ) ) <-> ( -. p  ( p |` suc G ) = ( v |` suc G ) ) ) )
59 58 ralbidv 
 |-  ( u = p -> ( A. v e. A ( -. u  ( u |` suc G ) = ( v |` suc G ) ) <-> A. v e. A ( -. p  ( 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 e. dom u /\ A. v e. A ( -. u  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = y ) <-> ( G e. dom p /\ A. v e. A ( -. p  ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) )
63 62 cbvrexvw 
 |-  ( E. u e. A ( G e. dom u /\ A. v e. A ( -. u  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = y ) <-> E. p e. A ( G e. dom p /\ A. v e. A ( -. p  ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) )
64 51 63 bitrdi 
 |-  ( x = y -> ( E. u e. A ( G e. dom u /\ A. v e. A ( -. u  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) <-> E. p e. A ( G e. dom p /\ A. v e. A ( -. p  ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) )
65 64 mo4 
 |-  ( E* x E. u e. A ( G e. dom u /\ A. v e. A ( -. u  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) <-> A. x A. y ( ( E. u e. A ( G e. dom u /\ A. v e. A ( -. u  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ E. p e. A ( G e. dom p /\ A. v e. A ( -. p  ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) -> x = y ) )
66 48 65 sylibr 
 |-  ( A C_ No -> E* x E. u e. A ( G e. dom u /\ A. v e. A ( -. u  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) )