Theorem n0ons

Description: A surreal natural is a surreal ordinal. (Contributed by Scott Fenton, 2-Apr-2025)

	Ref	Expression
Assertion	n0ons	Could not format assertion : No typesetting found for |- ( A e. NN0_s -> A e. On_s ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		n0sno	Could not format ( A e. NN0_s -> A e. No ) : No typesetting found for |- ( A e. NN0_s -> A e. No ) with typecode |-
2		1sno	Could not format 1s e. No : No typesetting found for |- 1s e. No with typecode |-
3		subscl	Could not format ( ( A e. No /\ 1s e. No ) -> ( A -s 1s ) e. No ) : No typesetting found for |- ( ( A e. No /\ 1s e. No ) -> ( A -s 1s ) e. No ) with typecode |-
4	1 2 3	sylancl	Could not format ( A e. NN0_s -> ( A -s 1s ) e. No ) : No typesetting found for |- ( A e. NN0_s -> ( A -s 1s ) e. No ) with typecode |-
5		ovex	Could not format ( A -s 1s ) e. _V : No typesetting found for |- ( A -s 1s ) e. _V with typecode |-
6	5	snelpw	Could not format ( ( A -s 1s ) e. No <-> { ( A -s 1s ) } e. ~P No ) : No typesetting found for |- ( ( A -s 1s ) e. No <-> { ( A -s 1s ) } e. ~P No ) with typecode |-
7	4 6	sylib	Could not format ( A e. NN0_s -> { ( A -s 1s ) } e. ~P No ) : No typesetting found for |- ( A e. NN0_s -> { ( A -s 1s ) } e. ~P No ) with typecode |-
8		n0scut	Could not format ( A e. NN0_s -> A = ( { ( A -s 1s ) } |s (/) ) ) : No typesetting found for |- ( A e. NN0_s -> A = ( { ( A -s 1s ) } |s (/) ) ) with typecode |-
9		oveq1	Could not format ( x = { ( A -s 1s ) } -> ( x |s (/) ) = ( { ( A -s 1s ) } |s (/) ) ) : No typesetting found for |- ( x = { ( A -s 1s ) } -> ( x |s (/) ) = ( { ( A -s 1s ) } |s (/) ) ) with typecode |-
10	9	eqeq2d	Could not format ( x = { ( A -s 1s ) } -> ( A = ( x |s (/) ) <-> A = ( { ( A -s 1s ) } |s (/) ) ) ) : No typesetting found for |- ( x = { ( A -s 1s ) } -> ( A = ( x |s (/) ) <-> A = ( { ( A -s 1s ) } |s (/) ) ) ) with typecode |-
11	10	rspcev	Could not format ( ( { ( A -s 1s ) } e. ~P No /\ A = ( { ( A -s 1s ) } |s (/) ) ) -> E. x e. ~P No A = ( x |s (/) ) ) : No typesetting found for |- ( ( { ( A -s 1s ) } e. ~P No /\ A = ( { ( A -s 1s ) } |s (/) ) ) -> E. x e. ~P No A = ( x |s (/) ) ) with typecode |-
12	7 8 11	syl2anc	Could not format ( A e. NN0_s -> E. x e. ~P No A = ( x |s (/) ) ) : No typesetting found for |- ( A e. NN0_s -> E. x e. ~P No A = ( x |s (/) ) ) with typecode |-
13		elons2	Could not format ( A e. On_s <-> E. x e. ~P No A = ( x |s (/) ) ) : No typesetting found for |- ( A e. On_s <-> E. x e. ~P No A = ( x |s (/) ) ) with typecode |-
14	12 13	sylibr	Could not format ( A e. NN0_s -> A e. On_s ) : No typesetting found for |- ( A e. NN0_s -> A e. On_s ) with typecode |-