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 ( E. x e. B A. y e. B -. y . } ) , ( g e. { y | E. u e. B ( y e. dom u /\ A. v e. B ( -. u ( u |` suc y ) = ( v |` suc y ) ) ) } |-> ( iota x E. u e. B ( g e. dom u /\ A. v e. B ( -. u ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) ) )
	noetainflem.2	|- W = ( T u. ( ( suc U. ( bday " A ) \ dom T ) X. { 2o } ) )
Assertion	noetainflem1	|- ( ( A e. _V /\ B C_ No /\ B e. _V ) -> W e. No )

Proof

Step	Hyp	Ref	Expression
1		noetainflem.1	|- T = if ( E. x e. B A. y e. B -. y . } ) , ( g e. { y | E. u e. B ( y e. dom u /\ A. v e. B ( -. u ( u |` suc y ) = ( v |` suc y ) ) ) } |-> ( iota x E. u e. B ( g e. dom u /\ A. v e. B ( -. u ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) ) )
2		noetainflem.2	|- W = ( T u. ( ( suc U. ( bday " A ) \ dom T ) X. { 2o } ) )
3	1	noinfno	|- ( ( B C_ No /\ B e. _V ) -> T e. No )
4	3	3adant1	|- ( ( A e. _V /\ B C_ No /\ B e. _V ) -> T e. No )
5		bdayimaon	|- ( A e. _V -> suc U. ( bday " A ) e. On )
6	5	3ad2ant1	|- ( ( A e. _V /\ B C_ No /\ B e. _V ) -> suc U. ( bday " A ) e. On )
7		2oex	|- 2o e. _V
8	7	prid2	|- 2o e. { 1o , 2o }
9	8	noextendseq	|- ( ( T e. No /\ suc U. ( bday " A ) e. On ) -> ( T u. ( ( suc U. ( bday " A ) \ dom T ) X. { 2o } ) ) e. No )
10	4 6 9	syl2anc	|- ( ( A e. _V /\ B C_ No /\ B e. _V ) -> ( T u. ( ( suc U. ( bday " A ) \ dom T ) X. { 2o } ) ) e. No )
11	2 10	eqeltrid	|- ( ( A e. _V /\ B C_ No /\ B e. _V ) -> W e. No )