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 ( E. x e. B A. y e. B -. y . } ) , ( g e. { y | E. u e. B ( y e. dom u /\ A. v e. B ( -. u  ( u |` suc y ) = ( v |` suc y ) ) ) } |-> ( iota x E. u e. B ( g e. dom u /\ A. v e. B ( -. u  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) ) )
Assertion noinffv 
|- ( ( -. E. x e. B A. y e. B -. y  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> ( T ` G ) = ( U ` G ) )

Proof

Step Hyp Ref Expression
1 noinffv.1 
 |-  T = if ( E. x e. B A. y e. B -. y . } ) , ( g e. { y | E. u e. B ( y e. dom u /\ A. v e. B ( -. u  ( u |` suc y ) = ( v |` suc y ) ) ) } |-> ( iota x E. u e. B ( g e. dom u /\ A. v e. B ( -. u  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) ) )
2 iffalse 
 |-  ( -. E. x e. B A. y e. B -. y  if ( E. x e. B A. y e. B -. y . } ) , ( g e. { y | E. u e. B ( y e. dom u /\ A. v e. B ( -. u  ( u |` suc y ) = ( v |` suc y ) ) ) } |-> ( iota x E. u e. B ( g e. dom u /\ A. v e. B ( -. u  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) ) ) = ( g e. { y | E. u e. B ( y e. dom u /\ A. v e. B ( -. u  ( u |` suc y ) = ( v |` suc y ) ) ) } |-> ( iota x E. u e. B ( g e. dom u /\ A. v e. B ( -. u  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) ) )
3 1 2 syl5eq 
 |-  ( -. E. x e. B A. y e. B -. y  T = ( g e. { y | E. u e. B ( y e. dom u /\ A. v e. B ( -. u  ( u |` suc y ) = ( v |` suc y ) ) ) } |-> ( iota x E. u e. B ( g e. dom u /\ A. v e. B ( -. u  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) ) )
4 3 fveq1d 
 |-  ( -. E. x e. B A. y e. B -. y  ( T ` G ) = ( ( g e. { y | E. u e. B ( y e. dom u /\ A. v e. B ( -. u  ( u |` suc y ) = ( v |` suc y ) ) ) } |-> ( iota x E. u e. B ( g e. dom u /\ A. v e. B ( -. u  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) ) ` G ) )
5 4 3ad2ant1 
 |-  ( ( -. E. x e. B A. y e. B -. y  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> ( T ` G ) = ( ( g e. { y | E. u e. B ( y e. dom u /\ A. v e. B ( -. u  ( u |` suc y ) = ( v |` suc y ) ) ) } |-> ( iota x E. u e. B ( g e. dom u /\ A. v e. B ( -. u  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) ) ` G ) )
6 dmeq 
 |-  ( u = U -> dom u = dom U )
7 6 eleq2d 
 |-  ( u = U -> ( G e. dom u <-> G e. dom U ) )
8 breq1 
 |-  ( u = U -> ( u  U
9 8 notbid 
 |-  ( u = U -> ( -. u  -. U
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  ( u |` suc G ) = ( v |` suc G ) ) <-> ( -. U  ( U |` suc G ) = ( v |` suc G ) ) ) )
13 12 ralbidv 
 |-  ( u = U -> ( A. v e. B ( -. u  ( u |` suc G ) = ( v |` suc G ) ) <-> A. v e. B ( -. U  ( U |` suc G ) = ( v |` suc G ) ) ) )
14 7 13 anbi12d 
 |-  ( u = U -> ( ( G e. dom u /\ A. v e. B ( -. u  ( u |` suc G ) = ( v |` suc G ) ) ) <-> ( G e. dom U /\ A. v e. B ( -. U  ( U |` suc G ) = ( v |` suc G ) ) ) ) )
15 14 rspcev 
 |-  ( ( U e. B /\ ( G e. dom U /\ A. v e. B ( -. U  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> E. u e. B ( G e. dom u /\ A. v e. B ( -. u  ( u |` suc G ) = ( v |` suc G ) ) ) )
16 15 3impb 
 |-  ( ( U e. B /\ G e. dom U /\ A. v e. B ( -. U  ( U |` suc G ) = ( v |` suc G ) ) ) -> E. u e. B ( G e. dom u /\ A. v e. B ( -. u  ( u |` suc G ) = ( v |` suc G ) ) ) )
17 16 3ad2ant3 
 |-  ( ( -. E. x e. B A. y e. B -. y  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> E. u e. B ( G e. dom u /\ A. v e. B ( -. u  ( u |` suc G ) = ( v |` suc G ) ) ) )
18 simp32 
 |-  ( ( -. E. x e. B A. y e. B -. y  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> G e. dom U )
19 eleq1 
 |-  ( y = G -> ( y e. dom u <-> G e. 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  ( u |` suc y ) = ( v |` suc y ) ) <-> ( -. u  ( u |` suc G ) = ( v |` suc G ) ) ) )
25 24 ralbidv 
 |-  ( y = G -> ( A. v e. B ( -. u  ( u |` suc y ) = ( v |` suc y ) ) <-> A. v e. B ( -. u  ( u |` suc G ) = ( v |` suc G ) ) ) )
26 19 25 anbi12d 
 |-  ( y = G -> ( ( y e. dom u /\ A. v e. B ( -. u  ( u |` suc y ) = ( v |` suc y ) ) ) <-> ( G e. dom u /\ A. v e. B ( -. u  ( u |` suc G ) = ( v |` suc G ) ) ) ) )
27 26 rexbidv 
 |-  ( y = G -> ( E. u e. B ( y e. dom u /\ A. v e. B ( -. u  ( u |` suc y ) = ( v |` suc y ) ) ) <-> E. u e. B ( G e. dom u /\ A. v e. B ( -. u  ( u |` suc G ) = ( v |` suc G ) ) ) ) )
28 27 elabg 
 |-  ( G e. dom U -> ( G e. { y | E. u e. B ( y e. dom u /\ A. v e. B ( -. u  ( u |` suc y ) = ( v |` suc y ) ) ) } <-> E. u e. B ( G e. dom u /\ A. v e. B ( -. u  ( u |` suc G ) = ( v |` suc G ) ) ) ) )
29 18 28 syl 
 |-  ( ( -. E. x e. B A. y e. B -. y  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> ( G e. { y | E. u e. B ( y e. dom u /\ A. v e. B ( -. u  ( u |` suc y ) = ( v |` suc y ) ) ) } <-> E. u e. B ( G e. dom u /\ A. v e. B ( -. u  ( u |` suc G ) = ( v |` suc G ) ) ) ) )
30 17 29 mpbird 
 |-  ( ( -. E. x e. B A. y e. B -. y  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> G e. { y | E. u e. B ( y e. dom u /\ A. v e. B ( -. u  ( u |` suc y ) = ( v |` suc y ) ) ) } )
31 eleq1 
 |-  ( g = G -> ( g e. dom u <-> G e. 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  ( u |` suc g ) = ( v |` suc g ) ) <-> ( -. u  ( u |` suc G ) = ( v |` suc G ) ) ) )
37 36 ralbidv 
 |-  ( g = G -> ( A. v e. B ( -. u  ( u |` suc g ) = ( v |` suc g ) ) <-> A. v e. B ( -. u  ( u |` suc G ) = ( v |` suc G ) ) ) )
38 fveqeq2 
 |-  ( g = G -> ( ( u ` g ) = x <-> ( u ` G ) = x ) )
39 31 37 38 3anbi123d 
 |-  ( g = G -> ( ( g e. dom u /\ A. v e. B ( -. u  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) <-> ( G e. dom u /\ A. v e. B ( -. u  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) ) )
40 39 rexbidv 
 |-  ( g = G -> ( E. u e. B ( g e. dom u /\ A. v e. B ( -. u  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) <-> E. u e. B ( G e. dom u /\ A. v e. B ( -. u  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) ) )
41 40 iotabidv 
 |-  ( g = G -> ( iota x E. u e. B ( g e. dom u /\ A. v e. B ( -. u  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) = ( iota x E. u e. B ( G e. dom u /\ A. v e. B ( -. u  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) ) )
42 eqid 
 |-  ( g e. { y | E. u e. B ( y e. dom u /\ A. v e. B ( -. u  ( u |` suc y ) = ( v |` suc y ) ) ) } |-> ( iota x E. u e. B ( g e. dom u /\ A. v e. B ( -. u  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) ) = ( g e. { y | E. u e. B ( y e. dom u /\ A. v e. B ( -. u  ( u |` suc y ) = ( v |` suc y ) ) ) } |-> ( iota x E. u e. B ( g e. dom u /\ A. v e. B ( -. u  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) )
43 iotaex 
 |-  ( iota x E. u e. B ( G e. dom u /\ A. v e. B ( -. u  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) ) e. _V
44 41 42 43 fvmpt 
 |-  ( G e. { y | E. u e. B ( y e. dom u /\ A. v e. B ( -. u  ( u |` suc y ) = ( v |` suc y ) ) ) } -> ( ( g e. { y | E. u e. B ( y e. dom u /\ A. v e. B ( -. u  ( u |` suc y ) = ( v |` suc y ) ) ) } |-> ( iota x E. u e. B ( g e. dom u /\ A. v e. B ( -. u  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) ) ` G ) = ( iota x E. u e. B ( G e. dom u /\ A. v e. B ( -. u  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) ) )
45 30 44 syl 
 |-  ( ( -. E. x e. B A. y e. B -. y  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> ( ( g e. { y | E. u e. B ( y e. dom u /\ A. v e. B ( -. u  ( u |` suc y ) = ( v |` suc y ) ) ) } |-> ( iota x E. u e. B ( g e. dom u /\ A. v e. B ( -. u  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) ) ` G ) = ( iota x E. u e. B ( G e. dom u /\ A. v e. B ( -. u  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) ) )
46 simp1 
 |-  ( ( U e. B /\ G e. dom U /\ A. v e. B ( -. U  ( U |` suc G ) = ( v |` suc G ) ) ) -> U e. B )
47 simp2 
 |-  ( ( U e. B /\ G e. dom U /\ A. v e. B ( -. U  ( U |` suc G ) = ( v |` suc G ) ) ) -> G e. dom U )
48 simp3 
 |-  ( ( U e. B /\ G e. dom U /\ A. v e. B ( -. U  ( U |` suc G ) = ( v |` suc G ) ) ) -> A. v e. B ( -. U  ( U |` suc G ) = ( v |` suc G ) ) )
49 eqidd 
 |-  ( ( U e. B /\ G e. dom U /\ A. v e. B ( -. U  ( 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 e. dom u /\ A. v e. B ( -. u  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = ( U ` G ) ) <-> ( G e. dom U /\ A. v e. B ( -. U  ( U |` suc G ) = ( v |` suc G ) ) /\ ( U ` G ) = ( U ` G ) ) ) )
53 52 rspcev 
 |-  ( ( U e. B /\ ( G e. dom U /\ A. v e. B ( -. U  ( U |` suc G ) = ( v |` suc G ) ) /\ ( U ` G ) = ( U ` G ) ) ) -> E. u e. B ( G e. dom u /\ A. v e. B ( -. u  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = ( U ` G ) ) )
54 46 47 48 49 53 syl13anc 
 |-  ( ( U e. B /\ G e. dom U /\ A. v e. B ( -. U  ( U |` suc G ) = ( v |` suc G ) ) ) -> E. u e. B ( G e. dom u /\ A. v e. B ( -. u  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = ( U ` G ) ) )
55 54 3ad2ant3 
 |-  ( ( -. E. x e. B A. y e. B -. y  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> E. u e. B ( G e. dom u /\ A. v e. B ( -. u  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = ( U ` G ) ) )
56 fvex 
 |-  ( U ` G ) e. _V
57 eqid 
 |-  ( u ` G ) = ( u ` G )
58 fvex 
 |-  ( u ` G ) e. _V
59 eqeq2 
 |-  ( x = ( u ` G ) -> ( ( u ` G ) = x <-> ( u ` G ) = ( u ` G ) ) )
60 59 3anbi3d 
 |-  ( x = ( u ` G ) -> ( ( G e. dom u /\ A. v e. B ( -. u  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) <-> ( G e. dom u /\ A. v e. B ( -. u  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = ( u ` G ) ) ) )
61 58 60 spcev 
 |-  ( ( G e. dom u /\ A. v e. B ( -. u  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = ( u ` G ) ) -> E. x ( G e. dom u /\ A. v e. B ( -. u  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) )
62 57 61 mp3an3 
 |-  ( ( G e. dom u /\ A. v e. B ( -. u  ( u |` suc G ) = ( v |` suc G ) ) ) -> E. x ( G e. dom u /\ A. v e. B ( -. u  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) )
63 62 reximi 
 |-  ( E. u e. B ( G e. dom u /\ A. v e. B ( -. u  ( u |` suc G ) = ( v |` suc G ) ) ) -> E. u e. B E. x ( G e. dom u /\ A. v e. B ( -. u  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) )
64 rexcom4 
 |-  ( E. u e. B E. x ( G e. dom u /\ A. v e. B ( -. u  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) <-> E. x E. u e. B ( G e. dom u /\ A. v e. B ( -. u  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) )
65 63 64 sylib 
 |-  ( E. u e. B ( G e. dom u /\ A. v e. B ( -. u  ( u |` suc G ) = ( v |` suc G ) ) ) -> E. x E. u e. B ( G e. dom u /\ A. v e. B ( -. u  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) )
66 16 65 syl 
 |-  ( ( U e. B /\ G e. dom U /\ A. v e. B ( -. U  ( U |` suc G ) = ( v |` suc G ) ) ) -> E. x E. u e. B ( G e. dom u /\ A. v e. B ( -. u  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) )
67 66 3ad2ant3 
 |-  ( ( -. E. x e. B A. y e. B -. y  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> E. x E. u e. B ( G e. dom u /\ A. v e. B ( -. u  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) )
68 simp2l 
 |-  ( ( -. E. x e. B A. y e. B -. y  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> B C_ No )
69 noinfprefixmo 
 |-  ( B C_ No -> E* x E. u e. B ( G e. dom u /\ A. v e. B ( -. u  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) )
70 68 69 syl 
 |-  ( ( -. E. x e. B A. y e. B -. y  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> E* x E. u e. B ( G e. dom u /\ A. v e. B ( -. u  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) )
71 df-eu 
 |-  ( E! x E. u e. B ( G e. dom u /\ A. v e. B ( -. u  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) <-> ( E. x E. u e. B ( G e. dom u /\ A. v e. B ( -. u  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ E* x E. u e. B ( G e. dom u /\ A. v e. B ( -. u  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) ) )
72 67 70 71 sylanbrc 
 |-  ( ( -. E. x e. B A. y e. B -. y  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> E! x E. u e. B ( G e. dom u /\ A. v e. B ( -. u  ( 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 e. dom u /\ A. v e. B ( -. u  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) <-> ( G e. dom u /\ A. v e. B ( -. u  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = ( U ` G ) ) ) )
75 74 rexbidv 
 |-  ( x = ( U ` G ) -> ( E. u e. B ( G e. dom u /\ A. v e. B ( -. u  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) <-> E. u e. B ( G e. dom u /\ A. v e. B ( -. u  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = ( U ` G ) ) ) )
76 75 iota2 
 |-  ( ( ( U ` G ) e. _V /\ E! x E. u e. B ( G e. dom u /\ A. v e. B ( -. u  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) ) -> ( E. u e. B ( G e. dom u /\ A. v e. B ( -. u  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = ( U ` G ) ) <-> ( iota x E. u e. B ( G e. dom u /\ A. v e. B ( -. u  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) ) = ( U ` G ) ) )
77 56 72 76 sylancr 
 |-  ( ( -. E. x e. B A. y e. B -. y  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> ( E. u e. B ( G e. dom u /\ A. v e. B ( -. u  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = ( U ` G ) ) <-> ( iota x E. u e. B ( G e. dom u /\ A. v e. B ( -. u  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) ) = ( U ` G ) ) )
78 55 77 mpbid 
 |-  ( ( -. E. x e. B A. y e. B -. y  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> ( iota x E. u e. B ( G e. dom u /\ A. v e. B ( -. u  ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) ) = ( U ` G ) )
79 5 45 78 3eqtrd 
 |-  ( ( -. E. x e. B A. y e. B -. y  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> ( T ` G ) = ( U ` G ) )