Metamath Proof Explorer

Theorem noinfbnd2

Description: Bounding law from below for the surreal infimum. Analagous to proposition 4.3 of Lipparini p. 6. (Contributed by Scott Fenton, 9-Aug-2024)

Ref Expression
Hypothesis noinfbnd2.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 noinfbnd2 
|- ( ( B C_ No /\ B e. V /\ Z e. No ) -> ( A. b e. B Z  -. T

Proof

Step Hyp Ref Expression
1 noinfbnd2.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 nfv 
 |-  F/ x ( ( B C_ No /\ B e. V /\ Z e. No ) /\ A. b e. B Z
3 nfre1 
 |-  F/ x E. x e. B A. y e. B -. y
4 nfriota1 
 |-  F/_ x ( iota_ x e. B A. y e. B -. y
5 4 nfdm 
 |-  F/_ x dom ( iota_ x e. B A. y e. B -. y
6 nfcv 
 |-  F/_ x 1o
7 5 6 nfop 
 |-  F/_ x <. dom ( iota_ x e. B A. y e. B -. y .
8 7 nfsn 
 |-  F/_ x { <. dom ( iota_ x e. B A. y e. B -. y . }
9 4 8 nfun 
 |-  F/_ x ( ( iota_ x e. B A. y e. B -. y . } )
10 nfcv 
 |-  F/_ x { y | E. u e. B ( y e. dom u /\ A. v e. B ( -. u  ( u |` suc y ) = ( v |` suc y ) ) ) }
11 nfiota1 
 |-  F/_ 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 ) )
12 10 11 nfmpt 
 |-  F/_ 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 ) ) )
13 3 9 12 nfif 
 |-  F/_ x 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 ) ) ) )
14 1 13 nfcxfr 
 |-  F/_ x T
15 nfcv 
 |-  F/_ x
16 nfcv 
 |-  F/_ x Z
17 14 nfdm 
 |-  F/_ x dom T
18 16 17 nfres 
 |-  F/_ x ( Z |` dom T )
19 14 15 18 nfbr 
 |-  F/ x T
20 19 nfn 
 |-  F/ x -. T
21 2 20 nfim 
 |-  F/ x ( ( ( B C_ No /\ B e. V /\ Z e. No ) /\ A. b e. B Z  -. T
22 noinfbnd2lem1 
 |-  ( ( ( x e. B /\ A. y e. B -. y  -. ( x u. { <. dom x , 1o >. } )
23 22 3expb 
 |-  ( ( ( x e. B /\ A. y e. B -. y  -. ( x u. { <. dom x , 1o >. } )
24 rspe 
 |-  ( ( x e. B /\ A. y e. B -. y  E. x e. B A. y e. B -. y
25 24 adantr 
 |-  ( ( ( x e. B /\ A. y e. B -. y  E. x e. B A. y e. B -. y
26 25 iftrued 
 |-  ( ( ( 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 ) ) ) ) = ( ( iota_ x e. B A. y e. B -. y . } ) )
27 simpl 
 |-  ( ( ( x e. B /\ A. y e. B -. y  ( x e. B /\ A. y e. B -. y
28 simprl1 
 |-  ( ( ( x e. B /\ A. y e. B -. y  B C_ No )
29 nominmo 
 |-  ( B C_ No -> E* x e. B A. y e. B -. y
30 28 29 syl 
 |-  ( ( ( x e. B /\ A. y e. B -. y  E* x e. B A. y e. B -. y
31 reu5 
 |-  ( E! x e. B A. y e. B -. y  ( E. x e. B A. y e. B -. y
32 25 30 31 sylanbrc 
 |-  ( ( ( x e. B /\ A. y e. B -. y  E! x e. B A. y e. B -. y
33 riota1 
 |-  ( E! x e. B A. y e. B -. y  ( ( x e. B /\ A. y e. B -. y  ( iota_ x e. B A. y e. B -. y
34 32 33 syl 
 |-  ( ( ( x e. B /\ A. y e. B -. y  ( ( x e. B /\ A. y e. B -. y  ( iota_ x e. B A. y e. B -. y
35 27 34 mpbid 
 |-  ( ( ( x e. B /\ A. y e. B -. y  ( iota_ x e. B A. y e. B -. y
36 35 dmeqd 
 |-  ( ( ( x e. B /\ A. y e. B -. y  dom ( iota_ x e. B A. y e. B -. y
37 36 opeq1d 
 |-  ( ( ( x e. B /\ A. y e. B -. y  <. dom ( iota_ x e. B A. y e. B -. y . = <. dom x , 1o >. )
38 37 sneqd 
 |-  ( ( ( x e. B /\ A. y e. B -. y  { <. dom ( iota_ x e. B A. y e. B -. y . } = { <. dom x , 1o >. } )
39 35 38 uneq12d 
 |-  ( ( ( x e. B /\ A. y e. B -. y  ( ( iota_ x e. B A. y e. B -. y . } ) = ( x u. { <. dom x , 1o >. } ) )
40 26 39 eqtrd 
 |-  ( ( ( 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 ) ) ) ) = ( x u. { <. dom x , 1o >. } ) )
41 1 40 syl5eq 
 |-  ( ( ( x e. B /\ A. y e. B -. y  T = ( x u. { <. dom x , 1o >. } ) )
42 41 dmeqd 
 |-  ( ( ( x e. B /\ A. y e. B -. y  dom T = dom ( x u. { <. dom x , 1o >. } ) )
43 1oex 
 |-  1o e. _V
44 43 dmsnop 
 |-  dom { <. dom x , 1o >. } = { dom x }
45 44 uneq2i 
 |-  ( dom x u. dom { <. dom x , 1o >. } ) = ( dom x u. { dom x } )
46 dmun 
 |-  dom ( x u. { <. dom x , 1o >. } ) = ( dom x u. dom { <. dom x , 1o >. } )
47 df-suc 
 |-  suc dom x = ( dom x u. { dom x } )
48 45 46 47 3eqtr4ri 
 |-  suc dom x = dom ( x u. { <. dom x , 1o >. } )
49 42 48 eqtr4di 
 |-  ( ( ( x e. B /\ A. y e. B -. y  dom T = suc dom x )
50 49 reseq2d 
 |-  ( ( ( x e. B /\ A. y e. B -. y  ( Z |` dom T ) = ( Z |` suc dom x ) )
51 41 50 breq12d 
 |-  ( ( ( x e. B /\ A. y e. B -. y  ( T  ( x u. { <. dom x , 1o >. } )
52 23 51 mtbird 
 |-  ( ( ( x e. B /\ A. y e. B -. y  -. T
53 52 exp31 
 |-  ( x e. B -> ( A. y e. B -. y  ( ( ( B C_ No /\ B e. V /\ Z e. No ) /\ A. b e. B Z  -. T
54 21 53 rexlimi 
 |-  ( E. x e. B A. y e. B -. y  ( ( ( B C_ No /\ B e. V /\ Z e. No ) /\ A. b e. B Z  -. T
55 54 imp 
 |-  ( ( E. x e. B A. y e. B -. y  -. T
56 simprl3 
 |-  ( ( -. E. x e. B A. y e. B -. y  Z e. No )
57 1 noinfno 
 |-  ( ( B C_ No /\ B e. V ) -> T e. No )
58 57 3adant3 
 |-  ( ( B C_ No /\ B e. V /\ Z e. No ) -> T e. No )
59 58 ad2antrl 
 |-  ( ( -. E. x e. B A. y e. B -. y  T e. No )
60 nodmon 
 |-  ( T e. No -> dom T e. On )
61 59 60 syl 
 |-  ( ( -. E. x e. B A. y e. B -. y  dom T e. On )
62 noreson 
 |-  ( ( Z e. No /\ dom T e. On ) -> ( Z |` dom T ) e. No )
63 56 61 62 syl2anc 
 |-  ( ( -. E. x e. B A. y e. B -. y  ( Z |` dom T ) e. No )
64 nofun 
 |-  ( T e. No -> Fun T )
65 funrel 
 |-  ( Fun T -> Rel T )
66 58 64 65 3syl 
 |-  ( ( B C_ No /\ B e. V /\ Z e. No ) -> Rel T )
67 66 ad2antrl 
 |-  ( ( -. E. x e. B A. y e. B -. y  Rel T )
68 resdm 
 |-  ( Rel T -> ( T |` dom T ) = T )
69 67 68 syl 
 |-  ( ( -. E. x e. B A. y e. B -. y  ( T |` dom T ) = T )
70 69 59 eqeltrd 
 |-  ( ( -. E. x e. B A. y e. B -. y  ( T |` dom T ) e. No )
71 resdmss 
 |-  dom ( Z |` dom T ) C_ dom T
72 71 a1i 
 |-  ( ( -. E. x e. B A. y e. B -. y  dom ( Z |` dom T ) C_ dom T )
73 resdmss 
 |-  dom ( T |` dom T ) C_ dom T
74 73 a1i 
 |-  ( ( -. E. x e. B A. y e. B -. y  dom ( T |` dom T ) C_ dom T )
75 1 noinfdm 
 |-  ( -. E. x e. B A. y e. B -. y  dom T = { g | E. p e. B ( g e. dom p /\ A. q e. B ( -. p  ( p |` suc g ) = ( q |` suc g ) ) ) } )
76 75 abeq2d 
 |-  ( -. E. x e. B A. y e. B -. y  ( g e. dom T <-> E. p e. B ( g e. dom p /\ A. q e. B ( -. p  ( p |` suc g ) = ( q |` suc g ) ) ) ) )
77 76 adantr 
 |-  ( ( -. E. x e. B A. y e. B -. y  ( g e. dom T <-> E. p e. B ( g e. dom p /\ A. q e. B ( -. p  ( p |` suc g ) = ( q |` suc g ) ) ) ) )
78 simpll 
 |-  ( ( ( -. E. x e. B A. y e. B -. y  ( p |` suc g ) = ( q |` suc g ) ) ) ) ) -> -. E. x e. B A. y e. B -. y
79 simprl1 
 |-  ( ( -. E. x e. B A. y e. B -. y  B C_ No )
80 79 adantr 
 |-  ( ( ( -. E. x e. B A. y e. B -. y  ( p |` suc g ) = ( q |` suc g ) ) ) ) ) -> B C_ No )
81 simprl2 
 |-  ( ( -. E. x e. B A. y e. B -. y  B e. V )
82 81 adantr 
 |-  ( ( ( -. E. x e. B A. y e. B -. y  ( p |` suc g ) = ( q |` suc g ) ) ) ) ) -> B e. V )
83 simprl 
 |-  ( ( ( -. E. x e. B A. y e. B -. y  ( p |` suc g ) = ( q |` suc g ) ) ) ) ) -> p e. B )
84 simprrl 
 |-  ( ( ( -. E. x e. B A. y e. B -. y  ( p |` suc g ) = ( q |` suc g ) ) ) ) ) -> g e. dom p )
85 simprrr 
 |-  ( ( ( -. E. x e. B A. y e. B -. y  ( p |` suc g ) = ( q |` suc g ) ) ) ) ) -> A. q e. B ( -. p  ( p |` suc g ) = ( q |` suc g ) ) )
86 breq2 
 |-  ( q = v -> ( p  p
87 86 notbid 
 |-  ( q = v -> ( -. p  -. p
88 reseq1 
 |-  ( q = v -> ( q |` suc g ) = ( v |` suc g ) )
89 88 eqeq2d 
 |-  ( q = v -> ( ( p |` suc g ) = ( q |` suc g ) <-> ( p |` suc g ) = ( v |` suc g ) ) )
90 87 89 imbi12d 
 |-  ( q = v -> ( ( -. p  ( p |` suc g ) = ( q |` suc g ) ) <-> ( -. p  ( p |` suc g ) = ( v |` suc g ) ) ) )
91 90 cbvralvw 
 |-  ( A. q e. B ( -. p  ( p |` suc g ) = ( q |` suc g ) ) <-> A. v e. B ( -. p  ( p |` suc g ) = ( v |` suc g ) ) )
92 85 91 sylib 
 |-  ( ( ( -. E. x e. B A. y e. B -. y  ( p |` suc g ) = ( q |` suc g ) ) ) ) ) -> A. v e. B ( -. p  ( p |` suc g ) = ( v |` suc g ) ) )
93 1 noinfres 
 |-  ( ( -. E. x e. B A. y e. B -. y  ( p |` suc g ) = ( v |` suc g ) ) ) ) -> ( T |` suc g ) = ( p |` suc g ) )
94 78 80 82 83 84 92 93 syl123anc 
 |-  ( ( ( -. E. x e. B A. y e. B -. y  ( p |` suc g ) = ( q |` suc g ) ) ) ) ) -> ( T |` suc g ) = ( p |` suc g ) )
95 breq2 
 |-  ( b = p -> ( Z  Z
96 simplrr 
 |-  ( ( ( -. E. x e. B A. y e. B -. y  ( p |` suc g ) = ( q |` suc g ) ) ) ) ) -> A. b e. B Z
97 95 96 83 rspcdva 
 |-  ( ( ( -. E. x e. B A. y e. B -. y  ( p |` suc g ) = ( q |` suc g ) ) ) ) ) -> Z
98 56 adantr 
 |-  ( ( ( -. E. x e. B A. y e. B -. y  ( p |` suc g ) = ( q |` suc g ) ) ) ) ) -> Z e. No )
99 80 83 sseldd 
 |-  ( ( ( -. E. x e. B A. y e. B -. y  ( p |` suc g ) = ( q |` suc g ) ) ) ) ) -> p e. No )
100 sltso 
 |-
101 soasym 
 |-  ( (  ( Z  -. p
102 100 101 mpan 
 |-  ( ( Z e. No /\ p e. No ) -> ( Z  -. p
103 98 99 102 syl2anc 
 |-  ( ( ( -. E. x e. B A. y e. B -. y  ( p |` suc g ) = ( q |` suc g ) ) ) ) ) -> ( Z  -. p
104 97 103 mpd 
 |-  ( ( ( -. E. x e. B A. y e. B -. y  ( p |` suc g ) = ( q |` suc g ) ) ) ) ) -> -. p
105 nodmon 
 |-  ( p e. No -> dom p e. On )
106 99 105 syl 
 |-  ( ( ( -. E. x e. B A. y e. B -. y  ( p |` suc g ) = ( q |` suc g ) ) ) ) ) -> dom p e. On )
107 onelon 
 |-  ( ( dom p e. On /\ g e. dom p ) -> g e. On )
108 106 84 107 syl2anc 
 |-  ( ( ( -. E. x e. B A. y e. B -. y  ( p |` suc g ) = ( q |` suc g ) ) ) ) ) -> g e. On )
109 sucelon 
 |-  ( g e. On <-> suc g e. On )
110 108 109 sylib 
 |-  ( ( ( -. E. x e. B A. y e. B -. y  ( p |` suc g ) = ( q |` suc g ) ) ) ) ) -> suc g e. On )
111 sltres 
 |-  ( ( p e. No /\ Z e. No /\ suc g e. On ) -> ( ( p |` suc g )  p
112 99 98 110 111 syl3anc 
 |-  ( ( ( -. E. x e. B A. y e. B -. y  ( p |` suc g ) = ( q |` suc g ) ) ) ) ) -> ( ( p |` suc g )  p
113 104 112 mtod 
 |-  ( ( ( -. E. x e. B A. y e. B -. y  ( p |` suc g ) = ( q |` suc g ) ) ) ) ) -> -. ( p |` suc g )
114 94 113 eqnbrtrd 
 |-  ( ( ( -. E. x e. B A. y e. B -. y  ( p |` suc g ) = ( q |` suc g ) ) ) ) ) -> -. ( T |` suc g )
115 114 rexlimdvaa 
 |-  ( ( -. E. x e. B A. y e. B -. y  ( E. p e. B ( g e. dom p /\ A. q e. B ( -. p  ( p |` suc g ) = ( q |` suc g ) ) ) -> -. ( T |` suc g )
116 77 115 sylbid 
 |-  ( ( -. E. x e. B A. y e. B -. y  ( g e. dom T -> -. ( T |` suc g )
117 116 imp 
 |-  ( ( ( -. E. x e. B A. y e. B -. y  -. ( T |` suc g )
118 nodmord 
 |-  ( T e. No -> Ord dom T )
119 ordsucss 
 |-  ( Ord dom T -> ( g e. dom T -> suc g C_ dom T ) )
120 59 118 119 3syl 
 |-  ( ( -. E. x e. B A. y e. B -. y  ( g e. dom T -> suc g C_ dom T ) )
121 120 imp 
 |-  ( ( ( -. E. x e. B A. y e. B -. y  suc g C_ dom T )
122 121 resabs1d 
 |-  ( ( ( -. E. x e. B A. y e. B -. y  ( ( T |` dom T ) |` suc g ) = ( T |` suc g ) )
123 121 resabs1d 
 |-  ( ( ( -. E. x e. B A. y e. B -. y  ( ( Z |` dom T ) |` suc g ) = ( Z |` suc g ) )
124 122 123 breq12d 
 |-  ( ( ( -. E. x e. B A. y e. B -. y  ( ( ( T |` dom T ) |` suc g )  ( T |` suc g )
125 117 124 mtbird 
 |-  ( ( ( -. E. x e. B A. y e. B -. y  -. ( ( T |` dom T ) |` suc g )
126 125 ralrimiva 
 |-  ( ( -. E. x e. B A. y e. B -. y  A. g e. dom T -. ( ( T |` dom T ) |` suc g )
127 noresle 
 |-  ( ( ( ( Z |` dom T ) e. No /\ ( T |` dom T ) e. No ) /\ ( dom ( Z |` dom T ) C_ dom T /\ dom ( T |` dom T ) C_ dom T /\ A. g e. dom T -. ( ( T |` dom T ) |` suc g )  -. ( T |` dom T )
128 63 70 72 74 126 127 syl23anc 
 |-  ( ( -. E. x e. B A. y e. B -. y  -. ( T |` dom T )
129 69 breq1d 
 |-  ( ( -. E. x e. B A. y e. B -. y  ( ( T |` dom T )  T
130 128 129 mtbid 
 |-  ( ( -. E. x e. B A. y e. B -. y  -. T
131 55 130 pm2.61ian 
 |-  ( ( ( B C_ No /\ B e. V /\ Z e. No ) /\ A. b e. B Z  -. T
132 simplr 
 |-  ( ( ( ( B C_ No /\ B e. V /\ Z e. No ) /\ -. T  -. T
133 simpll1 
 |-  ( ( ( ( B C_ No /\ B e. V /\ Z e. No ) /\ -. T  B C_ No )
134 simpll2 
 |-  ( ( ( ( B C_ No /\ B e. V /\ Z e. No ) /\ -. T  B e. V )
135 simpr 
 |-  ( ( ( ( B C_ No /\ B e. V /\ Z e. No ) /\ -. T  b e. B )
136 1 noinfbnd1 
 |-  ( ( B C_ No /\ B e. V /\ b e. B ) -> T
137 133 134 135 136 syl3anc 
 |-  ( ( ( ( B C_ No /\ B e. V /\ Z e. No ) /\ -. T  T
138 simpl3 
 |-  ( ( ( B C_ No /\ B e. V /\ Z e. No ) /\ -. T  Z e. No )
139 simpl1 
 |-  ( ( ( B C_ No /\ B e. V /\ Z e. No ) /\ -. T  B C_ No )
140 simpl2 
 |-  ( ( ( B C_ No /\ B e. V /\ Z e. No ) /\ -. T  B e. V )
141 139 140 57 syl2anc 
 |-  ( ( ( B C_ No /\ B e. V /\ Z e. No ) /\ -. T  T e. No )
142 141 60 syl 
 |-  ( ( ( B C_ No /\ B e. V /\ Z e. No ) /\ -. T  dom T e. On )
143 138 142 62 syl2anc 
 |-  ( ( ( B C_ No /\ B e. V /\ Z e. No ) /\ -. T  ( Z |` dom T ) e. No )
144 143 adantr 
 |-  ( ( ( ( B C_ No /\ B e. V /\ Z e. No ) /\ -. T  ( Z |` dom T ) e. No )
145 141 adantr 
 |-  ( ( ( ( B C_ No /\ B e. V /\ Z e. No ) /\ -. T  T e. No )
146 139 sselda 
 |-  ( ( ( ( B C_ No /\ B e. V /\ Z e. No ) /\ -. T  b e. No )
147 142 adantr 
 |-  ( ( ( ( B C_ No /\ B e. V /\ Z e. No ) /\ -. T  dom T e. On )
148 noreson 
 |-  ( ( b e. No /\ dom T e. On ) -> ( b |` dom T ) e. No )
149 146 147 148 syl2anc 
 |-  ( ( ( ( B C_ No /\ B e. V /\ Z e. No ) /\ -. T  ( b |` dom T ) e. No )
150 sotr2 
 |-  ( (  ( ( -. T  ( Z |` dom T )
151 100 150 mpan 
 |-  ( ( ( Z |` dom T ) e. No /\ T e. No /\ ( b |` dom T ) e. No ) -> ( ( -. T  ( Z |` dom T )
152 144 145 149 151 syl3anc 
 |-  ( ( ( ( B C_ No /\ B e. V /\ Z e. No ) /\ -. T  ( ( -. T  ( Z |` dom T )
153 132 137 152 mp2and 
 |-  ( ( ( ( B C_ No /\ B e. V /\ Z e. No ) /\ -. T  ( Z |` dom T )
154 simpll3 
 |-  ( ( ( ( B C_ No /\ B e. V /\ Z e. No ) /\ -. T  Z e. No )
155 sltres 
 |-  ( ( Z e. No /\ b e. No /\ dom T e. On ) -> ( ( Z |` dom T )  Z
156 154 146 147 155 syl3anc 
 |-  ( ( ( ( B C_ No /\ B e. V /\ Z e. No ) /\ -. T  ( ( Z |` dom T )  Z
157 153 156 mpd 
 |-  ( ( ( ( B C_ No /\ B e. V /\ Z e. No ) /\ -. T  Z
158 157 ralrimiva 
 |-  ( ( ( B C_ No /\ B e. V /\ Z e. No ) /\ -. T  A. b e. B Z
159 131 158 impbida 
 |-  ( ( B C_ No /\ B e. V /\ Z e. No ) -> ( A. b e. B Z  -. T