Metamath Proof Explorer

Theorem noreson

Description: The restriction of a surreal to an ordinal is still a surreal. (Contributed by Scott Fenton, 4-Sep-2011)

Ref Expression
Assertion noreson 
|- ( ( A e. No /\ B e. On ) -> ( A |` B ) e. No )

Proof

Step Hyp Ref Expression
1 elno 
 |-  ( A e. No <-> E. x e. On A : x --> { 1o , 2o } )
2 onin 
 |-  ( ( x e. On /\ B e. On ) -> ( x i^i B ) e. On )
3 fresin 
 |-  ( A : x --> { 1o , 2o } -> ( A |` B ) : ( x i^i B ) --> { 1o , 2o } )
4 feq2 
 |-  ( y = ( x i^i B ) -> ( ( A |` B ) : y --> { 1o , 2o } <-> ( A |` B ) : ( x i^i B ) --> { 1o , 2o } ) )
5 4 rspcev 
 |-  ( ( ( x i^i B ) e. On /\ ( A |` B ) : ( x i^i B ) --> { 1o , 2o } ) -> E. y e. On ( A |` B ) : y --> { 1o , 2o } )
6 2 3 5 syl2an 
 |-  ( ( ( x e. On /\ B e. On ) /\ A : x --> { 1o , 2o } ) -> E. y e. On ( A |` B ) : y --> { 1o , 2o } )
7 6 an32s 
 |-  ( ( ( x e. On /\ A : x --> { 1o , 2o } ) /\ B e. On ) -> E. y e. On ( A |` B ) : y --> { 1o , 2o } )
8 7 ex 
 |-  ( ( x e. On /\ A : x --> { 1o , 2o } ) -> ( B e. On -> E. y e. On ( A |` B ) : y --> { 1o , 2o } ) )
9 8 rexlimiva 
 |-  ( E. x e. On A : x --> { 1o , 2o } -> ( B e. On -> E. y e. On ( A |` B ) : y --> { 1o , 2o } ) )
10 9 imp 
 |-  ( ( E. x e. On A : x --> { 1o , 2o } /\ B e. On ) -> E. y e. On ( A |` B ) : y --> { 1o , 2o } )
11 1 10 sylanb 
 |-  ( ( A e. No /\ B e. On ) -> E. y e. On ( A |` B ) : y --> { 1o , 2o } )
12 elno 
 |-  ( ( A |` B ) e. No <-> E. y e. On ( A |` B ) : y --> { 1o , 2o } )
13 11 12 sylibr 
 |-  ( ( A e. No /\ B e. On ) -> ( A |` B ) e. No )