Theorem noetasuplem1

Description: Lemma for noeta . Establish that our final surreal really is a surreal. (Contributed by Scott Fenton, 6-Dec-2021)

	Ref	Expression
Hypotheses	noetasuplem.1	|- S = if ( E. x e. A A. y e. A -. x . } ) , ( g e. { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v ( u |` suc y ) = ( v |` suc y ) ) ) } |-> ( iota x E. u e. A ( g e. dom u /\ A. v e. A ( -. v ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) ) )
	noetasuplem.2	|- Z = ( S u. ( ( suc U. ( bday " B ) \ dom S ) X. { 1o } ) )
Assertion	noetasuplem1	|- ( ( A C_ No /\ A e. _V /\ B e. _V ) -> Z e. No )

Proof

Step	Hyp	Ref	Expression
1		noetasuplem.1	|- S = if ( E. x e. A A. y e. A -. x . } ) , ( g e. { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v ( u |` suc y ) = ( v |` suc y ) ) ) } |-> ( iota x E. u e. A ( g e. dom u /\ A. v e. A ( -. v ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) ) )
2		noetasuplem.2	|- Z = ( S u. ( ( suc U. ( bday " B ) \ dom S ) X. { 1o } ) )
3	1	nosupno	|- ( ( A C_ No /\ A e. _V ) -> S e. No )
4	3	3adant3	|- ( ( A C_ No /\ A e. _V /\ B e. _V ) -> S e. No )
5		bdayimaon	|- ( B e. _V -> suc U. ( bday " B ) e. On )
6	5	3ad2ant3	|- ( ( A C_ No /\ A e. _V /\ B e. _V ) -> suc U. ( bday " B ) e. On )
7		1oex	|- 1o e. _V
8	7	prid1	|- 1o e. { 1o , 2o }
9	8	noextendseq	|- ( ( S e. No /\ suc U. ( bday " B ) e. On ) -> ( S u. ( ( suc U. ( bday " B ) \ dom S ) X. { 1o } ) ) e. No )
10	4 6 9	syl2anc	|- ( ( A C_ No /\ A e. _V /\ B e. _V ) -> ( S u. ( ( suc U. ( bday " B ) \ dom S ) X. { 1o } ) ) e. No )
11	2 10	eqeltrid	|- ( ( A C_ No /\ A e. _V /\ B e. _V ) -> Z e. No )