Metamath Proof Explorer

Theorem noinfbnd1lem6

Description: Lemma for noinfbnd1 . Establish a hard lower bound when there is no minimum. (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 noinfbnd1lem6 ⊢¬∃x∈B∀y∈B¬y<sx∧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 simp2l ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B→B⊆No
3 simp3 ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B→U∈B
4 2 3 sseldd ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B→U∈No
5 nofv ⊢U∈No→U⁡dom⁡T=∅∨U⁡dom⁡T=1𝑜∨U⁡dom⁡T=2𝑜
6 4 5 syl ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B→U⁡dom⁡T=∅∨U⁡dom⁡T=1𝑜∨U⁡dom⁡T=2𝑜
7 3oran ⊢U⁡dom⁡T=∅∨U⁡dom⁡T=1𝑜∨U⁡dom⁡T=2𝑜↔¬¬U⁡dom⁡T=∅∧¬U⁡dom⁡T=1𝑜∧¬U⁡dom⁡T=2𝑜
8 6 7 sylib ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B→¬¬U⁡dom⁡T=∅∧¬U⁡dom⁡T=1𝑜∧¬U⁡dom⁡T=2𝑜
9 simpl1 ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧T=U↾dom⁡T→¬∃x∈B∀y∈B¬y<sx
10 simpl2 ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧T=U↾dom⁡T→B⊆No∧B∈V
11 simpl3 ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧T=U↾dom⁡T→U∈B
12 simpr ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧T=U↾dom⁡T→T=U↾dom⁡T
13 12 eqcomd ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧T=U↾dom⁡T→U↾dom⁡T=T
14 1 noinfbnd1lem4 ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧U↾dom⁡T=T→U⁡dom⁡T≠∅
15 9 10 11 13 14 syl112anc ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧T=U↾dom⁡T→U⁡dom⁡T≠∅
16 15 neneqd ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧T=U↾dom⁡T→¬U⁡dom⁡T=∅
17 1 noinfbnd1lem3 ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧U↾dom⁡T=T→U⁡dom⁡T≠1𝑜
18 9 10 11 13 17 syl112anc ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧T=U↾dom⁡T→U⁡dom⁡T≠1𝑜
19 18 neneqd ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧T=U↾dom⁡T→¬U⁡dom⁡T=1𝑜
20 1 noinfbnd1lem5 ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧U↾dom⁡T=T→U⁡dom⁡T≠2𝑜
21 9 10 11 13 20 syl112anc ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧T=U↾dom⁡T→U⁡dom⁡T≠2𝑜
22 21 neneqd ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧T=U↾dom⁡T→¬U⁡dom⁡T=2𝑜
23 16 19 22 3jca ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B∧T=U↾dom⁡T→¬U⁡dom⁡T=∅∧¬U⁡dom⁡T=1𝑜∧¬U⁡dom⁡T=2𝑜
24 8 23 mtand ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B→¬T=U↾dom⁡T
25 1 noinfbnd1lem1 ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B→¬U↾dom⁡T<sT
26 1 noinfno ⊢B⊆No∧B∈V→T∈No
27 26 3ad2ant2 ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B→T∈No
28 nodmon ⊢T∈No→dom⁡T∈On
29 27 28 syl ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B→dom⁡T∈On
30 noreson ⊢U∈No∧dom⁡T∈On→U↾dom⁡T∈No
31 4 29 30 syl2anc ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B→U↾dom⁡T∈No
32 sltso ⊢<sOrNo
33 solin ⊢<sOrNo∧T∈No∧U↾dom⁡T∈No→T<sU↾dom⁡T∨T=U↾dom⁡T∨U↾dom⁡T<sT
34 32 33 mpan ⊢T∈No∧U↾dom⁡T∈No→T<sU↾dom⁡T∨T=U↾dom⁡T∨U↾dom⁡T<sT
35 27 31 34 syl2anc ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B→T<sU↾dom⁡T∨T=U↾dom⁡T∨U↾dom⁡T<sT
36 24 25 35 ecase23d ⊢¬∃x∈B∀y∈B¬y<sx∧B⊆No∧B∈V∧U∈B→T<sU↾dom⁡T