Metamath Proof Explorer

Theorem noinfbnd1

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

Ref Expression
Hypothesis noinfbnd1.1 ⊢T=if∃x∈B∀y∈B¬y<sxιx∈B|∀y∈B¬y<sx∪dom⁡ιx∈B|∀y∈B¬y<sx1𝑜g∈y|∃u∈By∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y⟼ιx|∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=x
Assertion noinfbnd1 ⊢B⊆No∧B∈V∧U∈B→T<sU↾dom⁡T

Proof

Step Hyp Ref Expression
1 noinfbnd1.1 ⊢T=if∃x∈B∀y∈B¬y<sxιx∈B|∀y∈B¬y<sx∪dom⁡ιx∈B|∀y∈B¬y<sx1𝑜g∈y|∃u∈By∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y⟼ιx|∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=x
2 simpr1 ⊢∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B→B⊆No
3 simpl ⊢∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B→∃x∈B∀y∈B¬y<sx
4 nominmo ⊢B⊆No→∃*x∈B∀y∈B¬y<sx
5 2 4 syl ⊢∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B→∃*x∈B∀y∈B¬y<sx
6 reu5 ⊢∃!x∈B∀y∈B¬y<sx↔∃x∈B∀y∈B¬y<sx∧∃*x∈B∀y∈B¬y<sx
7 3 5 6 sylanbrc ⊢∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B→∃!x∈B∀y∈B¬y<sx
8 riotacl ⊢∃!x∈B∀y∈B¬y<sx→ιx∈B|∀y∈B¬y<sx∈B
9 7 8 syl ⊢∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B→ιx∈B|∀y∈B¬y<sx∈B
10 2 9 sseldd ⊢∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B→ιx∈B|∀y∈B¬y<sx∈No
11 noextendlt ⊢ιx∈B|∀y∈B¬y<sx∈No→ιx∈B|∀y∈B¬y<sx∪dom⁡ιx∈B|∀y∈B¬y<sx1𝑜<sιx∈B|∀y∈B¬y<sx
12 10 11 syl ⊢∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B→ιx∈B|∀y∈B¬y<sx∪dom⁡ιx∈B|∀y∈B¬y<sx1𝑜<sιx∈B|∀y∈B¬y<sx
13 simpr3 ⊢∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B→U∈B
14 nfv ⊢ℲxB⊆No∧B∈V∧U∈B
15 nfcv ⊢Ⅎ_xB
16 nfcv ⊢Ⅎ_xy
17 nfcv ⊢Ⅎ_x<s
18 nfriota1 ⊢Ⅎ_xιx∈B|∀y∈B¬y<sx
19 16 17 18 nfbr ⊢Ⅎxy<sιx∈B|∀y∈B¬y<sx
20 19 nfn ⊢Ⅎx¬y<sιx∈B|∀y∈B¬y<sx
21 15 20 nfralw ⊢Ⅎx∀y∈B¬y<sιx∈B|∀y∈B¬y<sx
22 14 21 nfim ⊢ℲxB⊆No∧B∈V∧U∈B→∀y∈B¬y<sιx∈B|∀y∈B¬y<sx
23 simpl ⊢x∈B∧∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B→x∈B∧∀y∈B¬y<sx
24 rspe ⊢x∈B∧∀y∈B¬y<sx→∃x∈B∀y∈B¬y<sx
25 24 adantr ⊢x∈B∧∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B→∃x∈B∀y∈B¬y<sx
26 simpr1 ⊢x∈B∧∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B→B⊆No
27 26 4 syl ⊢x∈B∧∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B→∃*x∈B∀y∈B¬y<sx
28 25 27 6 sylanbrc ⊢x∈B∧∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B→∃!x∈B∀y∈B¬y<sx
29 riota1 ⊢∃!x∈B∀y∈B¬y<sx→x∈B∧∀y∈B¬y<sx↔ιx∈B|∀y∈B¬y<sx=x
30 28 29 syl ⊢x∈B∧∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B→x∈B∧∀y∈B¬y<sx↔ιx∈B|∀y∈B¬y<sx=x
31 23 30 mpbid ⊢x∈B∧∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B→ιx∈B|∀y∈B¬y<sx=x
32 simplr ⊢x∈B∧∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B→∀y∈B¬y<sx
33 nfra1 ⊢Ⅎy∀y∈B¬y<sx
34 nfcv ⊢Ⅎ_yB
35 33 34 nfriota ⊢Ⅎ_yιx∈B|∀y∈B¬y<sx
36 35 nfeq1 ⊢Ⅎyιx∈B|∀y∈B¬y<sx=x
37 breq2 ⊢ιx∈B|∀y∈B¬y<sx=x→y<sιx∈B|∀y∈B¬y<sx↔y<sx
38 37 notbid ⊢ιx∈B|∀y∈B¬y<sx=x→¬y<sιx∈B|∀y∈B¬y<sx↔¬y<sx
39 36 38 ralbid ⊢ιx∈B|∀y∈B¬y<sx=x→∀y∈B¬y<sιx∈B|∀y∈B¬y<sx↔∀y∈B¬y<sx
40 39 biimprd ⊢ιx∈B|∀y∈B¬y<sx=x→∀y∈B¬y<sx→∀y∈B¬y<sιx∈B|∀y∈B¬y<sx
41 31 32 40 sylc ⊢x∈B∧∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B→∀y∈B¬y<sιx∈B|∀y∈B¬y<sx
42 41 exp31 ⊢x∈B→∀y∈B¬y<sx→B⊆No∧B∈V∧U∈B→∀y∈B¬y<sιx∈B|∀y∈B¬y<sx
43 22 42 rexlimi ⊢∃x∈B∀y∈B¬y<sx→B⊆No∧B∈V∧U∈B→∀y∈B¬y<sιx∈B|∀y∈B¬y<sx
44 43 imp ⊢∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B→∀y∈B¬y<sιx∈B|∀y∈B¬y<sx
45 nfcv ⊢Ⅎ_yU
46 nfcv ⊢Ⅎ_y<s
47 45 46 35 nfbr ⊢ℲyU<sιx∈B|∀y∈B¬y<sx
48 47 nfn ⊢Ⅎy¬U<sιx∈B|∀y∈B¬y<sx
49 breq1 ⊢y=U→y<sιx∈B|∀y∈B¬y<sx↔U<sιx∈B|∀y∈B¬y<sx
50 49 notbid ⊢y=U→¬y<sιx∈B|∀y∈B¬y<sx↔¬U<sιx∈B|∀y∈B¬y<sx
51 48 50 rspc ⊢U∈B→∀y∈B¬y<sιx∈B|∀y∈B¬y<sx→¬U<sιx∈B|∀y∈B¬y<sx
52 13 44 51 sylc ⊢∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B→¬U<sιx∈B|∀y∈B¬y<sx
53 nofun ⊢ιx∈B|∀y∈B¬y<sx∈No→Fun⁡ιx∈B|∀y∈B¬y<sx
54 funrel ⊢Fun⁡ιx∈B|∀y∈B¬y<sx→Rel⁡ιx∈B|∀y∈B¬y<sx
55 10 53 54 3syl ⊢∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B→Rel⁡ιx∈B|∀y∈B¬y<sx
56 sssucid ⊢dom⁡ιx∈B|∀y∈B¬y<sx⊆suc⁡dom⁡ιx∈B|∀y∈B¬y<sx
57 relssres ⊢Rel⁡ιx∈B|∀y∈B¬y<sx∧dom⁡ιx∈B|∀y∈B¬y<sx⊆suc⁡dom⁡ιx∈B|∀y∈B¬y<sx→ιx∈B|∀y∈B¬y<sx↾suc⁡dom⁡ιx∈B|∀y∈B¬y<sx=ιx∈B|∀y∈B¬y<sx
58 55 56 57 sylancl ⊢∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B→ιx∈B|∀y∈B¬y<sx↾suc⁡dom⁡ιx∈B|∀y∈B¬y<sx=ιx∈B|∀y∈B¬y<sx
59 58 breq2d ⊢∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B→U↾suc⁡dom⁡ιx∈B|∀y∈B¬y<sx<sιx∈B|∀y∈B¬y<sx↾suc⁡dom⁡ιx∈B|∀y∈B¬y<sx↔U↾suc⁡dom⁡ιx∈B|∀y∈B¬y<sx<sιx∈B|∀y∈B¬y<sx
60 2 13 sseldd ⊢∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B→U∈No
61 nodmon ⊢ιx∈B|∀y∈B¬y<sx∈No→dom⁡ιx∈B|∀y∈B¬y<sx∈On
62 10 61 syl ⊢∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B→dom⁡ιx∈B|∀y∈B¬y<sx∈On
63 onsucb ⊢dom⁡ιx∈B|∀y∈B¬y<sx∈On↔suc⁡dom⁡ιx∈B|∀y∈B¬y<sx∈On
64 62 63 sylib ⊢∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B→suc⁡dom⁡ιx∈B|∀y∈B¬y<sx∈On
65 sltres ⊢U∈No∧ιx∈B|∀y∈B¬y<sx∈No∧suc⁡dom⁡ιx∈B|∀y∈B¬y<sx∈On→U↾suc⁡dom⁡ιx∈B|∀y∈B¬y<sx<sιx∈B|∀y∈B¬y<sx↾suc⁡dom⁡ιx∈B|∀y∈B¬y<sx→U<sιx∈B|∀y∈B¬y<sx
66 60 10 64 65 syl3anc ⊢∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B→U↾suc⁡dom⁡ιx∈B|∀y∈B¬y<sx<sιx∈B|∀y∈B¬y<sx↾suc⁡dom⁡ιx∈B|∀y∈B¬y<sx→U<sιx∈B|∀y∈B¬y<sx
67 59 66 sylbird ⊢∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B→U↾suc⁡dom⁡ιx∈B|∀y∈B¬y<sx<sιx∈B|∀y∈B¬y<sx→U<sιx∈B|∀y∈B¬y<sx
68 52 67 mtod ⊢∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B→¬U↾suc⁡dom⁡ιx∈B|∀y∈B¬y<sx<sιx∈B|∀y∈B¬y<sx
69 1oex ⊢1𝑜∈V
70 69 prid1 ⊢1𝑜∈1𝑜2𝑜
71 70 noextend ⊢ιx∈B|∀y∈B¬y<sx∈No→ιx∈B|∀y∈B¬y<sx∪dom⁡ιx∈B|∀y∈B¬y<sx1𝑜∈No
72 10 71 syl ⊢∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B→ιx∈B|∀y∈B¬y<sx∪dom⁡ιx∈B|∀y∈B¬y<sx1𝑜∈No
73 noreson ⊢U∈No∧suc⁡dom⁡ιx∈B|∀y∈B¬y<sx∈On→U↾suc⁡dom⁡ιx∈B|∀y∈B¬y<sx∈No
74 60 64 73 syl2anc ⊢∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B→U↾suc⁡dom⁡ιx∈B|∀y∈B¬y<sx∈No
75 sltso ⊢<sOrNo
76 sotr3 ⊢<sOrNo∧ιx∈B|∀y∈B¬y<sx∪dom⁡ιx∈B|∀y∈B¬y<sx1𝑜∈No∧ιx∈B|∀y∈B¬y<sx∈No∧U↾suc⁡dom⁡ιx∈B|∀y∈B¬y<sx∈No→ιx∈B|∀y∈B¬y<sx∪dom⁡ιx∈B|∀y∈B¬y<sx1𝑜<sιx∈B|∀y∈B¬y<sx∧¬U↾suc⁡dom⁡ιx∈B|∀y∈B¬y<sx<sιx∈B|∀y∈B¬y<sx→ιx∈B|∀y∈B¬y<sx∪dom⁡ιx∈B|∀y∈B¬y<sx1𝑜<sU↾suc⁡dom⁡ιx∈B|∀y∈B¬y<sx
77 75 76 mpan ⊢ιx∈B|∀y∈B¬y<sx∪dom⁡ιx∈B|∀y∈B¬y<sx1𝑜∈No∧ιx∈B|∀y∈B¬y<sx∈No∧U↾suc⁡dom⁡ιx∈B|∀y∈B¬y<sx∈No→ιx∈B|∀y∈B¬y<sx∪dom⁡ιx∈B|∀y∈B¬y<sx1𝑜<sιx∈B|∀y∈B¬y<sx∧¬U↾suc⁡dom⁡ιx∈B|∀y∈B¬y<sx<sιx∈B|∀y∈B¬y<sx→ιx∈B|∀y∈B¬y<sx∪dom⁡ιx∈B|∀y∈B¬y<sx1𝑜<sU↾suc⁡dom⁡ιx∈B|∀y∈B¬y<sx
78 72 10 74 77 syl3anc ⊢∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B→ιx∈B|∀y∈B¬y<sx∪dom⁡ιx∈B|∀y∈B¬y<sx1𝑜<sιx∈B|∀y∈B¬y<sx∧¬U↾suc⁡dom⁡ιx∈B|∀y∈B¬y<sx<sιx∈B|∀y∈B¬y<sx→ιx∈B|∀y∈B¬y<sx∪dom⁡ιx∈B|∀y∈B¬y<sx1𝑜<sU↾suc⁡dom⁡ιx∈B|∀y∈B¬y<sx
79 12 68 78 mp2and ⊢∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B→ιx∈B|∀y∈B¬y<sx∪dom⁡ιx∈B|∀y∈B¬y<sx1𝑜<sU↾suc⁡dom⁡ιx∈B|∀y∈B¬y<sx
80 iftrue ⊢∃x∈B∀y∈B¬y<sx→if∃x∈B∀y∈B¬y<sxιx∈B|∀y∈B¬y<sx∪dom⁡ιx∈B|∀y∈B¬y<sx1𝑜g∈y|∃u∈By∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y⟼ιx|∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=x=ιx∈B|∀y∈B¬y<sx∪dom⁡ιx∈B|∀y∈B¬y<sx1𝑜
81 1 80 eqtrid ⊢∃x∈B∀y∈B¬y<sx→T=ιx∈B|∀y∈B¬y<sx∪dom⁡ιx∈B|∀y∈B¬y<sx1𝑜
82 81 adantr ⊢∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B→T=ιx∈B|∀y∈B¬y<sx∪dom⁡ιx∈B|∀y∈B¬y<sx1𝑜
83 81 dmeqd ⊢∃x∈B∀y∈B¬y<sx→dom⁡T=dom⁡ιx∈B|∀y∈B¬y<sx∪dom⁡ιx∈B|∀y∈B¬y<sx1𝑜
84 69 dmsnop ⊢dom⁡dom⁡ιx∈B|∀y∈B¬y<sx1𝑜=dom⁡ιx∈B|∀y∈B¬y<sx
85 84 uneq2i ⊢dom⁡ιx∈B|∀y∈B¬y<sx∪dom⁡dom⁡ιx∈B|∀y∈B¬y<sx1𝑜=dom⁡ιx∈B|∀y∈B¬y<sx∪dom⁡ιx∈B|∀y∈B¬y<sx
86 dmun ⊢dom⁡ιx∈B|∀y∈B¬y<sx∪dom⁡ιx∈B|∀y∈B¬y<sx1𝑜=dom⁡ιx∈B|∀y∈B¬y<sx∪dom⁡dom⁡ιx∈B|∀y∈B¬y<sx1𝑜
87 df-suc ⊢suc⁡dom⁡ιx∈B|∀y∈B¬y<sx=dom⁡ιx∈B|∀y∈B¬y<sx∪dom⁡ιx∈B|∀y∈B¬y<sx
88 85 86 87 3eqtr4i ⊢dom⁡ιx∈B|∀y∈B¬y<sx∪dom⁡ιx∈B|∀y∈B¬y<sx1𝑜=suc⁡dom⁡ιx∈B|∀y∈B¬y<sx
89 83 88 eqtrdi ⊢∃x∈B∀y∈B¬y<sx→dom⁡T=suc⁡dom⁡ιx∈B|∀y∈B¬y<sx
90 89 reseq2d ⊢∃x∈B∀y∈B¬y<sx→U↾dom⁡T=U↾suc⁡dom⁡ιx∈B|∀y∈B¬y<sx
91 90 adantr ⊢∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B→U↾dom⁡T=U↾suc⁡dom⁡ιx∈B|∀y∈B¬y<sx
92 79 82 91 3brtr4d ⊢∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B→T<sU↾dom⁡T
93 simpl ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B→¬∃x∈B∀y∈B¬y<sx
94 simpr1 ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B→B⊆No
95 simpr2 ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B→B∈V
96 simpr3 ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B→U∈B
97 1 noinfbnd1lem6 ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B→T<sU↾dom⁡T
98 93 94 95 96 97 syl121anc ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B→T<sU↾dom⁡T
99 92 98 pm2.61ian ⊢B⊆No∧B∈V∧U∈B→T<sU↾dom⁡T