Metamath Proof Explorer

Theorem noetainflem1

Description: Lemma for noeta . Establish that this particular construction gives a surreal. (Contributed by Scott Fenton, 9-Aug-2024)

Ref Expression
Hypotheses noetainflem.1 ⊢ T = if ∃ x ∈ B ∀ y ∈ B ¬ y < s x ι x ∈ B | ∀ y ∈ B ¬ y < s x ∪ dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x 1 𝑜 g ∈ y | ∃ u ∈ B y ∈ dom ⁡ u ∧ ∀ v ∈ B ¬ u < s v → u ↾ suc ⁡ y = v ↾ suc ⁡ y ⟼ ι x | ∃ u ∈ B g ∈ dom ⁡ u ∧ ∀ v ∈ B ¬ u < s v → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = x
noetainflem.2 ⊢ W = T ∪ suc ⁡ ⋃ bday A ∖ dom ⁡ T × 2 𝑜
Assertion noetainflem1 ⊢ A ∈ V ∧ B ⊆ No ∧ B ∈ V → W ∈ No

Proof

Step Hyp Ref Expression
1 noetainflem.1 ⊢ T = if ∃ x ∈ B ∀ y ∈ B ¬ y < s x ι x ∈ B | ∀ y ∈ B ¬ y < s x ∪ dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x 1 𝑜 g ∈ y | ∃ u ∈ B y ∈ dom ⁡ u ∧ ∀ v ∈ B ¬ u < s v → u ↾ suc ⁡ y = v ↾ suc ⁡ y ⟼ ι x | ∃ u ∈ B g ∈ dom ⁡ u ∧ ∀ v ∈ B ¬ u < s v → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = x
2 noetainflem.2 ⊢ W = T ∪ suc ⁡ ⋃ bday A ∖ dom ⁡ T × 2 𝑜
3 1 noinfno ⊢ B ⊆ No ∧ B ∈ V → T ∈ No
4 3 3adant1 ⊢ A ∈ V ∧ B ⊆ No ∧ B ∈ V → T ∈ No
5 bdayimaon ⊢ A ∈ V → suc ⁡ ⋃ bday A ∈ On
6 5 3ad2ant1 ⊢ A ∈ V ∧ B ⊆ No ∧ B ∈ V → suc ⁡ ⋃ bday A ∈ On
7 2oex ⊢ 2 𝑜 ∈ V
8 7 prid2 ⊢ 2 𝑜 ∈ 1 𝑜 2 𝑜
9 8 noextendseq ⊢ T ∈ No ∧ suc ⁡ ⋃ bday A ∈ On → T ∪ suc ⁡ ⋃ bday A ∖ dom ⁡ T × 2 𝑜 ∈ No
10 4 6 9 syl2anc ⊢ A ∈ V ∧ B ⊆ No ∧ B ∈ V → T ∪ suc ⁡ ⋃ bday A ∖ dom ⁡ T × 2 𝑜 ∈ No
11 2 10 eqeltrid ⊢ A ∈ V ∧ B ⊆ No ∧ B ∈ V → W ∈ No