Theorem bdaybndbday

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

	Ref	Expression
Assertion	bdaybndbday	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 = ( bday ‘ 𝐴 ) ∧ 𝐶 ∈ { 1o , 2o } ) → ( bday ‘ ( 𝐵 × { 𝐶 } ) ) = ( bday ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		bdaybndex	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 = ( bday ‘ 𝐴 ) ∧ 𝐶 ∈ { 1o , 2o } ) → ( 𝐵 × { 𝐶 } ) ∈ No )
2		bdayval	⊢ ( ( 𝐵 × { 𝐶 } ) ∈ No → ( bday ‘ ( 𝐵 × { 𝐶 } ) ) = dom ( 𝐵 × { 𝐶 } ) )
3	1 2	syl	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 = ( bday ‘ 𝐴 ) ∧ 𝐶 ∈ { 1o , 2o } ) → ( bday ‘ ( 𝐵 × { 𝐶 } ) ) = dom ( 𝐵 × { 𝐶 } ) )
4		simp3	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 = ( bday ‘ 𝐴 ) ∧ 𝐶 ∈ { 1o , 2o } ) → 𝐶 ∈ { 1o , 2o } )
5		snnzg	⊢ ( 𝐶 ∈ { 1o , 2o } → { 𝐶 } ≠ ∅ )
6		dmxp	⊢ ( { 𝐶 } ≠ ∅ → dom ( 𝐵 × { 𝐶 } ) = 𝐵 )
7	4 5 6	3syl	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 = ( bday ‘ 𝐴 ) ∧ 𝐶 ∈ { 1o , 2o } ) → dom ( 𝐵 × { 𝐶 } ) = 𝐵 )
8		simp2	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 = ( bday ‘ 𝐴 ) ∧ 𝐶 ∈ { 1o , 2o } ) → 𝐵 = ( bday ‘ 𝐴 ) )
9	3 7 8	3eqtrd	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 = ( bday ‘ 𝐴 ) ∧ 𝐶 ∈ { 1o , 2o } ) → ( bday ‘ ( 𝐵 × { 𝐶 } ) ) = ( bday ‘ 𝐴 ) )