Theorem bdaybndex

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

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

Proof

Step	Hyp	Ref	Expression
1		simpr	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 = ( bday ‘ 𝐴 ) ) → 𝐵 = ( bday ‘ 𝐴 ) )
2		bdayval	⊢ ( 𝐴 ∈ No → ( bday ‘ 𝐴 ) = dom 𝐴 )
3	2	adantr	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 = ( bday ‘ 𝐴 ) ) → ( bday ‘ 𝐴 ) = dom 𝐴 )
4	1 3	eqtrd	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 = ( bday ‘ 𝐴 ) ) → 𝐵 = dom 𝐴 )
5		nodmon	⊢ ( 𝐴 ∈ No → dom 𝐴 ∈ On )
6	5	adantr	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 = ( bday ‘ 𝐴 ) ) → dom 𝐴 ∈ On )
7	4 6	eqeltrd	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 = ( bday ‘ 𝐴 ) ) → 𝐵 ∈ On )
8		onnoxpg	⊢ ( ( 𝐵 ∈ On ∧ 𝐶 ∈ { 1o , 2o } ) → ( 𝐵 × { 𝐶 } ) ∈ No )
9	7 8	stoic3	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 = ( bday ‘ 𝐴 ) ∧ 𝐶 ∈ { 1o , 2o } ) → ( 𝐵 × { 𝐶 } ) ∈ No )