Metamath Proof Explorer

Theorem bdaybndex

Description: Bounds formed from the birthday are surreal numbers. (Contributed by RP, 21-Sep-2023)

Ref Expression
Assertion bdaybndex 
|- ( ( A e. No /\ B = ( bday ` A ) /\ C e. { 1o , 2o } ) -> ( B X. { C } ) e. No )

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( A e. No /\ B = ( bday ` A ) ) -> B = ( bday ` A ) )
2 bdayval 
 |-  ( A e. No -> ( bday ` A ) = dom A )
3 2 adantr 
 |-  ( ( A e. No /\ B = ( bday ` A ) ) -> ( bday ` A ) = dom A )
4 1 3 eqtrd 
 |-  ( ( A e. No /\ B = ( bday ` A ) ) -> B = dom A )
5 nodmon 
 |-  ( A e. No -> dom A e. On )
6 5 adantr 
 |-  ( ( A e. No /\ B = ( bday ` A ) ) -> dom A e. On )
7 4 6 eqeltrd 
 |-  ( ( A e. No /\ B = ( bday ` A ) ) -> B e. On )
8 onnog 
 |-  ( ( B e. On /\ C e. { 1o , 2o } ) -> ( B X. { C } ) e. No )
9 7 8 stoic3 
 |-  ( ( A e. No /\ B = ( bday ` A ) /\ C e. { 1o , 2o } ) -> ( B X. { C } ) e. No )