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	⊢ 𝑇 = if ( ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 , ( ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) ∪ { ⟨ dom ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) , 1o ⟩ } ) , ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) )
	noetainflem.2	⊢ 𝑊 = ( 𝑇 ∪ ( ( suc ∪ ( bday “ 𝐴 ) ∖ dom 𝑇 ) × { 2o } ) )
Assertion	noetainflem1	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ⊆ No ∧ 𝐵 ∈ V ) → 𝑊 ∈ No )

Proof

Step	Hyp	Ref	Expression
1		noetainflem.1	⊢ 𝑇 = if ( ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 , ( ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) ∪ { ⟨ dom ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) , 1o ⟩ } ) , ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) )
2		noetainflem.2	⊢ 𝑊 = ( 𝑇 ∪ ( ( suc ∪ ( bday “ 𝐴 ) ∖ dom 𝑇 ) × { 2o } ) )
3	1	noinfno	⊢ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) → 𝑇 ∈ No )
4	3	3adant1	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ⊆ No ∧ 𝐵 ∈ V ) → 𝑇 ∈ No )
5		bdayimaon	⊢ ( 𝐴 ∈ V → suc ∪ ( bday “ 𝐴 ) ∈ On )
6	5	3ad2ant1	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ⊆ No ∧ 𝐵 ∈ V ) → suc ∪ ( bday “ 𝐴 ) ∈ On )
7		2oex	⊢ 2o ∈ V
8	7	prid2	⊢ 2o ∈ { 1o , 2o }
9	8	noextendseq	⊢ ( ( 𝑇 ∈ No ∧ suc ∪ ( bday “ 𝐴 ) ∈ On ) → ( 𝑇 ∪ ( ( suc ∪ ( bday “ 𝐴 ) ∖ dom 𝑇 ) × { 2o } ) ) ∈ No )
10	4 6 9	syl2anc	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ⊆ No ∧ 𝐵 ∈ V ) → ( 𝑇 ∪ ( ( suc ∪ ( bday “ 𝐴 ) ∖ dom 𝑇 ) × { 2o } ) ) ∈ No )
11	2 10	eqeltrid	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ⊆ No ∧ 𝐵 ∈ V ) → 𝑊 ∈ No )