Metamath Proof Explorer

Theorem onnog

Description: Every ordinal maps to a surreal number. (Contributed by RP, 21-Sep-2023)

Ref Expression
Assertion onnog 
|- ( ( A e. On /\ B e. { 1o , 2o } ) -> ( A X. { B } ) e. No )

Proof

Step Hyp Ref Expression
1 fconst6g 
 |-  ( B e. { 1o , 2o } -> ( A X. { B } ) : A --> { 1o , 2o } )
2 1 adantl 
 |-  ( ( A e. On /\ B e. { 1o , 2o } ) -> ( A X. { B } ) : A --> { 1o , 2o } )
3 simp3 
 |-  ( ( A e. On /\ B e. { 1o , 2o } /\ ( A X. { B } ) : A --> { 1o , 2o } ) -> ( A X. { B } ) : A --> { 1o , 2o } )
4 3 ffund 
 |-  ( ( A e. On /\ B e. { 1o , 2o } /\ ( A X. { B } ) : A --> { 1o , 2o } ) -> Fun ( A X. { B } ) )
5 simp2 
 |-  ( ( A e. On /\ B e. { 1o , 2o } /\ ( A X. { B } ) : A --> { 1o , 2o } ) -> B e. { 1o , 2o } )
6 snnzg 
 |-  ( B e. { 1o , 2o } -> { B } =/= (/) )
7 dmxp 
 |-  ( { B } =/= (/) -> dom ( A X. { B } ) = A )
8 7 eqcomd 
 |-  ( { B } =/= (/) -> A = dom ( A X. { B } ) )
9 5 6 8 3syl 
 |-  ( ( A e. On /\ B e. { 1o , 2o } /\ ( A X. { B } ) : A --> { 1o , 2o } ) -> A = dom ( A X. { B } ) )
10 simp1 
 |-  ( ( A e. On /\ B e. { 1o , 2o } /\ ( A X. { B } ) : A --> { 1o , 2o } ) -> A e. On )
11 9 10 eqeltrrd 
 |-  ( ( A e. On /\ B e. { 1o , 2o } /\ ( A X. { B } ) : A --> { 1o , 2o } ) -> dom ( A X. { B } ) e. On )
12 3 frnd 
 |-  ( ( A e. On /\ B e. { 1o , 2o } /\ ( A X. { B } ) : A --> { 1o , 2o } ) -> ran ( A X. { B } ) C_ { 1o , 2o } )
13 elno2 
 |-  ( ( A X. { B } ) e. No <-> ( Fun ( A X. { B } ) /\ dom ( A X. { B } ) e. On /\ ran ( A X. { B } ) C_ { 1o , 2o } ) )
14 4 11 12 13 syl3anbrc 
 |-  ( ( A e. On /\ B e. { 1o , 2o } /\ ( A X. { B } ) : A --> { 1o , 2o } ) -> ( A X. { B } ) e. No )
15 2 14 mpd3an3 
 |-  ( ( A e. On /\ B e. { 1o , 2o } ) -> ( A X. { B } ) e. No )