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	|- ( ( A e. On /\ X e. No ) -> ( X e. ( _N ` A ) <-> ( bday ` X ) = A ) )

Proof

Step	Hyp	Ref	Expression
1		madebday	|- ( ( A e. On /\ X e. No ) -> ( X e. ( _M ` A ) <-> ( bday ` X ) C_ A ) )
2		oldbday	|- ( ( A e. On /\ X e. No ) -> ( X e. ( _Old ` A ) <-> ( bday ` X ) e. A ) )
3	2	notbid	|- ( ( A e. On /\ X e. No ) -> ( -. X e. ( _Old ` A ) <-> -. ( bday ` X ) e. A ) )
4	1 3	anbi12d	|- ( ( A e. On /\ X e. No ) -> ( ( X e. ( _M ` A ) /\ -. X e. ( _Old ` A ) ) <-> ( ( bday ` X ) C_ A /\ -. ( bday ` X ) e. A ) ) )
5		newval	|- ( A e. On -> ( _N ` A ) = ( ( _M ` A ) \ ( _Old ` A ) ) )
6	5	eleq2d	|- ( A e. On -> ( X e. ( _N ` A ) <-> X e. ( ( _M ` A ) \ ( _Old ` A ) ) ) )
7		eldif	|- ( X e. ( ( _M ` A ) \ ( _Old ` A ) ) <-> ( X e. ( _M ` A ) /\ -. X e. ( _Old ` A ) ) )
8	6 7	bitrdi	|- ( A e. On -> ( X e. ( _N ` A ) <-> ( X e. ( _M ` A ) /\ -. X e. ( _Old ` A ) ) ) )
9	8	adantr	|- ( ( A e. On /\ X e. No ) -> ( X e. ( _N ` A ) <-> ( X e. ( _M ` A ) /\ -. X e. ( _Old ` A ) ) ) )
10		bdayelon	|- ( bday ` X ) e. On
11	10	onordi	|- Ord ( bday ` X )
12		eloni	|- ( A e. On -> Ord A )
13		ordtri4	|- ( ( Ord ( bday ` X ) /\ Ord A ) -> ( ( bday ` X ) = A <-> ( ( bday ` X ) C_ A /\ -. ( bday ` X ) e. A ) ) )
14	11 12 13	sylancr	|- ( A e. On -> ( ( bday ` X ) = A <-> ( ( bday ` X ) C_ A /\ -. ( bday ` X ) e. A ) ) )
15	14	adantr	|- ( ( A e. On /\ X e. No ) -> ( ( bday ` X ) = A <-> ( ( bday ` X ) C_ A /\ -. ( bday ` X ) e. A ) ) )
16	4 9 15	3bitr4d	|- ( ( A e. On /\ X e. No ) -> ( X e. ( _N ` A ) <-> ( bday ` X ) = A ) )