Theorem newbday

Description: A surreal is an element of a new set iff its birthday is equal to that ordinal. Remark in Conway p. 29. (Contributed by Scott Fenton, 19-Aug-2024)

	Ref	Expression
Assertion	newbday	⊢ ( ( 𝐴 ∈ On ∧ 𝑋 ∈ No ) → ( 𝑋 ∈ ( N ‘ 𝐴 ) ↔ ( bday ‘ 𝑋 ) = 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		madebday	⊢ ( ( 𝐴 ∈ On ∧ 𝑋 ∈ No ) → ( 𝑋 ∈ ( M ‘ 𝐴 ) ↔ ( bday ‘ 𝑋 ) ⊆ 𝐴 ) )
2		oldbday	⊢ ( ( 𝐴 ∈ On ∧ 𝑋 ∈ No ) → ( 𝑋 ∈ ( O ‘ 𝐴 ) ↔ ( bday ‘ 𝑋 ) ∈ 𝐴 ) )
3	2	notbid	⊢ ( ( 𝐴 ∈ On ∧ 𝑋 ∈ No ) → ( ¬ 𝑋 ∈ ( O ‘ 𝐴 ) ↔ ¬ ( bday ‘ 𝑋 ) ∈ 𝐴 ) )
4	1 3	anbi12d	⊢ ( ( 𝐴 ∈ On ∧ 𝑋 ∈ No ) → ( ( 𝑋 ∈ ( M ‘ 𝐴 ) ∧ ¬ 𝑋 ∈ ( O ‘ 𝐴 ) ) ↔ ( ( bday ‘ 𝑋 ) ⊆ 𝐴 ∧ ¬ ( bday ‘ 𝑋 ) ∈ 𝐴 ) ) )
5		newval	⊢ ( 𝐴 ∈ On → ( N ‘ 𝐴 ) = ( ( M ‘ 𝐴 ) ∖ ( O ‘ 𝐴 ) ) )
6	5	eleq2d	⊢ ( 𝐴 ∈ On → ( 𝑋 ∈ ( N ‘ 𝐴 ) ↔ 𝑋 ∈ ( ( M ‘ 𝐴 ) ∖ ( O ‘ 𝐴 ) ) ) )
7		eldif	⊢ ( 𝑋 ∈ ( ( M ‘ 𝐴 ) ∖ ( O ‘ 𝐴 ) ) ↔ ( 𝑋 ∈ ( M ‘ 𝐴 ) ∧ ¬ 𝑋 ∈ ( O ‘ 𝐴 ) ) )
8	6 7	bitrdi	⊢ ( 𝐴 ∈ On → ( 𝑋 ∈ ( N ‘ 𝐴 ) ↔ ( 𝑋 ∈ ( M ‘ 𝐴 ) ∧ ¬ 𝑋 ∈ ( O ‘ 𝐴 ) ) ) )
9	8	adantr	⊢ ( ( 𝐴 ∈ On ∧ 𝑋 ∈ No ) → ( 𝑋 ∈ ( N ‘ 𝐴 ) ↔ ( 𝑋 ∈ ( M ‘ 𝐴 ) ∧ ¬ 𝑋 ∈ ( O ‘ 𝐴 ) ) ) )
10		bdayelon	⊢ ( bday ‘ 𝑋 ) ∈ On
11	10	onordi	⊢ Ord ( bday ‘ 𝑋 )
12		eloni	⊢ ( 𝐴 ∈ On → Ord 𝐴 )
13		ordtri4	⊢ ( ( Ord ( bday ‘ 𝑋 ) ∧ Ord 𝐴 ) → ( ( bday ‘ 𝑋 ) = 𝐴 ↔ ( ( bday ‘ 𝑋 ) ⊆ 𝐴 ∧ ¬ ( bday ‘ 𝑋 ) ∈ 𝐴 ) ) )
14	11 12 13	sylancr	⊢ ( 𝐴 ∈ On → ( ( bday ‘ 𝑋 ) = 𝐴 ↔ ( ( bday ‘ 𝑋 ) ⊆ 𝐴 ∧ ¬ ( bday ‘ 𝑋 ) ∈ 𝐴 ) ) )
15	14	adantr	⊢ ( ( 𝐴 ∈ On ∧ 𝑋 ∈ No ) → ( ( bday ‘ 𝑋 ) = 𝐴 ↔ ( ( bday ‘ 𝑋 ) ⊆ 𝐴 ∧ ¬ ( bday ‘ 𝑋 ) ∈ 𝐴 ) ) )
16	4 9 15	3bitr4d	⊢ ( ( 𝐴 ∈ On ∧ 𝑋 ∈ No ) → ( 𝑋 ∈ ( N ‘ 𝐴 ) ↔ ( bday ‘ 𝑋 ) = 𝐴 ) )