Metamath Proof Explorer

Theorem noinfres

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

Ref Expression
Hypothesis noinfres.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 noinfres 
|- ( ( -. E. x e. B A. y e. B -. y  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> ( T |` suc G ) = ( U |` suc G ) )

Proof

Step Hyp Ref Expression
1 noinfres.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 dmres 
 |-  dom ( T |` suc G ) = ( suc G i^i dom T )
3 1 noinfno 
 |-  ( ( B C_ No /\ B e. V ) -> T e. No )
4 3 3ad2ant2 
 |-  ( ( -. E. x e. B A. y e. B -. y  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> T e. No )
5 nodmord 
 |-  ( T e. No -> Ord dom T )
6 4 5 syl 
 |-  ( ( -. E. x e. B A. y e. B -. y  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> Ord dom T )
7 simp31 
 |-  ( ( -. E. x e. B A. y e. B -. y  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> U e. B )
8 simp32 
 |-  ( ( -. E. x e. B A. y e. B -. y  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> G e. dom U )
9 simp33 
 |-  ( ( -. E. x e. B A. y e. B -. y  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> A. v e. B ( -. U  ( U |` suc G ) = ( v |` suc G ) ) )
10 dmeq 
 |-  ( b = U -> dom b = dom U )
11 10 eleq2d 
 |-  ( b = U -> ( G e. dom b <-> G e. dom U ) )
12 breq1 
 |-  ( b = U -> ( b  U
13 12 notbid 
 |-  ( b = U -> ( -. b  -. U
14 reseq1 
 |-  ( b = U -> ( b |` suc G ) = ( U |` suc G ) )
15 14 eqeq1d 
 |-  ( b = U -> ( ( b |` suc G ) = ( c |` suc G ) <-> ( U |` suc G ) = ( c |` suc G ) ) )
16 13 15 imbi12d 
 |-  ( b = U -> ( ( -. b  ( b |` suc G ) = ( c |` suc G ) ) <-> ( -. U  ( U |` suc G ) = ( c |` suc G ) ) ) )
17 16 ralbidv 
 |-  ( b = U -> ( A. c e. B ( -. b  ( b |` suc G ) = ( c |` suc G ) ) <-> A. c e. B ( -. U  ( U |` suc G ) = ( c |` suc G ) ) ) )
18 breq2 
 |-  ( c = v -> ( U  U
19 18 notbid 
 |-  ( c = v -> ( -. U  -. U
20 reseq1 
 |-  ( c = v -> ( c |` suc G ) = ( v |` suc G ) )
21 20 eqeq2d 
 |-  ( c = v -> ( ( U |` suc G ) = ( c |` suc G ) <-> ( U |` suc G ) = ( v |` suc G ) ) )
22 19 21 imbi12d 
 |-  ( c = v -> ( ( -. U  ( U |` suc G ) = ( c |` suc G ) ) <-> ( -. U  ( U |` suc G ) = ( v |` suc G ) ) ) )
23 22 cbvralvw 
 |-  ( A. c e. B ( -. U  ( U |` suc G ) = ( c |` suc G ) ) <-> A. v e. B ( -. U  ( U |` suc G ) = ( v |` suc G ) ) )
24 17 23 bitrdi 
 |-  ( b = U -> ( A. c e. B ( -. b  ( b |` suc G ) = ( c |` suc G ) ) <-> A. v e. B ( -. U  ( U |` suc G ) = ( v |` suc G ) ) ) )
25 11 24 anbi12d 
 |-  ( b = U -> ( ( G e. dom b /\ A. c e. B ( -. b  ( b |` suc G ) = ( c |` suc G ) ) ) <-> ( G e. dom U /\ A. v e. B ( -. U  ( U |` suc G ) = ( v |` suc G ) ) ) ) )
26 25 rspcev 
 |-  ( ( U e. B /\ ( G e. dom U /\ A. v e. B ( -. U  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> E. b e. B ( G e. dom b /\ A. c e. B ( -. b  ( b |` suc G ) = ( c |` suc G ) ) ) )
27 7 8 9 26 syl12anc 
 |-  ( ( -. E. x e. B A. y e. B -. y  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> E. b e. B ( G e. dom b /\ A. c e. B ( -. b  ( b |` suc G ) = ( c |` suc G ) ) ) )
28 eleq1 
 |-  ( a = G -> ( a e. dom b <-> G e. dom b ) )
29 suceq 
 |-  ( a = G -> suc a = suc G )
30 29 reseq2d 
 |-  ( a = G -> ( b |` suc a ) = ( b |` suc G ) )
31 29 reseq2d 
 |-  ( a = G -> ( c |` suc a ) = ( c |` suc G ) )
32 30 31 eqeq12d 
 |-  ( a = G -> ( ( b |` suc a ) = ( c |` suc a ) <-> ( b |` suc G ) = ( c |` suc G ) ) )
33 32 imbi2d 
 |-  ( a = G -> ( ( -. b  ( b |` suc a ) = ( c |` suc a ) ) <-> ( -. b  ( b |` suc G ) = ( c |` suc G ) ) ) )
34 33 ralbidv 
 |-  ( a = G -> ( A. c e. B ( -. b  ( b |` suc a ) = ( c |` suc a ) ) <-> A. c e. B ( -. b  ( b |` suc G ) = ( c |` suc G ) ) ) )
35 28 34 anbi12d 
 |-  ( a = G -> ( ( a e. dom b /\ A. c e. B ( -. b  ( b |` suc a ) = ( c |` suc a ) ) ) <-> ( G e. dom b /\ A. c e. B ( -. b  ( b |` suc G ) = ( c |` suc G ) ) ) ) )
36 35 rexbidv 
 |-  ( a = G -> ( E. b e. B ( a e. dom b /\ A. c e. B ( -. b  ( b |` suc a ) = ( c |` suc a ) ) ) <-> E. b e. B ( G e. dom b /\ A. c e. B ( -. b  ( b |` suc G ) = ( c |` suc G ) ) ) ) )
37 36 elabg 
 |-  ( G e. dom U -> ( G e. { a | E. b e. B ( a e. dom b /\ A. c e. B ( -. b  ( b |` suc a ) = ( c |` suc a ) ) ) } <-> E. b e. B ( G e. dom b /\ A. c e. B ( -. b  ( b |` suc G ) = ( c |` suc G ) ) ) ) )
38 8 37 syl 
 |-  ( ( -. E. x e. B A. y e. B -. y  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> ( G e. { a | E. b e. B ( a e. dom b /\ A. c e. B ( -. b  ( b |` suc a ) = ( c |` suc a ) ) ) } <-> E. b e. B ( G e. dom b /\ A. c e. B ( -. b  ( b |` suc G ) = ( c |` suc G ) ) ) ) )
39 27 38 mpbird 
 |-  ( ( -. E. x e. B A. y e. B -. y  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> G e. { a | E. b e. B ( a e. dom b /\ A. c e. B ( -. b  ( b |` suc a ) = ( c |` suc a ) ) ) } )
40 1 noinfdm 
 |-  ( -. E. x e. B A. y e. B -. y  dom T = { a | E. b e. B ( a e. dom b /\ A. c e. B ( -. b  ( b |` suc a ) = ( c |` suc a ) ) ) } )
41 40 3ad2ant1 
 |-  ( ( -. E. x e. B A. y e. B -. y  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> dom T = { a | E. b e. B ( a e. dom b /\ A. c e. B ( -. b  ( b |` suc a ) = ( c |` suc a ) ) ) } )
42 39 41 eleqtrrd 
 |-  ( ( -. E. x e. B A. y e. B -. y  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> G e. dom T )
43 ordsucss 
 |-  ( Ord dom T -> ( G e. dom T -> suc G C_ dom T ) )
44 6 42 43 sylc 
 |-  ( ( -. E. x e. B A. y e. B -. y  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> suc G C_ dom T )
45 df-ss 
 |-  ( suc G C_ dom T <-> ( suc G i^i dom T ) = suc G )
46 44 45 sylib 
 |-  ( ( -. E. x e. B A. y e. B -. y  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> ( suc G i^i dom T ) = suc G )
47 2 46 syl5eq 
 |-  ( ( -. E. x e. B A. y e. B -. y  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> dom ( T |` suc G ) = suc G )
48 dmres 
 |-  dom ( U |` suc G ) = ( suc G i^i dom U )
49 simp2l 
 |-  ( ( -. E. x e. B A. y e. B -. y  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> B C_ No )
50 49 7 sseldd 
 |-  ( ( -. E. x e. B A. y e. B -. y  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> U e. No )
51 nodmon 
 |-  ( U e. No -> dom U e. On )
52 50 51 syl 
 |-  ( ( -. E. x e. B A. y e. B -. y  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> dom U e. On )
53 eloni 
 |-  ( dom U e. On -> Ord dom U )
54 52 53 syl 
 |-  ( ( -. E. x e. B A. y e. B -. y  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> Ord dom U )
55 ordsucss 
 |-  ( Ord dom U -> ( G e. dom U -> suc G C_ dom U ) )
56 54 8 55 sylc 
 |-  ( ( -. E. x e. B A. y e. B -. y  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> suc G C_ dom U )
57 df-ss 
 |-  ( suc G C_ dom U <-> ( suc G i^i dom U ) = suc G )
58 56 57 sylib 
 |-  ( ( -. E. x e. B A. y e. B -. y  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> ( suc G i^i dom U ) = suc G )
59 48 58 syl5eq 
 |-  ( ( -. E. x e. B A. y e. B -. y  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> dom ( U |` suc G ) = suc G )
60 47 59 eqtr4d 
 |-  ( ( -. E. x e. B A. y e. B -. y  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> dom ( T |` suc G ) = dom ( U |` suc G ) )
61 47 eleq2d 
 |-  ( ( -. E. x e. B A. y e. B -. y  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> ( a e. dom ( T |` suc G ) <-> a e. suc G ) )
62 simpl1 
 |-  ( ( ( -. E. x e. B A. y e. B -. y  ( U |` suc G ) = ( v |` suc G ) ) ) ) /\ a e. suc G ) -> -. E. x e. B A. y e. B -. y
63 simpl2 
 |-  ( ( ( -. E. x e. B A. y e. B -. y  ( U |` suc G ) = ( v |` suc G ) ) ) ) /\ a e. suc G ) -> ( B C_ No /\ B e. V ) )
64 simpl31 
 |-  ( ( ( -. E. x e. B A. y e. B -. y  ( U |` suc G ) = ( v |` suc G ) ) ) ) /\ a e. suc G ) -> U e. B )
65 56 sselda 
 |-  ( ( ( -. E. x e. B A. y e. B -. y  ( U |` suc G ) = ( v |` suc G ) ) ) ) /\ a e. suc G ) -> a e. dom U )
66 50 adantr 
 |-  ( ( ( -. E. x e. B A. y e. B -. y  ( U |` suc G ) = ( v |` suc G ) ) ) ) /\ a e. suc G ) -> U e. No )
67 66 51 syl 
 |-  ( ( ( -. E. x e. B A. y e. B -. y  ( U |` suc G ) = ( v |` suc G ) ) ) ) /\ a e. suc G ) -> dom U e. On )
68 simpl32 
 |-  ( ( ( -. E. x e. B A. y e. B -. y  ( U |` suc G ) = ( v |` suc G ) ) ) ) /\ a e. suc G ) -> G e. dom U )
69 onelon 
 |-  ( ( dom U e. On /\ G e. dom U ) -> G e. On )
70 67 68 69 syl2anc 
 |-  ( ( ( -. E. x e. B A. y e. B -. y  ( U |` suc G ) = ( v |` suc G ) ) ) ) /\ a e. suc G ) -> G e. On )
71 sucelon 
 |-  ( G e. On <-> suc G e. On )
72 70 71 sylib 
 |-  ( ( ( -. E. x e. B A. y e. B -. y  ( U |` suc G ) = ( v |` suc G ) ) ) ) /\ a e. suc G ) -> suc G e. On )
73 eloni 
 |-  ( suc G e. On -> Ord suc G )
74 72 73 syl 
 |-  ( ( ( -. E. x e. B A. y e. B -. y  ( U |` suc G ) = ( v |` suc G ) ) ) ) /\ a e. suc G ) -> Ord suc G )
75 simpr 
 |-  ( ( ( -. E. x e. B A. y e. B -. y  ( U |` suc G ) = ( v |` suc G ) ) ) ) /\ a e. suc G ) -> a e. suc G )
76 ordsucss 
 |-  ( Ord suc G -> ( a e. suc G -> suc a C_ suc G ) )
77 74 75 76 sylc 
 |-  ( ( ( -. E. x e. B A. y e. B -. y  ( U |` suc G ) = ( v |` suc G ) ) ) ) /\ a e. suc G ) -> suc a C_ suc G )
78 simpl33 
 |-  ( ( ( -. E. x e. B A. y e. B -. y  ( U |` suc G ) = ( v |` suc G ) ) ) ) /\ a e. suc G ) -> A. v e. B ( -. U  ( U |` suc G ) = ( v |` suc G ) ) )
79 reseq1 
 |-  ( ( U |` suc G ) = ( v |` suc G ) -> ( ( U |` suc G ) |` suc a ) = ( ( v |` suc G ) |` suc a ) )
80 resabs1 
 |-  ( suc a C_ suc G -> ( ( U |` suc G ) |` suc a ) = ( U |` suc a ) )
81 resabs1 
 |-  ( suc a C_ suc G -> ( ( v |` suc G ) |` suc a ) = ( v |` suc a ) )
82 80 81 eqeq12d 
 |-  ( suc a C_ suc G -> ( ( ( U |` suc G ) |` suc a ) = ( ( v |` suc G ) |` suc a ) <-> ( U |` suc a ) = ( v |` suc a ) ) )
83 79 82 syl5ib 
 |-  ( suc a C_ suc G -> ( ( U |` suc G ) = ( v |` suc G ) -> ( U |` suc a ) = ( v |` suc a ) ) )
84 83 imim2d 
 |-  ( suc a C_ suc G -> ( ( -. U  ( U |` suc G ) = ( v |` suc G ) ) -> ( -. U  ( U |` suc a ) = ( v |` suc a ) ) ) )
85 84 ralimdv 
 |-  ( suc a C_ suc G -> ( A. v e. B ( -. U  ( U |` suc G ) = ( v |` suc G ) ) -> A. v e. B ( -. U  ( U |` suc a ) = ( v |` suc a ) ) ) )
86 77 78 85 sylc 
 |-  ( ( ( -. E. x e. B A. y e. B -. y  ( U |` suc G ) = ( v |` suc G ) ) ) ) /\ a e. suc G ) -> A. v e. B ( -. U  ( U |` suc a ) = ( v |` suc a ) ) )
87 1 noinffv 
 |-  ( ( -. E. x e. B A. y e. B -. y  ( U |` suc a ) = ( v |` suc a ) ) ) ) -> ( T ` a ) = ( U ` a ) )
88 62 63 64 65 86 87 syl113anc 
 |-  ( ( ( -. E. x e. B A. y e. B -. y  ( U |` suc G ) = ( v |` suc G ) ) ) ) /\ a e. suc G ) -> ( T ` a ) = ( U ` a ) )
89 75 fvresd 
 |-  ( ( ( -. E. x e. B A. y e. B -. y  ( U |` suc G ) = ( v |` suc G ) ) ) ) /\ a e. suc G ) -> ( ( T |` suc G ) ` a ) = ( T ` a ) )
90 75 fvresd 
 |-  ( ( ( -. E. x e. B A. y e. B -. y  ( U |` suc G ) = ( v |` suc G ) ) ) ) /\ a e. suc G ) -> ( ( U |` suc G ) ` a ) = ( U ` a ) )
91 88 89 90 3eqtr4d 
 |-  ( ( ( -. E. x e. B A. y e. B -. y  ( U |` suc G ) = ( v |` suc G ) ) ) ) /\ a e. suc G ) -> ( ( T |` suc G ) ` a ) = ( ( U |` suc G ) ` a ) )
92 91 ex 
 |-  ( ( -. E. x e. B A. y e. B -. y  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> ( a e. suc G -> ( ( T |` suc G ) ` a ) = ( ( U |` suc G ) ` a ) ) )
93 61 92 sylbid 
 |-  ( ( -. E. x e. B A. y e. B -. y  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> ( a e. dom ( T |` suc G ) -> ( ( T |` suc G ) ` a ) = ( ( U |` suc G ) ` a ) ) )
94 93 ralrimiv 
 |-  ( ( -. E. x e. B A. y e. B -. y  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> A. a e. dom ( T |` suc G ) ( ( T |` suc G ) ` a ) = ( ( U |` suc G ) ` a ) )
95 nofun 
 |-  ( T e. No -> Fun T )
96 95 funresd 
 |-  ( T e. No -> Fun ( T |` suc G ) )
97 4 96 syl 
 |-  ( ( -. E. x e. B A. y e. B -. y  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> Fun ( T |` suc G ) )
98 nofun 
 |-  ( U e. No -> Fun U )
99 98 funresd 
 |-  ( U e. No -> Fun ( U |` suc G ) )
100 50 99 syl 
 |-  ( ( -. E. x e. B A. y e. B -. y  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> Fun ( U |` suc G ) )
101 eqfunfv 
 |-  ( ( Fun ( T |` suc G ) /\ Fun ( U |` suc G ) ) -> ( ( T |` suc G ) = ( U |` suc G ) <-> ( dom ( T |` suc G ) = dom ( U |` suc G ) /\ A. a e. dom ( T |` suc G ) ( ( T |` suc G ) ` a ) = ( ( U |` suc G ) ` a ) ) ) )
102 97 100 101 syl2anc 
 |-  ( ( -. E. x e. B A. y e. B -. y  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> ( ( T |` suc G ) = ( U |` suc G ) <-> ( dom ( T |` suc G ) = dom ( U |` suc G ) /\ A. a e. dom ( T |` suc G ) ( ( T |` suc G ) ` a ) = ( ( U |` suc G ) ` a ) ) ) )
103 60 94 102 mpbir2and 
 |-  ( ( -. E. x e. B A. y e. B -. y  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> ( T |` suc G ) = ( U |` suc G ) )