Theorem om2noseqiso

Description: G is an isomorphism from the finite ordinals to a surreal sequence. (Contributed by Scott Fenton, 18-Apr-2025)

	Ref	Expression
Hypotheses	om2noseq.1	|- ( ph -> C e. No )
	om2noseq.2	|- ( ph -> G = ( rec ( ( x e. _V |-> ( x +s 1s ) ) , C ) |` _om ) )
	om2noseq.3	|- ( ph -> Z = ( rec ( ( x e. _V |-> ( x +s 1s ) ) , C ) " _om ) )
Assertion	om2noseqiso	|- ( ph -> G Isom _E ,

Proof

Step	Hyp	Ref	Expression
1		om2noseq.1	|- ( ph -> C e. No )
2		om2noseq.2	|- ( ph -> G = ( rec ( ( x e. _V |-> ( x +s 1s ) ) , C ) |` _om ) )
3		om2noseq.3	|- ( ph -> Z = ( rec ( ( x e. _V |-> ( x +s 1s ) ) , C ) " _om ) )
4	1 2 3	om2noseqf1o	|- ( ph -> G : _om -1-1-onto-> Z )
5		epel	|- ( y _E z <-> y e. z )
6	1 2 3	om2noseqlt2	|- ( ( ph /\ ( y e. _om /\ z e. _om ) ) -> ( y e. z <-> ( G ` y )
7	5 6	bitrid	|- ( ( ph /\ ( y e. _om /\ z e. _om ) ) -> ( y _E z <-> ( G ` y )
8	7	ralrimivva	|- ( ph -> A. y e. _om A. z e. _om ( y _E z <-> ( G ` y )
9		df-isom	|- ( G Isom _E , ( G : _om -1-1-onto-> Z /\ A. y e. _om A. z e. _om ( y _E z <-> ( G ` y )
10	4 8 9	sylanbrc	|- ( ph -> G Isom _E ,