Metamath Proof Explorer

Theorem noetainflem3

Description: Lemma for noeta . W bounds B below . (Contributed by Scott Fenton, 9-Aug-2024)

Ref Expression
Hypotheses noetainflem.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
noetainflem.2 ⊢W=T∪suc⁡⋃bdayA∖dom⁡T×2𝑜
Assertion noetainflem3 ⊢A∈V∧B⊆No∧B∈V∧Y∈B→W<sY

Proof

Step Hyp Ref Expression
1 noetainflem.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 noetainflem.2 ⊢W=T∪suc⁡⋃bdayA∖dom⁡T×2𝑜
3 simpl2 ⊢A∈V∧B⊆No∧B∈V∧Y∈B→B⊆No
4 simpl3 ⊢A∈V∧B⊆No∧B∈V∧Y∈B→B∈V
5 1 2 noetainflem2 ⊢B⊆No∧B∈V→W↾dom⁡T=T
6 3 4 5 syl2anc ⊢A∈V∧B⊆No∧B∈V∧Y∈B→W↾dom⁡T=T
7 simpr ⊢A∈V∧B⊆No∧B∈V∧Y∈B→Y∈B
8 1 noinfbnd1 ⊢B⊆No∧B∈V∧Y∈B→T<sY↾dom⁡T
9 3 4 7 8 syl3anc ⊢A∈V∧B⊆No∧B∈V∧Y∈B→T<sY↾dom⁡T
10 6 9 eqbrtrd ⊢A∈V∧B⊆No∧B∈V∧Y∈B→W↾dom⁡T<sY↾dom⁡T
11 1 2 noetainflem1 ⊢A∈V∧B⊆No∧B∈V→W∈No
12 11 adantr ⊢A∈V∧B⊆No∧B∈V∧Y∈B→W∈No
13 simp2 ⊢A∈V∧B⊆No∧B∈V→B⊆No
14 13 sselda ⊢A∈V∧B⊆No∧B∈V∧Y∈B→Y∈No
15 1 noinfno ⊢B⊆No∧B∈V→T∈No
16 3 4 15 syl2anc ⊢A∈V∧B⊆No∧B∈V∧Y∈B→T∈No
17 nodmon ⊢T∈No→dom⁡T∈On
18 16 17 syl ⊢A∈V∧B⊆No∧B∈V∧Y∈B→dom⁡T∈On
19 sltres ⊢W∈No∧Y∈No∧dom⁡T∈On→W↾dom⁡T<sY↾dom⁡T→W<sY
20 12 14 18 19 syl3anc ⊢A∈V∧B⊆No∧B∈V∧Y∈B→W↾dom⁡T<sY↾dom⁡T→W<sY
21 10 20 mpd ⊢A∈V∧B⊆No∧B∈V∧Y∈B→W<sY