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	⊢ ( N ‘ 𝐴 ) = ( ( M ‘ 𝐴 ) ∖ ( O ‘ 𝐴 ) )
6	5	a1i	⊢ ( 𝐴 ∈ On → ( N ‘ 𝐴 ) = ( ( M ‘ 𝐴 ) ∖ ( O ‘ 𝐴 ) ) )
7	6	eleq2d	⊢ ( 𝐴 ∈ On → ( 𝑋 ∈ ( N ‘ 𝐴 ) ↔ 𝑋 ∈ ( ( M ‘ 𝐴 ) ∖ ( O ‘ 𝐴 ) ) ) )
8		eldif	⊢ ( 𝑋 ∈ ( ( M ‘ 𝐴 ) ∖ ( O ‘ 𝐴 ) ) ↔ ( 𝑋 ∈ ( M ‘ 𝐴 ) ∧ ¬ 𝑋 ∈ ( O ‘ 𝐴 ) ) )
9	7 8	bitrdi	⊢ ( 𝐴 ∈ On → ( 𝑋 ∈ ( N ‘ 𝐴 ) ↔ ( 𝑋 ∈ ( M ‘ 𝐴 ) ∧ ¬ 𝑋 ∈ ( O ‘ 𝐴 ) ) ) )
10	9	adantr	⊢ ( ( 𝐴 ∈ On ∧ 𝑋 ∈ No ) → ( 𝑋 ∈ ( N ‘ 𝐴 ) ↔ ( 𝑋 ∈ ( M ‘ 𝐴 ) ∧ ¬ 𝑋 ∈ ( O ‘ 𝐴 ) ) ) )
11		bdayelon	⊢ ( bday ‘ 𝑋 ) ∈ On
12	11	onordi	⊢ Ord ( bday ‘ 𝑋 )
13		eloni	⊢ ( 𝐴 ∈ On → Ord 𝐴 )
14		ordtri4	⊢ ( ( Ord ( bday ‘ 𝑋 ) ∧ Ord 𝐴 ) → ( ( bday ‘ 𝑋 ) = 𝐴 ↔ ( ( bday ‘ 𝑋 ) ⊆ 𝐴 ∧ ¬ ( bday ‘ 𝑋 ) ∈ 𝐴 ) ) )
15	12 13 14	sylancr	⊢ ( 𝐴 ∈ On → ( ( bday ‘ 𝑋 ) = 𝐴 ↔ ( ( bday ‘ 𝑋 ) ⊆ 𝐴 ∧ ¬ ( bday ‘ 𝑋 ) ∈ 𝐴 ) ) )
16	15	adantr	⊢ ( ( 𝐴 ∈ On ∧ 𝑋 ∈ No ) → ( ( bday ‘ 𝑋 ) = 𝐴 ↔ ( ( bday ‘ 𝑋 ) ⊆ 𝐴 ∧ ¬ ( bday ‘ 𝑋 ) ∈ 𝐴 ) ) )
17	4 10 16	3bitr4d	⊢ ( ( 𝐴 ∈ On ∧ 𝑋 ∈ No ) → ( 𝑋 ∈ ( N ‘ 𝐴 ) ↔ ( bday ‘ 𝑋 ) = 𝐴 ) )