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∃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 noinfres ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧G∈dom⁡U∧∀v∈B¬U<sv→U↾suc⁡G=v↾suc⁡G→T↾suc⁡G=U↾suc⁡G

Proof

Step Hyp Ref Expression
1 noinfres.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 dmres ⊢dom⁡T↾suc⁡G=suc⁡G∩dom⁡T
3 1 noinfno ⊢B⊆No∧B∈V→T∈No
4 3 3ad2ant2 ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧G∈dom⁡U∧∀v∈B¬U<sv→U↾suc⁡G=v↾suc⁡G→T∈No
5 nodmord ⊢T∈No→Ord⁡dom⁡T
6 4 5 syl ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧G∈dom⁡U∧∀v∈B¬U<sv→U↾suc⁡G=v↾suc⁡G→Ord⁡dom⁡T
7 simp31 ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧G∈dom⁡U∧∀v∈B¬U<sv→U↾suc⁡G=v↾suc⁡G→U∈B
8 simp32 ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧G∈dom⁡U∧∀v∈B¬U<sv→U↾suc⁡G=v↾suc⁡G→G∈dom⁡U
9 simp33 ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧G∈dom⁡U∧∀v∈B¬U<sv→U↾suc⁡G=v↾suc⁡G→∀v∈B¬U<sv→U↾suc⁡G=v↾suc⁡G
10 dmeq ⊢b=U→dom⁡b=dom⁡U
11 10 eleq2d ⊢b=U→G∈dom⁡b↔G∈dom⁡U
12 breq1 ⊢b=U→b<sc↔U<sc
13 12 notbid ⊢b=U→¬b<sc↔¬U<sc
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<sc→b↾suc⁡G=c↾suc⁡G↔¬U<sc→U↾suc⁡G=c↾suc⁡G
17 16 ralbidv ⊢b=U→∀c∈B¬b<sc→b↾suc⁡G=c↾suc⁡G↔∀c∈B¬U<sc→U↾suc⁡G=c↾suc⁡G
18 breq2 ⊢c=v→U<sc↔U<sv
19 18 notbid ⊢c=v→¬U<sc↔¬U<sv
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<sc→U↾suc⁡G=c↾suc⁡G↔¬U<sv→U↾suc⁡G=v↾suc⁡G
23 22 cbvralvw ⊢∀c∈B¬U<sc→U↾suc⁡G=c↾suc⁡G↔∀v∈B¬U<sv→U↾suc⁡G=v↾suc⁡G
24 17 23 bitrdi ⊢b=U→∀c∈B¬b<sc→b↾suc⁡G=c↾suc⁡G↔∀v∈B¬U<sv→U↾suc⁡G=v↾suc⁡G
25 11 24 anbi12d ⊢b=U→G∈dom⁡b∧∀c∈B¬b<sc→b↾suc⁡G=c↾suc⁡G↔G∈dom⁡U∧∀v∈B¬U<sv→U↾suc⁡G=v↾suc⁡G
26 25 rspcev ⊢U∈B∧G∈dom⁡U∧∀v∈B¬U<sv→U↾suc⁡G=v↾suc⁡G→∃b∈BG∈dom⁡b∧∀c∈B¬b<sc→b↾suc⁡G=c↾suc⁡G
27 7 8 9 26 syl12anc ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧G∈dom⁡U∧∀v∈B¬U<sv→U↾suc⁡G=v↾suc⁡G→∃b∈BG∈dom⁡b∧∀c∈B¬b<sc→b↾suc⁡G=c↾suc⁡G
28 eleq1 ⊢a=G→a∈dom⁡b↔G∈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<sc→b↾suc⁡a=c↾suc⁡a↔¬b<sc→b↾suc⁡G=c↾suc⁡G
34 33 ralbidv ⊢a=G→∀c∈B¬b<sc→b↾suc⁡a=c↾suc⁡a↔∀c∈B¬b<sc→b↾suc⁡G=c↾suc⁡G
35 28 34 anbi12d ⊢a=G→a∈dom⁡b∧∀c∈B¬b<sc→b↾suc⁡a=c↾suc⁡a↔G∈dom⁡b∧∀c∈B¬b<sc→b↾suc⁡G=c↾suc⁡G
36 35 rexbidv ⊢a=G→∃b∈Ba∈dom⁡b∧∀c∈B¬b<sc→b↾suc⁡a=c↾suc⁡a↔∃b∈BG∈dom⁡b∧∀c∈B¬b<sc→b↾suc⁡G=c↾suc⁡G
37 36 elabg ⊢G∈dom⁡U→G∈a|∃b∈Ba∈dom⁡b∧∀c∈B¬b<sc→b↾suc⁡a=c↾suc⁡a↔∃b∈BG∈dom⁡b∧∀c∈B¬b<sc→b↾suc⁡G=c↾suc⁡G
38 8 37 syl ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧G∈dom⁡U∧∀v∈B¬U<sv→U↾suc⁡G=v↾suc⁡G→G∈a|∃b∈Ba∈dom⁡b∧∀c∈B¬b<sc→b↾suc⁡a=c↾suc⁡a↔∃b∈BG∈dom⁡b∧∀c∈B¬b<sc→b↾suc⁡G=c↾suc⁡G
39 27 38 mpbird ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧G∈dom⁡U∧∀v∈B¬U<sv→U↾suc⁡G=v↾suc⁡G→G∈a|∃b∈Ba∈dom⁡b∧∀c∈B¬b<sc→b↾suc⁡a=c↾suc⁡a
40 1 noinfdm ⊢¬∃x∈B∀y∈B¬y<sx→dom⁡T=a|∃b∈Ba∈dom⁡b∧∀c∈B¬b<sc→b↾suc⁡a=c↾suc⁡a
41 40 3ad2ant1 ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧G∈dom⁡U∧∀v∈B¬U<sv→U↾suc⁡G=v↾suc⁡G→dom⁡T=a|∃b∈Ba∈dom⁡b∧∀c∈B¬b<sc→b↾suc⁡a=c↾suc⁡a
42 39 41 eleqtrrd ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧G∈dom⁡U∧∀v∈B¬U<sv→U↾suc⁡G=v↾suc⁡G→G∈dom⁡T
43 ordsucss ⊢Ord⁡dom⁡T→G∈dom⁡T→suc⁡G⊆dom⁡T
44 6 42 43 sylc ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧G∈dom⁡U∧∀v∈B¬U<sv→U↾suc⁡G=v↾suc⁡G→suc⁡G⊆dom⁡T
45 df-ss ⊢suc⁡G⊆dom⁡T↔suc⁡G∩dom⁡T=suc⁡G
46 44 45 sylib ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧G∈dom⁡U∧∀v∈B¬U<sv→U↾suc⁡G=v↾suc⁡G→suc⁡G∩dom⁡T=suc⁡G
47 2 46 eqtrid ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧G∈dom⁡U∧∀v∈B¬U<sv→U↾suc⁡G=v↾suc⁡G→dom⁡T↾suc⁡G=suc⁡G
48 dmres ⊢dom⁡U↾suc⁡G=suc⁡G∩dom⁡U
49 simp2l ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧G∈dom⁡U∧∀v∈B¬U<sv→U↾suc⁡G=v↾suc⁡G→B⊆No
50 49 7 sseldd ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧G∈dom⁡U∧∀v∈B¬U<sv→U↾suc⁡G=v↾suc⁡G→U∈No
51 nodmon ⊢U∈No→dom⁡U∈On
52 50 51 syl ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧G∈dom⁡U∧∀v∈B¬U<sv→U↾suc⁡G=v↾suc⁡G→dom⁡U∈On
53 eloni ⊢dom⁡U∈On→Ord⁡dom⁡U
54 52 53 syl ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧G∈dom⁡U∧∀v∈B¬U<sv→U↾suc⁡G=v↾suc⁡G→Ord⁡dom⁡U
55 ordsucss ⊢Ord⁡dom⁡U→G∈dom⁡U→suc⁡G⊆dom⁡U
56 54 8 55 sylc ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧G∈dom⁡U∧∀v∈B¬U<sv→U↾suc⁡G=v↾suc⁡G→suc⁡G⊆dom⁡U
57 df-ss ⊢suc⁡G⊆dom⁡U↔suc⁡G∩dom⁡U=suc⁡G
58 56 57 sylib ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧G∈dom⁡U∧∀v∈B¬U<sv→U↾suc⁡G=v↾suc⁡G→suc⁡G∩dom⁡U=suc⁡G
59 48 58 eqtrid ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧G∈dom⁡U∧∀v∈B¬U<sv→U↾suc⁡G=v↾suc⁡G→dom⁡U↾suc⁡G=suc⁡G
60 47 59 eqtr4d ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧G∈dom⁡U∧∀v∈B¬U<sv→U↾suc⁡G=v↾suc⁡G→dom⁡T↾suc⁡G=dom⁡U↾suc⁡G
61 47 eleq2d ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧G∈dom⁡U∧∀v∈B¬U<sv→U↾suc⁡G=v↾suc⁡G→a∈dom⁡T↾suc⁡G↔a∈suc⁡G
62 simpl1 ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧G∈dom⁡U∧∀v∈B¬U<sv→U↾suc⁡G=v↾suc⁡G∧a∈suc⁡G→¬∃x∈B∀y∈B¬y<sx
63 simpl2 ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧G∈dom⁡U∧∀v∈B¬U<sv→U↾suc⁡G=v↾suc⁡G∧a∈suc⁡G→B⊆No∧B∈V
64 simpl31 ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧G∈dom⁡U∧∀v∈B¬U<sv→U↾suc⁡G=v↾suc⁡G∧a∈suc⁡G→U∈B
65 56 sselda ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧G∈dom⁡U∧∀v∈B¬U<sv→U↾suc⁡G=v↾suc⁡G∧a∈suc⁡G→a∈dom⁡U
66 50 adantr ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧G∈dom⁡U∧∀v∈B¬U<sv→U↾suc⁡G=v↾suc⁡G∧a∈suc⁡G→U∈No
67 66 51 syl ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧G∈dom⁡U∧∀v∈B¬U<sv→U↾suc⁡G=v↾suc⁡G∧a∈suc⁡G→dom⁡U∈On
68 simpl32 ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧G∈dom⁡U∧∀v∈B¬U<sv→U↾suc⁡G=v↾suc⁡G∧a∈suc⁡G→G∈dom⁡U
69 onelon ⊢dom⁡U∈On∧G∈dom⁡U→G∈On
70 67 68 69 syl2anc ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧G∈dom⁡U∧∀v∈B¬U<sv→U↾suc⁡G=v↾suc⁡G∧a∈suc⁡G→G∈On
71 onsucb ⊢G∈On↔suc⁡G∈On
72 70 71 sylib ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧G∈dom⁡U∧∀v∈B¬U<sv→U↾suc⁡G=v↾suc⁡G∧a∈suc⁡G→suc⁡G∈On
73 eloni ⊢suc⁡G∈On→Ord⁡suc⁡G
74 72 73 syl ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧G∈dom⁡U∧∀v∈B¬U<sv→U↾suc⁡G=v↾suc⁡G∧a∈suc⁡G→Ord⁡suc⁡G
75 simpr ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧G∈dom⁡U∧∀v∈B¬U<sv→U↾suc⁡G=v↾suc⁡G∧a∈suc⁡G→a∈suc⁡G
76 ordsucss ⊢Ord⁡suc⁡G→a∈suc⁡G→suc⁡a⊆suc⁡G
77 74 75 76 sylc ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧G∈dom⁡U∧∀v∈B¬U<sv→U↾suc⁡G=v↾suc⁡G∧a∈suc⁡G→suc⁡a⊆suc⁡G
78 simpl33 ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧G∈dom⁡U∧∀v∈B¬U<sv→U↾suc⁡G=v↾suc⁡G∧a∈suc⁡G→∀v∈B¬U<sv→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⊆suc⁡G→U↾suc⁡G↾suc⁡a=U↾suc⁡a
81 resabs1 ⊢suc⁡a⊆suc⁡G→v↾suc⁡G↾suc⁡a=v↾suc⁡a
82 80 81 eqeq12d ⊢suc⁡a⊆suc⁡G→U↾suc⁡G↾suc⁡a=v↾suc⁡G↾suc⁡a↔U↾suc⁡a=v↾suc⁡a
83 79 82 imbitrid ⊢suc⁡a⊆suc⁡G→U↾suc⁡G=v↾suc⁡G→U↾suc⁡a=v↾suc⁡a
84 83 imim2d ⊢suc⁡a⊆suc⁡G→¬U<sv→U↾suc⁡G=v↾suc⁡G→¬U<sv→U↾suc⁡a=v↾suc⁡a
85 84 ralimdv ⊢suc⁡a⊆suc⁡G→∀v∈B¬U<sv→U↾suc⁡G=v↾suc⁡G→∀v∈B¬U<sv→U↾suc⁡a=v↾suc⁡a
86 77 78 85 sylc ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧G∈dom⁡U∧∀v∈B¬U<sv→U↾suc⁡G=v↾suc⁡G∧a∈suc⁡G→∀v∈B¬U<sv→U↾suc⁡a=v↾suc⁡a
87 1 noinffv ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧a∈dom⁡U∧∀v∈B¬U<sv→U↾suc⁡a=v↾suc⁡a→T⁡a=U⁡a
88 62 63 64 65 86 87 syl113anc ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧G∈dom⁡U∧∀v∈B¬U<sv→U↾suc⁡G=v↾suc⁡G∧a∈suc⁡G→T⁡a=U⁡a
89 75 fvresd ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧G∈dom⁡U∧∀v∈B¬U<sv→U↾suc⁡G=v↾suc⁡G∧a∈suc⁡G→T↾suc⁡G⁡a=T⁡a
90 75 fvresd ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧G∈dom⁡U∧∀v∈B¬U<sv→U↾suc⁡G=v↾suc⁡G∧a∈suc⁡G→U↾suc⁡G⁡a=U⁡a
91 88 89 90 3eqtr4d ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧G∈dom⁡U∧∀v∈B¬U<sv→U↾suc⁡G=v↾suc⁡G∧a∈suc⁡G→T↾suc⁡G⁡a=U↾suc⁡G⁡a
92 91 ex ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧G∈dom⁡U∧∀v∈B¬U<sv→U↾suc⁡G=v↾suc⁡G→a∈suc⁡G→T↾suc⁡G⁡a=U↾suc⁡G⁡a
93 61 92 sylbid ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧G∈dom⁡U∧∀v∈B¬U<sv→U↾suc⁡G=v↾suc⁡G→a∈dom⁡T↾suc⁡G→T↾suc⁡G⁡a=U↾suc⁡G⁡a
94 93 ralrimiv ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧G∈dom⁡U∧∀v∈B¬U<sv→U↾suc⁡G=v↾suc⁡G→∀a∈dom⁡T↾suc⁡GT↾suc⁡G⁡a=U↾suc⁡G⁡a
95 nofun ⊢T∈No→Fun⁡T
96 95 funresd ⊢T∈No→Fun⁡T↾suc⁡G
97 4 96 syl ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧G∈dom⁡U∧∀v∈B¬U<sv→U↾suc⁡G=v↾suc⁡G→Fun⁡T↾suc⁡G
98 nofun ⊢U∈No→Fun⁡U
99 98 funresd ⊢U∈No→Fun⁡U↾suc⁡G
100 50 99 syl ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧G∈dom⁡U∧∀v∈B¬U<sv→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∈dom⁡T↾suc⁡GT↾suc⁡G⁡a=U↾suc⁡G⁡a
102 97 100 101 syl2anc ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧G∈dom⁡U∧∀v∈B¬U<sv→U↾suc⁡G=v↾suc⁡G→T↾suc⁡G=U↾suc⁡G↔dom⁡T↾suc⁡G=dom⁡U↾suc⁡G∧∀a∈dom⁡T↾suc⁡GT↾suc⁡G⁡a=U↾suc⁡G⁡a
103 60 94 102 mpbir2and ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧G∈dom⁡U∧∀v∈B¬U<sv→U↾suc⁡G=v↾suc⁡G→T↾suc⁡G=U↾suc⁡G