Metamath Proof Explorer

Theorem bdaybndbday

Description: Bounds formed from the birthday have the same birthday. (Contributed by RP, 30-Sep-2023)

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

Proof

Step Hyp Ref Expression
1 bdaybndex 
 |-  ( ( A e. No /\ B = ( bday ` A ) /\ C e. { 1o , 2o } ) -> ( B X. { C } ) e. No )
2 bdayval 
 |-  ( ( B X. { C } ) e. No -> ( bday ` ( B X. { C } ) ) = dom ( B X. { C } ) )
3 1 2 syl 
 |-  ( ( A e. No /\ B = ( bday ` A ) /\ C e. { 1o , 2o } ) -> ( bday ` ( B X. { C } ) ) = dom ( B X. { C } ) )
4 simp3 
 |-  ( ( A e. No /\ B = ( bday ` A ) /\ C e. { 1o , 2o } ) -> C e. { 1o , 2o } )
5 snnzg 
 |-  ( C e. { 1o , 2o } -> { C } =/= (/) )
6 dmxp 
 |-  ( { C } =/= (/) -> dom ( B X. { C } ) = B )
7 4 5 6 3syl 
 |-  ( ( A e. No /\ B = ( bday ` A ) /\ C e. { 1o , 2o } ) -> dom ( B X. { C } ) = B )
8 simp2 
 |-  ( ( A e. No /\ B = ( bday ` A ) /\ C e. { 1o , 2o } ) -> B = ( bday ` A ) )
9 3 7 8 3eqtrd 
 |-  ( ( A e. No /\ B = ( bday ` A ) /\ C e. { 1o , 2o } ) -> ( bday ` ( B X. { C } ) ) = ( bday ` A ) )